Necessity that means provable

Every modal logic so far has been a proposal. Someone suggests that necessity ought to be transitive, or symmetric, and the frames tell them what they have committed to. This rung is about a logic that is not a proposal at all.

Read $\Box\varphi$ as Peano arithmetic proves $\varphi$. Then some modal formulas become true statements about arithmetic and others become false ones, and the set of formulas that come out true whatever is substituted is a specific modal logic — one that was identified, axiomatised, and proved complete.

What the reading commits to #

Two of the standard modal principles survive the reading and one famously does not.

$\Box(\varphi \to \psi) \to (\Box\varphi \to \Box\psi)$ holds: if the theory proves an implication and proves its antecedent, it proves the consequent, since the proofs can be concatenated.

The necessitation rule holds: if $\varphi$ is provable then $\Box\varphi$ is provable, because a proof of $\varphi$ can be exhibited and the theory can verify that it is one.

$\Box\varphi \to \varphi$ does not hold. It says that whatever the theory proves is true, and while that is a reasonable thing to believe about arithmetic it is not something arithmetic proves about itself — by the second incompleteness theorem, a consistent theory cannot prove its own consistency, and $\Box\bot \to \bot$ is exactly a statement of consistency.

So the logic of provability rejects the axiom every other modal logic on this ladder accepts. Necessity in this sense does not imply truth, and that is not a defect of the reading but the content of Gödel’s theorem.

Löb’s axiom #

What holds instead is stranger and stronger.

$$\Box(\Box\varphi \to \varphi) \to \Box\varphi.$$

In words: if the theory proves that provability of $\varphi$ implies $\varphi$, then the theory proves $\varphi$ outright.

Löb proved that in 1955, answering a question of Henkin’s. The proof is a diagonal argument: build a sentence asserting that if it is provable then $\varphi$, and the reasoning that follows is five lines and entirely mechanical.

The consequence worth noticing immediately is the special case $\varphi = \bot$. Löb’s axiom then reads $\Box(\Box\bot \to \bot) \to \Box\bot$: if the theory proves its own consistency, it proves a contradiction. Contrapositively, a consistent theory does not prove its own consistency, and the second incompleteness theorem is a corollary of Löb’s axiom rather than a separate result.

The frames it forces #

Löb’s axiom is not of Sahlqvist shape either, so the previous rung’s recipe does not apply, and the correspondence has to be found another way.

The answer, for finite frames, is: transitive, and with no cycles at all. The hero sweeps every relation on up to four worlds — sixty-six thousand of them — and finds the axiom valid on exactly the two hundred and forty-two that are transitive and acyclic, refusing to draw if a single frame disagrees.

Transitivity is expected, since Löb’s axiom implies $\Box\varphi \to \Box\Box\varphi$ and the sweep checks that too. The acyclicity is the surprise, and it has a sharp consequence: no world may see itself. A reflexive point is not a frame of this logic, so $\Box\varphi \to \varphi$ fails everywhere, and the sweep confirms that not one frame validates both Löb’s axiom and that one.

Read back through the arithmetic, acyclicity says the relation is provably weaker than has no loops — a theory cannot see itself, which is the reflection of the failure of $\Box\varphi \to \varphi$.

Löb’s proof, in five lines #

The argument deserves to be seen, because it is short and because it is the same diagonal move Gödel’s is, run at a different target.

Suppose the theory proves $\Box\varphi \to \varphi$. Build, by the diagonal construction, a sentence $\psi$ with $\psi \leftrightarrow (\Box\psi \to \varphi)$ — a sentence asserting that if it is provable then $\varphi$.

From that equivalence, the theory proves $\psi \to (\Box\psi \to \varphi)$. Applying necessitation and the distribution axiom gives $\Box\psi \to (\Box\Box\psi \to \Box\varphi)$. The provability predicate satisfies $\Box\psi \to \Box\Box\psi$ — a proof can be recognised as one — so this collapses to $\Box\psi \to \Box\varphi$.

Combining with the assumption $\Box\varphi \to \varphi$ gives $\Box\psi \to \varphi$. But that is the right-hand side of $\psi$’s defining equivalence, so the theory proves $\psi$; hence it proves $\Box\psi$ by necessitation; hence it proves $\varphi$.

The whole argument is four applications of rules and one diagonal sentence, and every step is available in any theory that can formalise its own proof predicate. Reading it once is the best way to see why the axiom is not an assumption about necessity but a fact about provability.

Solovay’s theorem, which is the point #

The reason this logic is different in kind from the others on the ladder is a theorem of Solovay’s from 1976.

Call the logic axiomatised by the modal $K$ axioms plus Löb’s axiom $\mathrm{GL}$. Solovay proved: a modal formula is a theorem of $\mathrm{GL}$ exactly when its arithmetical translation is provable in Peano arithmetic under every substitution.

So $\mathrm{GL}$ is not one candidate account of provability among several. It is the complete set of schematic facts about provability that arithmetic can prove, and there is nothing left over. Anything true of the provability predicate in that schematic sense is derivable from Löb’s axiom and the basic rules.

That is a very unusual thing for a modal logic to be. Every other logic in the subject is a proposal to be assessed; this one is an answer, and the question it answers was posed by Gödel.

The fixed point, and Gödel’s sentence made unique #

The most striking consequence is about self-reference, and it removes the arbitrariness from Gödel’s construction.

Gödel builds a sentence $G$ satisfying $G \leftrightarrow \neg\Box G$: it says of itself that it has no proof. The construction is a diagonal trick and it produces a sentence with that property; nothing in it says the sentence is unique or identifies what it amounts to.

The de Jongh–Sambin theorem says both. For any modal formula $A(p)$ in which $p$ occurs only inside boxes, there is a formula $F$ with no $p$ in it such that $\mathrm{GL}$ proves $F \leftrightarrow A(F)$, and it proves that any two solutions are equivalent. The fixed point exists, is unique, and is computable from $A$.

For $A(p) = \neg\Box p$ the fixed point is $\neg\Box\bot$ — the statement that the theory is consistent.

So Gödel’s sentence is provably equivalent to the consistency statement, in the theory itself. That is why the first and second incompleteness theorems are not two facts but one, and the figure checks the equivalence on every frame of the logic it sweeps, in both directions.

Checking the fixed point on frames #

The check is worth describing, because the semantic version of the identity is easy to see and the syntactic one is not.

On a finite transitive acyclic frame, $\Box\bot$ holds at a world exactly when it has no successors — vacuously, since there is nothing to check. So $\neg\Box\bot$ says this world sees something.

And $\Box\neg\Box\bot$ says every successor sees something. On a finite acyclic frame, a world with any successors has a maximal one, which sees nothing; so $\Box\neg\Box\bot$ is false whenever the world has successors, and vacuously true when it has none.

Therefore $\neg\Box\neg\Box\bot$ is true exactly when the world has successors, which is exactly when $\neg\Box\bot$ is. The two are equivalent, on every frame of the logic and only there — a reflexive point breaks it, and the sweep confirms the equivalence fails off the logic’s frames.

Finiteness and acyclicity are both doing work in that argument, and their arithmetic reading is that proofs are finite objects and a theory cannot prove things about itself for free. The finiteness is the same hypothesis an infinite tree’s path is about, used in the opposite direction: there the interest is that infinite branches exist, here it is that on an acyclic finite frame every branch stops.

Reading a frame as a theory #

The correspondence is more vivid with the arithmetic put back in, and it is worth doing once even loosely.

Think of the worlds as theories and an arrow from $w$ to $v$ as $v$ is one step weaker in proof strength — $w$ can prove things about $v$’s proofs. Transitivity says that relation composes. Acyclicity says no theory reaches back to itself, which is the statement that a theory cannot prove its own consistency.

A dead end is a world where $\Box\bot$ holds vacuously: a theory that proves everything, or from whose position nothing further is visible. On a finite acyclic frame every path reaches one, which is the statement that the tower of reflections is well-founded.

Then $\neg\Box\bot$ at a world says the world is not such a dead end — consistency — and the fixed-point computation above says a world’s own Gödel sentence is exactly that assertion. The frames are a picture of theories reflecting on weaker theories, and the picture is finite and terminates, which is the whole difference from the reflexive frames of every other modal logic.

That reading is a heuristic and not the theorem. Solovay’s proof does construct, for a given finite frame, an assignment of arithmetical sentences to worlds behaving as the frame says — so the picture is closer to literal than most such readings — but the construction is intricate and nothing in a diagram displays it.

Why the logic is decidable and arithmetic is not #

A tension worth resolving, since the two facts sit oddly together.

Arithmetic’s set of theorems is not decidable — that is the other half of Gödel’s work. Yet $\mathrm{GL}$, which describes what arithmetic proves about its own proofs, is decidable: there is a procedure that settles whether a modal formula is a theorem.

The resolution is that $\mathrm{GL}$ describes only the schematic facts, the ones holding under every substitution. Deciding whether a particular arithmetical sentence is provable is undecidable; deciding whether a modal formula’s translation is provable whatever is substituted is a much coarser question, and coarse enough to be answered.

$\mathrm{GL}$ has the finite model property — every non-theorem is refuted on a finite transitive acyclic frame, whose size is bounded by the formula’s — so the decision procedure is the one the canonical construction supplies: enumerate small frames and check.

That the logic has the finite model property while its canonical model does not is the standard curiosity here. The canonical model of $\mathrm{GL}$ has infinite ascending chains and so is not a frame of the logic at all, which is why completeness for it needs the finite construction rather than the classical one.

What the reading does not cover #

Three qualifications, since the logic of provability is a phrase that invites over-reading.

It is schematic. $\mathrm{GL}$ says what holds under every substitution. Individual sentences can be provable without their modal shape being a theorem, and nothing here identifies which.

It is about one theory at a time. The translation fixes Peano arithmetic, or any theory with enough arithmetic to formalise its own proof predicate. A theory too weak to talk about its own proofs has no such logic.

And the box is a specific predicate. The results depend on the provability predicate satisfying the Hilbert–Bernays conditions, and a badly chosen predicate — one that describes proofs in an unnatural encoding — can fail them and make Löb’s axiom false. Rosser’s variant provability predicate is the standard example, and its logic is different.

Where the axiom came from #

The chronology has a pleasing shape: the axiom was found as an answer to a question that was expected to go the other way.

Henkin asked in 1952 what happens to a sentence asserting its own provability — the opposite of Gödel’s. Is it true? Is it provable? The natural guess is that it is undecidable, by analogy.

Löb answered in 1955 that it is provable, and the proof is the argument above with $\varphi$ taken to be the sentence itself. So Henkin’s sentence is a theorem, and Gödel’s is not, and the asymmetry between a sentence asserting its own provability and one denying it is total.

What Löb actually established was the general schema, which he stated because his proof gave it. The recognition that the schema is a modal axiom, and that the modal logic it generates is the whole story, took another twenty years — Segerberg proved completeness for the frames in 1971, and Solovay’s arithmetical completeness came in 1976.

A question about one self-referential sentence produced an axiom, which produced a logic, which turned out to be complete for a subject. That is an unusually good return, and it is the reason this rung exists: the object it describes was not designed, it was discovered by asking a small question carefully.

What the pictures cannot show #

The arithmetic is not there. Every frame in the figure is a diagram of worlds and arrows, and the theorem making them interesting is Solovay’s, which relates them to Peano arithmetic. Nothing in a graph mentions arithmetic.

The sweep is over frames of at most four worlds. The correspondence between Löb’s axiom and transitivity-with-no-cycles is checked exhaustively there and stated for all finite frames. The infinite case is genuinely different, and the canonical model is the place it bites.

And the fixed point is checked and not derived. The generator verifies the equivalence between $\neg\Box\bot$ and its own box-image on every frame of the logic it sweeps. That the fixed point is unique, and computable from the formula, is de Jongh and Sambin’s theorem and is syntactic.

Where the ladder goes next #

This closes the ladder. It began with an operator whose axioms were a matter of taste, settled by asking which diagrams they held on; it ends with one whose axioms are not a matter of taste at all, because the operator has a fixed meaning and the axioms are the complete list of what is true of it.

What is left unwritten belongs to other anchors. The interpretability logics, which read the box as interprets rather than proves, are a family with the same shape and different frames. Bimodal provability logics compare two theories. And the arithmetical hierarchy that the translation’s complexity lives in is a subject of its own. Sideways: the sentence that says it has no proof is the construction this rung makes unique, and the axiom no property of the arrows defines is the other non-Sahlqvist axiom on the ladder.

The other readings of the box #

Provability is not the only interpretation with an exact answer, and naming a couple makes the shape of the achievement clearer.

Read the box as is true in every extension of the current theory by finitely many axioms of a stated kind, and a different but related logic appears. Read it as is interpretable in, and the interpretability logics arrive, with their own axioms and their own frames.

What those readings share with this one is that they are not proposals. Each fixes a mathematical relation, asks which modal schemata hold of it, and gets an answer that is a specific logic — sometimes known completely, sometimes not.

A modal logic with an interpretation of that kind is a description; one without is a stipulation. Almost all of them are stipulations, which is why the subject looks like a taxonomy of possible opinions, and why the few that are descriptions are worth singling out.

What is worth carrying away #

A formalism invented to model an intuition can turn out to describe something exactly, and when it does the status of the whole enterprise changes.

Modal logic was invented to say what necessity means, which is a question philosophers had been arguing about without a way to settle anything. Reading the box as provability turns the question into mathematics: there is a fact of the matter about which schemata arithmetic proves, and Solovay’s theorem says it is $\mathrm{GL}$.

There is a companion lesson about proof systems generally. A logic is normally judged by whether its theorems match an intuition, which is an argument nobody wins. A logic with an arithmetical completeness theorem is judged against a set of facts, and a system’s limits about itself turn out to be exactly the facts in question.

The move worth carrying is that giving a contested notion a mathematical home is what turns disagreement into computation. The first rung of this ladder made that point about frames and axioms; this one makes it about a case where the home turned out to be occupied already.