The second letter breaks the pattern

Classically, a formula in $n$ letters is a function from the $2^n$ ways the letters can turn out to true or false, so there are $2^{2^n}$ of them up to equivalence: four in one letter, sixteen in two, 256 in three. That is the whole content of a formula as a corner of a cube, and it makes the classical count finite at every size.

The constructive system is different from the first letter. Refutable in something small recorded Rieger and Nishimura’s theorem — infinitely many inequivalent formulas in the single letter $p$, arranged in a lattice with a three-line description — and ended on a sentence it did not pursue: in two letters the lattice is infinite, has no comparably explicit description, and is a subject in its own right.

This essay measures why. The instrument is a single model built so that it tells apart every pair of formulas that can be told apart at all, and the measurement is how many formulas it separates as it grows one step at a time. In one letter the answer is four more at every step. In two letters it is sixteen, then 265,454, then a number with eighty thousand digits.

A formula is a set of states that only grows #

The constructive reading of logic is a reading about knowledge that accumulates. A Kripke model is a set of states of knowledge with an order saying which states can develop into which, and with each letter marked as established at some states. Once a letter is established it stays established, so the marked states are closed upwards: if $p$ holds at a state it holds at every state that state can become.

The connectives are read the same way. A conjunction holds where both parts hold, and a disjunction where one part does. An implication $A \to B$ holds at a state when, at every later state where $A$ comes to hold, $B$ holds too, and negation $\neg A$ is $A \to \bot$: no later state ever establishes $A$. Excluded middle fails at any state that has not yet decided $p$ but could still go either way, which is the counterexample a proof that says which half uses.

The consequence that matters here is that every formula, read at every state, also holds at every later one. So a formula’s truth set is an up-set — a set of states closed under moving later — and two formulas are equivalent in a model exactly when their up-sets coincide. The up-sets of any order themselves form a Heyting algebra, which is how every finite one arises, so a Kripke model is an algebra of truth values drawn as a picture of time.

The model drawn is one that logicians call universal, and it is built rather than chosen. At the top are the final states: for one letter there are two, one where $p$ has been established and one where it never will be. Every lower layer adds each state that could possibly precede the layers already built — a state that can become exactly some collection of incomparable later states, with the letters it has already established, which must be among those all of its later states share — except the ones that would only copy an existing state, such as a state whose sole future is a single other state with the same letters. A copy is a state no formula could distinguish from its original — the relation two diagrams the language cannot tell apart calls a bisimulation — and leaving copies out is what keeps the model from counting one formula twice.

That rule leaves exactly the states that make a difference. A formula that can be refuted at all can be refuted at a state of the universal model, because the finite model property produces a finite countermodel and every finite model collapses onto a piece of the universal one. So counting the up-sets of the universal model, layer by layer, counts the formulas that states of that depth can tell apart, provided every up-set is the truth set of some formula. For one letter the figures check that it is, by building formulas until every up-set has one.

One letter: two new states and four new formulas a step #

For one letter the universal model grows slowly. Every layer has exactly two states, and the computation checks it to eight layers: the antichains that can sit above a new state, with the letters it could carry, produce two states that are not copies at every step and no more.

So the formulas grow slowly too. States at most $D$ steps from final tell apart exactly $4D$ formulas: four at the last step, which are the four classical ones, $\bot$, $p$, $\neg p$ and $\top$; eight one step back; and four more at every step after that. The formulas told apart at depth $D$ are also told apart at every greater depth, so the counts nest, and the whole lattice is their union.

The new formulas are the classically trivial ones that the constructive system refuses to identify. The first step back adds $p \vee \neg p$, which is classically $\top$ and here is not; $\neg\neg p$, classically $p$; $\neg\neg p \to p$, classically $\top$; and $\neg p \vee \neg\neg p$, classically $\top$ again. Each later step adds two more pairs built out of the pair before, and the order among them — which implies which — is the column in the figure.

That column is the Rieger–Nishimura lattice. Its levels are pairs of incomparable formulas, each one either the disjunction of the two just beneath it or an implication whose conclusion lies beneath it, and every level is strictly above the last, so the lattice never closes. Classical logic folds the whole of it onto four points, and the folding is exactly what adding excluded middle does — the axiom that the middle that is not excluded drops, put back, identifying every level with one of the four classical formulas.

What makes it a column rather than a tangle is the slow growth of the model. Two new states a step give the formulas only a few new ways to differ, and four new formulas a step is all those ways amount to.

Each level costs Fibonacci numbers of symbols #

The lattice is infinite, and the formulas in it get long. Counting every letter, every $\bot$ and every connective, and writing $\neg A$ as $A \to \bot$, the shortest formulas for the truth sets in order run 1, 1, 3, 3, 5, 5, 7, 9, 13, 13, 21, 23, 37, 37, 59, 61, 97, 97, 157 and on, reaching 2,857 symbols by the thirty-second.

The reason is in the description of the levels. A formula on a new level is a disjunction or an implication of formulas on the two levels below, and its length is their lengths added together, plus one for the connective. That is the Fibonacci recursion with a constant thrown in — $37 + 59 + 1 = 97$, $59 + 97 + 1 = 157$ — and the ratio from one formula to the formula two places on settles on $1.6176$ by the end of the range, against the golden ratio’s $1.6180$.

So the $k$-th level needs a formula whose length grows like the golden ratio to the power $k$. Nothing more efficient is available: the lengths are minimal over every formula the search built, at every depth it ran to, so a shorter formula for a level would have to be one that differs from it only at states deeper than eight steps.

This is also why the classical count is a surprise rather than a convenience. A classical formula in one letter needs at most three symbols to name — $p \to \bot$ is the longest — and the reason is that there are only four things to name. The constructive system has infinitely many things to name in the same letter, and naming them costs exponentially many symbols in their height in the lattice, which is what an infinite set of objects described by a two-term recurrence has to cost.

Two letters: eighteen states one step from the end #

The second letter changes the first layer. There are four final states rather than two — both letters established, only $p$, only $q$, neither — and at the final layer alone the model tells apart sixteen formulas, which are exactly the sixteen classical ones.

The second layer is where it stops resembling the first. A state one step from final sits below a non-empty set of final states, any set at all since final states are incomparable, and it can have established only the letters that every one of those final states shares. Counting by hand:

• below a single final state, a state must establish strictly less than that state does, or it would be a copy: none below the state with neither letter, one below each of the two states with one letter, three below the state with both, five in all;
• below two final states, the shared letters are the intersection: eight states over the six pairs;
• below three, four states; below all four, one.

That is eighteen, and the figure at the top of the essay draws them with the lines to their futures. The twenty-two states together have 265,454 up-sets, counted by the computation exactly; at the same depth one letter has eight.

The count is only a count of formulas if every one of those up-sets is a truth set, and that is a theorem of Dick de Jongh’s from 1968: for every state of finite depth in the universal model there is a formula true exactly at that state and the states after it, so every up-set — a union of finitely many such sets — is a disjunction of them. The computation checks the theorem at this depth rather than quoting it. Starting from $\bot$, $p$ and $q$ and combining everything with everything under the three connectives, the up-set above each of the twenty-two states appears by the fifth round: one of them at the first, six by the second, twelve by the third, nineteen by the fourth and the last three at the fifth.

So 265,454 inequivalent formulas in two letters are told apart by states at most one step from final, and every one of them is classically one of sixteen. The ratio is a measure of how much the second letter’s states can disagree with each other about the future.

The third step is past writing down #

The third layer is where the size runs away, and the reason can be read off the construction. A new state is placed below an antichain of the states already built, so the number of new states is roughly the number of antichains of the model above. But antichains and up-sets are the same thing counted twice — every up-set is determined by its lowest states, and those form an antichain — so the number of antichains is the number of up-sets, which is the number of formulas the layer above told apart.

So each layer of the model is about as large as the count of formulas at the layer before, and the formulas at the next layer number at least two to that. For two letters the computation builds the third layer state by state and finds 265,428 new states, twenty-six short of the 265,454 up-sets above it because some antichains have no valuation that is not a copy. Any selection of those new states, together with everything above them, is an up-set, so the third depth tells apart more than $2^{265{,}428}$ formulas — a number with 79,902 digits.

Three letters reach the same wall a step sooner. The final layer has eight states and 256 formulas, the second layer has 302 states, and so the second depth already separates more than $2^{302}$ formulas, while the third layer’s states are at least as many as the subsets of those 302, which puts the third depth’s count beyond $2^{2^{301}}$.

One letter escapes because its antichains are few. With two states a layer, the antichains that reach the newest layer and carry a valuation that is not a copy come to exactly two at every step — the computation confirms it to eight — so the model never thickens and the formulas cannot multiply. The second letter is enough to break that: the first layer already has four incomparable states, so the second already has eighteen, and from there each layer feeds the next an exponential.

Why nobody has drawn the two-letter lattice #

The objects being counted are the elements of the free Heyting algebra on one or two generators: the algebra of all formulas in those letters, with equivalent formulas identified. On one generator it is the Rieger–Nishimura lattice, and a column two wide can be drawn. On two, the counts above say what any drawing would have to contain.

Not just more elements but more shape. The column works because every layer of the one-letter model adds the same two kinds of state, so the formulas repeat a pattern; in two letters each layer is built from the up-sets of the previous one, and the up-sets of a model with 265,454 of them do not repeat any pattern that a description of the layer above would give. The lattice at each depth is the lattice of up-sets of an order that is itself made of the previous lattice, which is a recursion that describes the object and does not simplify it.

None of this makes the logic intractable in the sense that matters for proofs. Deciding whether two formulas are equivalent is still a finite search, because the finite model property bounds the depth that has to be checked by the size of the formulas — two formulas of a hundred symbols, if they differ at all, differ at a state no deeper than the number of their subformulas plus one, since along any chain of states in a collapsed countermodel the set of true subformulas only grows, and strictly. What is hopeless is the global picture, not the local question.

There is a classical shadow of the same growth, and it is Dedekind’s problem of counting antichains in the cube of subsets, where the counts also run away doubly exponentially and have no closed form. The two-letter Heyting algebra is that problem iterated: each layer asks Dedekind’s question of the layer above.

Chains: the logic where the count stops #

The runaway has a precise cause, the states that can still become several incomparable futures, and removing them removes it. In the logic of Gödel and Dummett, where of any two statements one implies the other, the models are chains: every state has at most one next state. Michael Dummett axiomatised it in 1959 as the logic of Gödel’s chains of truth values, and Alfred Horn proved in 1969 that its algebras are locally finite: finitely many letters give only finitely many formulas.

The figure shows why. A chain state must establish strictly fewer letters than the state after it, or it would be a copy, so a chain in $n$ letters is at most $n + 1$ states long. For one letter that leaves three states — the two final ones and one below the state where $p$ holds — and six up-sets, the six formulas $\bot$, $p$, $\neg p$, $\neg\neg p$, $p \vee \neg p$ and $\top$ that this logic can tell apart. For two letters it leaves eleven states in four trees, and the trees have 342 up-sets.

The computation reaches 342 two ways. The up-sets of a forest multiply over its trees, and each tree’s count is one more than the product over its branches, which gives 342 in a line. Independently, closing $\bot$, $p$ and $q$ under the three connectives on those eleven states finds exactly 342 distinct truth sets and stops. Three letters give 137,186,159,382 — large, but a number and not a tower, and every further letter gives another.

So the one-letter column and the two-letter explosion are a single phenomenon. The column stops at six in this logic for the same reason the explosion stops at 342: without branching futures, the model is finite for every number of letters, and a finite model has finitely many up-sets.

What the counts are and are not #

Each number here is a computation and each carries an assumption that is worth stating.

The one-letter counts are exact to depth eight, and the identification of up-sets with formulas is checked rather than assumed: closing $\bot$ and $p$ under the connectives reaches exactly $4D$ truth sets at each depth, which is the number of up-sets. The formula lengths are minimal among the formulas the closure built, which is every combination of shorter classes, so they are true minima for distinguishing the truth sets at depth eight.

The two-letter count at depth two is an exact count of up-sets, 265,454, and de Jongh’s theorem is checked at that depth by reaching each of the twenty-two principal up-sets with a formula. The third-layer figure of 265,428 states is exact; the formula count it implies is a lower bound, and a very loose one, since it counts only the up-sets that contain all of the second layer.

The Gödel–Dummett counts rest on Dummett’s theorem that chains suffice for his logic, and on the forest being the right reduction of chain models, which the second computation corroborates by finding the same 342 from the formulas themselves.

Still open: how many short formulas there are #

The counts above group formulas by the depth of the states needed to tell them apart. The natural alternative is to group them by length: how many inequivalent two-letter formulas have at most $s$ symbols. In one letter the answer follows from the lattice, since the levels’ lengths grow like powers of the golden ratio, so there are about $2 \log_\varphi s$ classes of length at most $s$.

In two letters the depth counts say only that the number is eventually enormous, and that long formulas are needed to reach the deep layers. Which formulas of moderate length are equivalent, and how fast the count of classes grows with length, is the question a census of the free Heyting algebra on two generators would answer. A computation of the kind behind these figures can carry it some distance, and the doubly exponential growth of the layers is exactly what limits how far.