Weekly log for 24 May 2026

Ditch day

Last Friday was Caltech’s “ditch day”. Caltech’s undergraduates are organized into “houses” (the dormitories where they reside), and seniors plan an elaborate scavanger hunt for ditch day. Each house has its own independent scavanger hunt.

This year, one house had themed its ditch day around “the amazing race”: people in the house formed teams of 3 or so, then used the clues to find where they were supposed to race off to.

On the bus ride home, I ran into one “amazing race” team. I offered them help, they were trying to get to Echo Park. They got off at Del Mar station, and took the subway to Lincoln/Cypress station. I wonder how they fared?

Like Mark Twain in A Tramp Abroad, I found myself (by random chance) cheering on one particular team, and I wish them well.

Proof assistant stuff

Since Friday was “ditch day” at Caltech, I outlined material I wanted to edit, add, or revise in the literate program for Myo.

Again, I am working on it slowly.

Decidable equality

I’ve also been bogged down with Intuitionistic logic and decidable equality. (The Devil take this Intuitionism!) “Decidable equality” means we have the theorem $\vdash\forall x,y\ldotp(x=y\lor x\neq y)$.

I believe (thanks to $FS_{0}$ induction on the universe axiom), we can prove equality is decidable for individual-sorted terms in $FS_{0}$…but I have not proven it. I would like to say, “And I will get to it this week!” But I cannot, I suspect I will be bogged down with a lot of distractions.

I mean, I should be able to prove this claim using Myo.

In general, identity is not a decidable binary relation in Intuitionistic logic (c.f., top of page 16 of this PDF).

Tactics

I have not been able to dedicate adequate time to tactics. I suspect I will have to add a “kludge” Tactic.exists_elim which corresponds to the Thm.exists_elim inference rule, rather than figure out how to use Tactic.choose properly.

Note taking migration

I am in the middle of migrating from Forester to plain TeX.

During this process, I am also adding more notes about $FS_{0}$ set theory.

“Agile” note-taking

This has made me ponder a bit more about Luhmann’s Zettelkasten. I think one critical aspect which people neglect is that a ZK is an “agile” note-taking system: you “live” in it.

In particular, you should “wander” through it, revisiting old threads, and thinking about new material to add.

I thought about writing something about this to post to the /r/zettelkasten subreddit, but I don’t think anyone would be interested.

I’m not sure if what I’m doing qualifies as a Zettelkasten, per se.

Luhmann’s Zettelkasten

I’ve been arguing with myself about the importance of autopoiesis in Luhmann’s Zettelkasten system, and I keep talking myself into the opposite position I held the day before.

I can see the argument in favor of it, and against it.

However, I think that Luhmann’s theory of communication (particularly the role “understanding” plays) turns out to be important in understanding his note-taking methodology.

Patching TeX macros

I have patched my \label macro to write to the .aux file. I’m not sure how I feel about this, the old macros ensures a “linear ordering” (which is not what you want with a Zettelkasten!).

Reading

I finished R.A. Salvatore’s Streams of Silver yesterday (Saturday). It was amusing enough. I will start The Halfling’s Gem probably this Wednesday.

I have noticed I am not going to bed as early, so I am not reading as much before sleeping. By this I mean, I am going to bed at 7pm instead of 6pm, so it’s just one hour less of reading.