No table of truth values is enough

Classical propositional logic is decided by a table with two values in it. Each connective is a function on the two values, a formula is a tautology when it comes out true at every row, and the tautologies are exactly the theorems. The table is the logic, in the most complete sense possible: a finite object, checked mechanically, that says yes to the theorems and no to everything else.

The constructive system is decidable too, by a search through finite algebras. The natural question, which Łukasiewicz and others had already made concrete with three-valued tables, is whether that search could be replaced by a single table — some finite list of truth values, some functions for the connectives, whose tautologies are exactly the constructive theorems. Gödel answered it in 1932, in a note of about a page. The answer is no, and the proof is a pigeonhole.

The formula that counts #

Take $m$ statement letters $p_1, \dots, p_m$ and write the disjunction, over every pair, of their equivalences:

$$G_m \;=\; \bigvee_{i < j} \,(p_i \leftrightarrow p_j).$$

It says that some two of the $m$ statements are equivalent. Classically it is a tautology as soon as $m \ge 3$, since three statements with only two truth values must repeat one. Constructively it is a much stronger claim, and the constructive system does not prove it for any $m$.

Now suppose some table with $n$ values characterised the constructive system. Give the letters of $G_{n+1}$ any values at all. There are $n + 1$ letters and $n$ values, so some two letters get the same value, and for those two $p_i \leftrightarrow p_j$ is equivalent to $p_i \leftrightarrow p_i$, which is a constructive theorem and so comes out designated in the table. A disjunction with a designated disjunct is designated too — the table has to respect the theorem $A \to A \vee B$ and modus ponens. So $G_{n+1}$ comes out designated at every row, and the table would declare it a theorem. It is not one. So no $n$ works.

The argument needs one thing checked, and it is where the chains come in: that $G_{n+1}$ really is not a constructive theorem. For that it is enough to exhibit one Heyting algebra refuting it, and the chains of truth values provide one for every $n$.

One refutation, pair by pair #

A chain of $n$ truth values is the list $0 < 1 < \dots < n-1$ with the constructive connectives: “and” is the smaller value, “or” the larger, $a \to b$ is the top value when $a \le b$ and is $b$ otherwise, and $\neg a$ is $a \to 0$. The two-element chain is the classical table; the longer ones are Heyting algebras in which some statements are neither true nor false but partially established, in a linear order of how far.

In a chain, $a \leftrightarrow b$ is the top when $a = b$ and the smaller of the two values otherwise: if $a < b$ then $a \to b$ is the top and $b \to a$ is $a$, and their meet is $a$. Give the $n$ letters of $G_n$ the $n$ distinct values of the $n$-chain, and every equivalence takes the value of its lower letter. The largest of those is the second-highest value, from the top two letters, and the disjunction is exactly that. It is not the top, so $G_n$ fails in the $n$-chain.

That is the whole of Gödel’s argument: the $n$-chain refutes $G_n$, so no $G_m$ is a constructive theorem, while every $n$-valued table validates $G_{n+1}$. No finite table can tell the constructive theorems from $G_{n+1}$.

The pigeonhole here is the ordinary one — more letters than values forces a repeat — used in an unusual direction. It is not deciding a question about objects; it is showing that a finite set of values cannot hold a logic that refuses to count.

The same refutation as stages of knowledge #

The chains have a second reading, in the stages-of-knowledge models the constructive system was first drawn with. A model whose stages form a single line of $k$ stages has exactly $k + 1$ possible truth sets for a statement: known from the first stage, known from the second, …, known from the last, or never known. Those are ordered by how early the statement becomes known, and the algebra they form is the $(k+1)$-chain. So a chain of truth values is a line of stages seen from above, and a value is the moment a statement is learned.

In that reading the refutation of $G_n$ is a story. There are $n - 1$ stages in a row, and the $n$ letters are learned at $n$ different times — one at the first stage, one at the second, and so on, with one never learned at all. At the first stage no two of them are equivalent: for any pair, a later stage knows one and not the other, so neither implies the other there. The disjunction of their equivalences is not forced at the start. It becomes forced only at the last stage, where every letter that will ever be learned has been, and then the ones known agree with each other.

That is why the formula fails in the constructive system and yet holds in any table short enough. A chain with $n$ values is a line with $n - 1$ stages, and $n + 1$ letters cannot all be learned at different moments on it; two must be learned together, and from the start they are equivalent. What the constructive system refuses is a bound on how many different moments there are.

The reading also explains which axioms the chains share. Linearity says that of two statements one is learned no later than the other, which is true on any line. A modal axiom is a condition on the shape of the frame, and so is this one: it holds exactly on the frames that are lines.

What each chain adds #

Every chain is a Heyting algebra, so every chain’s logic contains the constructive system. The chains are not all alike, and a table of formulas against chain length shows where each one gives way.

Three of the rows are the classical laws the constructive system rejects, and each fails as soon as there is a middle value: set $p$ to it, and $p \vee \neg p$ is the middle value, $\neg\neg p$ is the top while $p$ is not, and Peirce’s law falls short in the same way. The three-chain is the smallest algebra that is not classical, and it already refutes all of them.

The fourth row is more interesting. $p \vee (p \to q) \vee \neg q$ survives three values and fails at four. In three values, if $p$ is not the top then either $p \le q$ — making $p \to q$ the top — or $q$ is below $p$ and hence is $0$, making $\neg q$ the top. With four values there is room for $0 < q < p < 3$, and nothing in the disjunction reaches the top. So the logic of the three-chain proves a formula the four-chain does not, and the two logics differ.

The last two rows are the constant ones. The weak law and the linearity axiom fail in no chain, because a chain has one top and no two incomparable elements. Those are exactly the two axioms whose frames could not be glued — linearity forbids the fork and the weak law forbids two final stages — and a chain is the shape that has neither.

An infinite descent #

The chains fit together in a specific way. Merge the top two values of the $(n+1)$-chain and the result is the $n$-chain, and the merge commutes with every connective — the figure checks it for implication, the only one where it could go wrong. A formula refuted in the shorter chain is therefore refuted in the longer one, since a refuting valuation lifts back. So the logic of each chain contains the logic of the next, and $G_{n+1}$, true in the $n$-chain and false in the $(n+1)$-chain, shows that each containment is strict.

At the top of the descent is the two-chain, whose logic is classical. Next is the three-chain, whose logic is the one immediately below classical logic in the whole continuum of logics between the two. The descent then goes on without end. What every chain validates, the intersection of all their logics, is Gödel–Dummett logic: the constructive system plus linearity, $(p \to q) \vee (q \to p)$. Dummett proved in 1959 that this is exactly the logic of all finite chains, and exactly the logic of a single infinite one.

Below Gödel–Dummett logic there is still a gap to the constructive system, and it is the linearity axiom that marks it: the constructive system does not prove linearity, and every chain does. Gödel’s formulas cannot see this gap, since they fail in every sufficiently long chain as well as in the constructive system. Only a shape that is not a chain — a fork — separates the two.

The interval from 0 to 1 #

The infinite chain in Dummett’s theorem can be taken to be the real interval $[0, 1]$, with the same connectives: “and” the minimum, “or” the maximum, $a \to b$ equal to $1$ when $a \le b$ and to $b$ otherwise. This is a many-valued logic in the most literal sense — a truth value for every real number between false and true — and its tautologies are exactly Gödel–Dummett logic.

The picture compares Gödel’s implication with the other famous one on the same interval, Łukasiewicz’s, where $a \to b$ is $\min(1, 1 - a + b)$. Both are $1$ whenever $a \le b$, which is why both make every instance of linearity true. They differ only below the diagonal, and the difference is large. Gödel’s implication jumps: as soon as $a$ exceeds $b$, the value is $b$, however slightly $a$ exceeds it. Łukasiewicz’s is continuous, sliding down to $1 - a + b$.

The continuity costs the Łukasiewicz interval its place among the constructive logics. It refutes contraction, $(p \to (p \to q)) \to (p \to q)$ — using a hypothesis twice is no better than using it once — which the constructive system proves. At $p = 0.5$ and $q = 0$ the formula takes the value $0.5$. So Łukasiewicz’s logic is not an intermediate logic at all; it is a different kind of logic, in which a hypothesis is a resource that can be used up. Gödel’s jump is what keeps contraction true: $p \to (p \to q)$ and $p \to q$ are always equal under his rule.

Two three-valued tables that disagree #

Gödel’s note answered a question that three-valued tables had already made pressing. Łukasiewicz had introduced a three-valued logic in 1920, for statements about the future that are not yet settled, and Heyting’s formalisation of the constructive system a decade later came with its own three-valued table. The two agree on “and”, “or” and on every implication between the classical values. They disagree at one entry: the value of $\tfrac12 \to 0$.

Łukasiewicz set it to $\tfrac12$, which is the three-valued slice of the interval picture above: $1 - a + b$ with $a = \tfrac12$ and $b = 0$. Heyting’s table sets it to $0$, which is Gödel’s rule — below the diagonal, the value is $b$. One entry, and the two tables belong to different kinds of logic: Heyting’s three values are the three-chain, a Heyting algebra whose logic lies just below the classical one, and Łukasiewicz’s three values refute contraction already, since with $p = \tfrac12$ and $q = 0$ the implication $p \to (p \to q)$ is $1$ while $p \to q$ is $\tfrac12$.

Heyting’s three-valued table validates every constructive theorem and refutes excluded middle, which was enough to show the two logics are different. What it could not do was capture the constructive system exactly, since it also validates $G_4$ and $p \vee (p \to q) \vee \neg q$. Gödel’s question was whether any longer table could, and the answer was that each longer chain fixes the previous one’s excess and adds its own.

Why the pigeonhole cannot be dodged #

It is tempting to think a cleverer table might escape the argument — one whose values are not a chain, or whose connectives are not those of a Heyting algebra, or in which several values count as true. None of these helps, and the reason is how little the argument used.

It used that $p \leftrightarrow p$ comes out designated, which any table for the constructive system must arrange, since it is a theorem. It used that a disjunction with a designated disjunct is designated, which follows from the theorem $A \to A \vee B$ and closure under modus ponens. And it used that the table has $n$ values. Nothing about order, about chains or about algebraic structure entered the direction that matters. The chains are needed only to show $G_m$ is not a theorem; the pigeonhole alone shows every finite table validates one of them.

What the argument leaves open is an infinite table, or a family of finite ones. Both work. The constructive system is the logic of all finite Heyting algebras together, which is the finite model property again, and Jaśkowski gave an explicit sequence of finite algebras in 1936 whose common logic is exactly the constructive system. What does not exist is one finite algebra that does the job alone.

What the pictures cannot show #

The staircase is drawn to six values and seven letters. The pattern — $G_m$ holds in the $n$-chain exactly when $m > n$ — is proved for all $n$ by the pigeonhole and the pair-by-pair refutation, and the figure checks the finite piece of it. It does not check a chain of a thousand values.

Dummett’s theorem is quoted, not drawn. That Gödel–Dummett logic is exactly the logic of all finite chains is a completeness theorem; the figures show chains validating linearity and never refuting it, which is the easy half. That every non-theorem of the logic fails in some finite chain — so that nothing beyond linearity is shared — is the hard half, and it is not on the page.

The interval is sampled. The two panels are grids of values and the contraction check runs on a grid of twenty-one points each way. The functions themselves are defined everywhere and the check is a statement about them; the drawings are pictures of two formulas, not proofs about uncountably many truth values.

Still open: the continuous side #

The chains close the story on their own side. The logics above Gödel–Dummett logic are known completely — they are the logics of the finite chains and nothing else, a single descending sequence with the classical logic at its head — and each is decided by its own finite table. That is a rare situation among these logics, most of whose families are far wilder.

The other interval is less tame. Łukasiewicz’s logic on $[0, 1]$ has its own completeness theorem and its own characterisation, McNaughton’s, which says exactly which functions of the truth values its formulas can define: the continuous ones built from finitely many linear pieces with integer coefficients. Why those functions and not others, and what the logic’s many-valued tables look like between the finite ones and the interval, is a subject with a structure of its own — and one in which the pigeonhole that closed this page plays no part at all, because in Łukasiewicz’s logic $p \leftrightarrow p$ is still true but using it twice is not free.

A table that refuses to count #

Two truth values fit classical logic because classical logic is willing to count: with two values, three statements must repeat one, and classical logic proves that. The constructive system refuses to prove it for any number of statements. Every finite table counts, whether it means to or not, since the pigeonhole applies to anything finite. So no finite table can hold a logic that will not count.

The chains are what the refusal looks like when it is made concrete. Each finite chain counts up to its own length and no further, and the constructive system sits below all of them, refusing every $G_m$. A logic defined by what it will not prove turns out to need infinitely many truth values — not because it proves anything elaborate, but because it withholds something that every finite table would have to grant.