Weekly log for 17 May 2026

Proof assistant stuff

There are a few things I want to work on next with Myo:

  1. Finish unit testing tactics
  2. Implement definitions (this would require implementing a binary search tree, of some kind)
  3. Implement conversions for rewriting

Like a donkey caught equidistant between three bales of hay, I find myself starving to death.

Progress with unit tests and tactics

I have added more unit tests to Myo, specifically checking the tactics work by re-deriving results from derived.sml.

Surprisingly, I caught a few bugs this way! That’s great news!

This tells me I should continue writing unit tests, but I am easily distracted.

Definition-by-cases issues

Feferman claims characteristic functions exist in $FS_{0}$, but I cannot prove it. Certainly, it does not follow from the axioms. I think we need definition-by-cases. I think this follows from the usual definitional principle for terms in first-order logic, but I’m having difficulty proving it.

I spent this week fruitlessly thinking about definition-by-cases. I noticed that Mizar does something like (if $P[x]$ abbreviates $(C\implies A[x])\land(\neg C\implies B[x])$): \begin{equation} \frac{\vdash(C\implies\exists x\ldotp A[x])\land(\neg C\implies\exists x\ldotp B[x]),\qquad\vdash\forall x,y\ldotp P[x]\land P[y]\implies x=y}{\vdash\exists!x\ldotp P[x]} \end{equation} Several undergraduates were interested in the problem I was trying to solve.

I gave a brief 30-minute talk about the background to this problem, how it came about. Most of this was about the basic concepts of $FS_{0}$, metalogical frameworks, inductively-defined judgements as a suitable approximation of “deductive systems”, and so on.

Abandoning forester

I have decided to stop using Forester for notes about Myo and proof assistants. Forester was too unstable, and it was too difficult to migrate to Forester 5.

Instead, I have migrated to plain TeX with my “poor man’s LaTeX” macros. I don’t think I’ll make my notes public, but I have written a bit about “poor man’s LaTeX” elsewhere. Briefly, it’s a minimal subset of LaTeX macros to support environments, counters, links, and very little else.

Since I’m writing a bunch of “numbered paragraphs” (like Allen U. Kennington’s Differential Geometry Reconstructed), these macros are “good enough”.

Plain TeX has the advantage of longevity and stability. I know 1000 years from now (if humans have not killed themselves off), this TeX will compile just fine. I could not say the same thing about Forester.

Reading

I had to stop reading Douglas Adams’s Hitchiker’s Guide to the Galaxy. It was just too tedious to read.

I’ve been reading Salvatore’s Icewind Dale trilogy on the commute to Caltech and back. Well, I finished the first book, and just started Streams of Silver Friday.

Before bed, I am re-reading the Gotrek & Felix omnibus (volume I).