The Law

Let □φ abbreviate the arithmetical sentence Prov_T(⌜φ⌝) — “T proves φ.” For any theory T extending elementary arithmetic EA and recursively axiomatized, this operator satisfies three conditions, isolated by Hilbert, Bernays, and Löb. They are the only facts about provability the rest of this study will use.

Read these as modal axioms and they are an exactly familiar system. D1 is the rule of necessitation. D2 is the distribution axiom K. D3 is the transitivity axiom 4. Together they are the modal logic K4 — no more, no less.

In 1952 Leon Henkin posed a question dual to Gödel's. Gödel's sentence says “I am not provable” and is, in a consistent theory, unprovable and true. What of the sentence H that says “I am provable” — a fixed point of □p, so that T ⊢ H ↔ □H? Is it true? Is it provable? Nothing about its self-referential form decides the matter; both answers seemed initially consistent.

Martin Löb (1955) settled it, and the settlement was far more general than the question. He proved that the only way a theory can prove “if φ is provable then φ” is the trivial way — by proving φ outright.

The proof is the diagonal again — one application of the fixed-point lemma, then the derivability conditions doing all the rest. It is short enough to give in full.

Henkin, answered  Apply Löb to the Henkin sentence. H ↔ □H gives T ⊢ □H → H directly (it is half of the biconditional), so Löb yields T ⊢ H: the sentence claiming its own provability is provable, hence true. Henkin's sentence is not delicately balanced after all — it is forced all the way to ⊤. The self-affirming twin of the Gödel sentence simply asserts a truth.

Gödel-2, contained  Now set φ = ⊥. The hypothesis □⊥ → ⊥ is exactly ¬□⊥ — that is, Con(T). Löb's theorem then reads: if T ⊢ Con(T) then T ⊢ ⊥ — a consistent theory cannot prove its own consistency. Gödel's second incompleteness theorem is not analogous to Löb's theorem; it is Löb's theorem, evaluated at the single point ⊥. Everything the ladder is built from is one instance of this one law.

A Kripke frame is a set of worlds W with an accessibility relation R. A formula is forced at a world by the usual clauses, with the modal one reading: □φ holds at w iff φ holds at every world w can see. The miracle of GL is that its theorems are exactly the formulas that survive on a very particular class of frames.

That last clause is the first marvel of the subject, and worth pausing on. Arithmetical provability is Σ₁-complete — undecidable, the very engine of Gödel's theorem. Yet the logic of that undecidable operator is decidable: a finite algorithm settles which modal schemata hold of provability. The complexity collapses on the way from the predicate to its laws.

why soundness fails, visibly  On a frame with irreflexive worlds the soundness axiom □p → p simply breaks. Take a world that sees nothing — a leaf. There, □p is vacuously true (it sees no world where p fails), so if p is false at the leaf, □p → p is false. The frame is a countermodel to reflection — the modal echo of the fact that PA cannot prove □p→p. Meanwhile Löb's own axiom holds at every world no matter how you assign p. Refute the one, confirm the other, on a fixed frame:

The arithmetical diagonal lemma says: for any A(x) there exists a sentence G with T ⊢ G ↔ A(⌜G⌝). It gives existence and nothing more — no uniqueness, no canonical form. Its modal counterpart is sharper on both counts.

The algorithm is the one the law makes converge: substitute A into itself, starting from ⊤, and the box-guard means each round pins down one more layer of modal depth — which on GL's finite-depth frames must stabilize. Watch it land, on four sentences each of independent interest:

the guarded reading  Why must a box-guarded definition have a unique solution at all? The deepest modern answer comes from computer science. The provability box and the “later” modality ▷ of guarded recursion obey the very same law — Löb's — and under that law a guarded recursive definition has a unique fixed point, computed as the limit of its finite approximations (Nakano; the topos-of-trees semantics of Birkedal and others). The two modalities are not identical — one is provability, one is a step of computation — but they share the axiom, and the axiom is what guarantees the limit exists and is one. The de Jongh–Sambin fixed point and the guarded recursive fixed point are the same construction under the same law.

Make the connection to arithmetic precise. An arithmetical realization ∗ assigns to each modal variable a sentence of arithmetic, extends to connectives in the obvious way, and translates the box by provability: (□ψ)∗ = Prov_PA(⌜ψ∗⌝). Call a modal formula φ arithmetically valid if PA ⊢ φ∗ for every realization. The soundness direction we already have in hand — each axiom of GL translates to a theorem of PA (the derivability conditions give K4; the formalized Löb theorem of §II gives the Löb axiom). The depth is all in the converse.

the construction  To prove the converse one shows: if GL ⊬ φ, some realization makes φ∗ unprovable. Solovay's method is to take a finite Kripke countermodel for φ — a finite transitive irreflexive tree whose root refuses φ, which §III guarantees exists — and embed it into arithmetic. The embedding is a function, and the function is built by the diagonal.

Adjoin a new bottom node to the countermodel so the whole tree has a single root the climb can start from. Now define a primitive recursive function h : ℕ → W, the Solovay function, that walks up the tree: h(0) is the root, and h steps from a world i to an accessible successor j exactly when a proof appears that the walk's own eventual limit does not lie outside the subtree above j. That definition refers to the limit of the very function being defined — so it is legitimized, as ever, by the recursion theorem: Gödel's fixed-point lemma, used here not to build a sentence but to build a process.

The shape of this is worth dwelling on. The diagonal argument that limits the theory from within — Gödel's — is here the very tool that builds a faithful arithmetical copy of an abstract model. The same fixed-point construction that forbids the summit constructs the bridge. Provability is undecidable; its logic, by this construction, is laid out in full and decided by machine.

a question §IV could not answer, now answered  Transporting the modal facts back through Solovay's realization settles something arithmetic alone left open. The diagonal lemma manufactures many sentences G with PA ⊢ G ↔ ¬Prov(⌜G⌝), syntactically unalike; it never says they agree. But de Jongh–Sambin's uniqueness — GL ⊢ □(p↔¬□p) → (p ↔ ¬□⊥) — realized and combined with the derivability condition D1, forces PA ⊢ G ↔ Con(PA) for every such G. So the Gödel sentence is unique up to provable equivalence — and that equivalence class is Con itself. The famous slogan that the Gödel sentence “asserts its own unprovability” understates the case: in PA it asserts, neither more nor less, the consistency of PA. Guarded self-reference in arithmetic is not merely solvable; it is determinate, and the modal logic is what reveals the determinacy.

provable versus true  Solovay proved a second completeness theorem in the same paper, and it draws the corpus's central line in modal ink. Ask not which φ∗ are provable in PA, but which are true in the standard model ℕ. The answer is a different logic:

So the syntax–semantics gap that runs through the whole corpus — proof on one side, truth on the other, incompleteness in between — has a perfectly compact modal form. It is the single axiom □p → p: present in the logic of truth, absent from the logic of proof, and the entire reflection ladder is the attempt to import it, one bounded instance at a time, across the line that GLS draws and GL cannot.

The provability box is the first of a tower. For each n, let [n]φ mean “φ is provable in PA together with all true Π_n sentences” — provability with an oracle for the n-th level of truth. Then [0] is ordinary provability, and each [n] is a stronger notion built on the last. Japaridze's logic GLP axiomatizes them together: every [n] obeys Löb's law, and interaction principles link the levels.

The remarkable fact, Beklemishev's, concerns the closed fragment — the formulas built from ⊤ using only the modalities, no variables at all.

So the two studies meet. The Measure reached ε₀ from proof theory — the supremum of the well-orderings PA can certify, the threshold of provable growth, the height of Gentzen's reduction. Here the same ordinal falls out of the algebra of provability itself, with no transfinite induction assumed at the outset — it is generated by the modalities. One ordinal, approached from the calculus of climbing and from the logic of the box, and the same number both times. That convergence is not a coincidence; it is two views of the single object these studies circle — the exact strength of arithmetic.

the law's two faces  We can now close the account the whole study has been keeping. Löb's law gives, in §IV, an abundance: every box-guarded self-reference has a unique fixed point. Yet the reflection operator R(T) = T + (□p→p) — the operator that would import soundness — has no fixed point at all: R(T) ⊋ T strictly at every consistent rung, which is Gödel-2, which is Löb at ⊥. The same law, abundance on one side and barrenness on the other. The resolution is exact, and it is a difference of kind.