Weekly log for 7 June 2026

Leaving town next week

I think I will be leaving town next week to visit family and friends in Sacramento. I expect to be out of town for a week, so the next “weekly log” may be abbreviated and late.

Proof assistant progress

I realize I have been sitting on a few changes since May 7th, which I have not pushed in! How embarrassing! Ah, well, I pushed them in on Wednesday and Thursday of this week.

Also, I have found Solomon Feferman’s earlier paper “Inductively presented systems and the formalization of metamathematics” (doi:10.1016/S0049-237X(09)70506-3, 1982) invaluable in trying to make sense of cryptic passages of his 1989 paper on $FS_{0}$. The earlier paper was freely available online until recently, so…there you have it…

Characteristic functions are definable?

I have been arguing with myself about whether characteristic functions for class-sorted terms is a well-defined notion in $FS_{0}$.

We can try defining it by induction on the structure of class-sorted terms, but inductively-defined classes $\mathcal{I}_{2}(A,B)$ pose a problem for this strategy.

I vaguely recall Feferman introducing the class of derivation trees $D(A,B)$ defined inductively as $D(A,B):=\mathcal{I}_2 (A’,B’)$ where $A’=\{(0,x)\mid x\in A\}$ and $B’=\{((d_1, d_2), x)\mid(x,\pi_2 d_1,\pi_2 d_2)\in B\}$ which consists of ordered pairs $(d,x)$ where $d$ is the derivation tree for $x\in\mathcal{I}_2 (A,B)$.

At first, it seems like proving “If there exists characteristic functions $c_{A}$ and $c_{B}$ for classes $A$ and $B$, then there exists a characteristic function $c_{D}$ for the class of derivation trees $D(A,B)$” by primitive recursion, but that requires a variant of primitive recursion different from the axiom found in $FS_{0}$.

So what? Well, if characteristic functions are definable using induction and primitive recursion alone, and every class-sorted term has a characteristic function, then class-membership is a decidable predicate and we have the theorem $\vdash\forall C\ldotp\forall x\ldotp x\in C\lor x\notin C$ (for any class-sorted term $C$ and for any individual-sorted term $x$, either $x\in C$ or $x\notin C$).

Missing Axioms

I also realized that there is an axiom missing from Feferman 1989 paper on $FS_{0}$:

\[\vdash\forall x\ldotp x=0\lor\bigl(\exists y,z\ldotp x=(y,z)\bigr)\tag{1}\]

Since $FS_{0}$ was a “pure Lisp”, there are no other urelements other than the $0$ constant, so nothing is really lost here.

Equivalently, since equality is decidable, adding the following axiom will allow us to derive the result in Equation (1) as a theorem:

\[\vdash\forall x\ldotp x\neq0\iff\bigl(\exists y,z\ldotp x=(y,z)\bigr)\tag{2}\]

The $\Longleftarrow$ direction is obvious with the axioms found in the paper. (Hint: its contrapositive is literally one of the axioms!) But the forwards direction is not at all obvious (and wrong if there are other Urelements allowed).

If we have Equation (1), then we can prove the theorem concerning the existence of the characteristic function for derivation trees $D(A,B)$ discussed in the previous section.

(In)efficiency concerns

It dawned on me as I was trying to sleep that the way I have implemented first-order logic may be inefficient. It may be more efficient to implement something like HOL’s approach to higher-order logic: use a simply-typed lambda calculus with primitive equality, then add a prop (analogous to HOL’s bool) and term (analogous to HOL’s ind) types.

Coincidentally, this is what Lisa does — see, e.g.:

(Lisa calls its ortholattice first-order logic $F(OL)^{2}$ but it should really be $OLFOL$ [homonym of ‘awful’]. Or better, since it is a weak ortholattice first-order logic, it’s $WOLFOL$ [homonym of ‘waffle’ the delicious breakfast item].)

It would be possible to have first-class schemes and class-comprehension operators (instad of the hacks I currently have).

But it might be too odious in other regards. For example, it would completely break Standard ML’s built-in pattern matching with formulas (which would only matter in the Formula module).

Reflections on literate programming

After having written a large-ish literate program, I think one observation worth passing along is: it pays dividends to write a series of fairly self-contained modules or “units”. In other words, “serialize” your program like Charles Dickens serialized his books.

I say this because the XUnit testing framework (Appendix B) originated as a self-contained vignette. As such, I could edit it down, simplify the code, polish the prose, etc., without too much worry: it was self-contained, almost nothing else directly depended on it.

All I needed to do was provide a contract for how to write tests using the Assert module and they had to have their type signature be Test.Case : string * (unit -> unit) -> Test.t. All that was really needed was name : string and test : unit -> unit be provided, and I could construct a test case from these alone.

Unfortunately, there is not much else which can be so isolated as this (in Myo, at least). I can’t rewrite, say, the Term module with this in mind: it’s needed by too many other modules, there’s no way to isolate it to just one or two public-facing functions. Revising the code would be, well, difficult.

Transcribing notes

I’m continuing my migration from Forester to plain TeX, and expanding on the material I’m including. So far I’ve written iii+61 pages of notes (I started the week with iii+25 or iii+40 pages of notes).

I have added some notes about Intuitionistic first-order logic, proving a grocery list of theorems using natural deduction.

Structured Proofs macros

I have also written some macros (in plain TeX) for “structured proofs” similar to Leslie Lamport’s “structured proofs”, but using Mizar syntax.

The neat thing about it is that I have the proof steps be their own command \Consider\ x, y, z \st\ ..., \Let\ $A$, $B$ be classes \PerCases\ since $x\in A$ or $x\notin A$, etc.

I also have “suppose” be their own environment \begin{Suppose}{$x\in A$}...\end{Suppose}.

The outermost proof environment will also end with a QED symbol.

Some quirks: If you want to use the previous proof step as part of the justification for the current proof step when proving a formula, then you use the command \ThenHave\ ... (instead of Mizar’s then ...). But when combining then with a proof step like consider, you can write \Then\Consider.

There are probably other quirks I am forgetting about.

However, the implementation only uses 2 counters (whereas, I think, Lamport’s macros uses “as many counters as necessary”), which is something I am proud of.

Using structured proofs

I’ve used these macros to prove some elementary things, like the existence and uniqueness of the empty class in $FS_{0}$, or the existence and uniqueness of the singleton class $\{x\}$ in $FS_{0}$.

Even used “informally”, I realize the urgency of getting something like Mizar’s “checker” working for Myo. It may even force me to rewrite the many-sorted term and formula modules to adopt locally nameless conventions.

Notes on Unicode

I also have written some notes on formal languages, which led me to talk a great deal about “alphabets” — a critically important concept relegated to “some countable set” in most texts. This naturally led me to talk about ASCII and Unicode, which led me to talk about the convoluted conceptual model used by Unicode.

It makes a certain kind of sense, but it’s still rather convoluted. Basically, you have some alphabet, then you convert it to “code points” (some subset of the natural numbers), then you convert it to “data units” (think of a finite sequence of integers between 0 and $U-1$), then you convert it to bytes. “It’s just that simple!”

The Unicode standard is frustrating informal, unfortunately, which led me to formalize it to some degree in my notes.

Physics

I’ve been thinking again about physics, specifically about whether there is a “suitably nice” purely Classical model of transistors and circuits. By this I mean, it works well enough for the situation we might find a Desktop computer working (temperature range 10-90 Celsius, standard air pressure, etc.).

I think this is “device physics”, but I have only heard Electrical Engineers use the phrase “device physics”.

Reading

I finished reading R.A. Salvatore’s The Halfling’s Gem Wednesday (3 June). It was pleasant enough, but I was surprised reviewers praise it as substantially different (better) than the other entries in the Icewind Dale trilogy. For myself, the writing style was consistent, and if I were not told of the author then I would have guessed Salvatore wrote it.

I’ve been reading the first Gotrek and Felix omnibus before bed. Right now, I am in the middle of Skavenslayer. “Why am I standing here half-naked and alone, facing a pack of skaven assassins? Why do these things always happen to me? This sort of thing never happened to Sigmar in the legends!”

My Mom picked up a few thick fantasy books the public Library was discarding: Terry Goodkind’s Stone of Tears (book 2 of “The Sword of Truth” series), Tad Williams’s To Green Angel Tower, and Robert Jordan’s The Shadow Rising (book 4 of the wheel of time series). I’m uncertain whether I need to read the earlier installments of Goodkind’s series (or Jordan’s Wheel of Time series) for me to make sense of these books, but at least I’ve got something to read.