Weekly log for 31 May 2026

End of classes

This week was the last week of lectures for graduate courses at Caltech. I’m quite sad that the quarter is over, especially since Monday was Memorial Day (a holiday in the US).

Notes

I’m continuing to transcribe my Forest into plain TeX. There is a lot of material I want to discuss, but will probably end up “on the cutting room floor”.

Indexing terms

I am getting bogged down with indexing terms. I’ll probably skip it for now, but circle back to it eventually. (Actually, a lot of writing manuals suggest to defer writing the index until you’re done with the manuscript, so it is wise to skip it for now…)

Proof Assistant progress

Equality is decidable

There’s a metatheorem which is unprovable in Myo: $\vdash(\exists f\ldotp\forall x\ldotp f(x)=0\iff P[x])\implies\forall x\ldotp(P[x]\lor\neg P[x])$. Informally: if there is a function-sorted term $f$ such that $f(x)=0$ whenever $P[x]$ holds, then $P[-]$ is a decidable predicate.

We can define the equality function $E(x,y):=D(x,y,0,1)$ which allows us to observe that equality of individual-sorted terms is decidable.

This cannot be proven using Myo because it requires defining a second-order predicate “$P$ is decidable” which is impossible in first-order logic.

Declarative-style proofs

I realize it would be really beneficial to have declarative-style proofs for Myo. This is something I think I can work towards, but only because I am standing on the shoulders of giants. In particular, John Harrison and Freek Wiedijk did amazing work implementing declarative-style proofs for HOL Light (which, in turn, was based on the amazing work of the Mizar proof assistant).

I believe that the Mizar language (for proofs) can be implemented for Myo, more or less. The only idiosyncracy is that we have to use Title_Cased_Words. Oh, and the semantics are slightly different (at least because the checker is weaker, and the type system is different/weaker).

Intuitionistic Tableaux

Towards that end (implementing declarative-style proofs for Myo), I need to implement Intuitionistic tableaux method. Philip Zucker shared with me Otten’s paper on Intuitionistic tableaux, so I want to thank him for the reference.

Just some reading list I should remember (for myself):

• Otten and Kreitz’s “T-String-Unification: Unifying Prefixes in Non-Classical Proof Methods” Eprint
• Jens Otten’s “ileanTAP: An Intuitionistic Theorem Prover”. Eprint

Beware: iLeanTAP uses Prolog’s ^ operator, which is wonky (consult David Tonhofer excellent answer about it).

Also, after reading Mauro ALLEGRANZA’s helpful answer, I think I should also look up (viz., pp.29 et seq):

• Melvin Fitting, Intuitionistic logic, Model theory and Forcing (1969)

Fitting notes that signed formulas have a different interpretation in Intuitionistic logic, namely $TX$ means “X is proven”, but $FX$ means “X has not been proven” (or “X is not known to be true”). This matters since the rules for Intuitionistic tableaux are

where $a$ is fresh (“new”) in that last rule, and $S_{T}=\{TX\mid TX\in S\}$.

(Fitting’s book is very, very good for people who want to become familiar with model theory for Intuitionistic logic.)