The Calculus

Begin with what provability does, as against what it is. Fix a system — Peano Arithmetic, say — and write □A for the arithmetic sentence that says “A is provable in PA,” the formalized provability predicate built by Gödel coding. Now set the coding aside and ask only how □ behaves. Three laws govern it — the Hilbert–Bernays–Löb derivability conditions. First, necessitation: if PA proves A, then PA proves □A — a theorem is provably a theorem. Second, distribution: PA proves □(A→B) → (□A → □B) — provability respects modus ponens. Third, provable provability: PA proves □A → □□A — what is provable is provably provable. None of these is a deep fact about the particular coding; every reasonable provability predicate satisfies them, and they are exactly the laws the limitative proofs lean on.

And these three laws are precisely the axioms of a known modal logic. Read □ as a modal box: then necessitation and distribution are the defining rules of the minimal normal modal logic K, and “provable provability,” □A→□□A, is the modal axiom called 4. So provability is, to start, a normal modality of type K4 — an operator obeying the same laws as “it is necessary that” in a transitive frame. This is already a clarifying move: the tangle of Gödel coding has been replaced by an operator with three clean rules, and everything the limitative results require of provability is captured by them. But K4 is not yet enough. Provability obeys one further law — and that law is the whole difference.

The further law is Löb's theorem, and stated as a fact about provability it is startling. Löb proved, in 1955: if PA proves (□A → A), then PA proves A. Read it slowly. The antecedent □A → A says “if A is provable, then A is true” — a soundness claim for the one sentence A. Löb's theorem says the system can prove that soundness claim only in the trivial case where it can already prove A outright. A system cannot certify, of any particular sentence, that provability would deliver truth — except where the sentence is a theorem anyway. As a schema about □, this is Löb's axiom: □(□A → A) → □A.

Adjoin Löb's axiom to the modal logic of provability and you have the whole system. GL — for Gödel and Löb — is the smallest normal modal logic containing □(□A→A)→□A. It is a small miracle of bookkeeping that Löb's axiom already implies the 4 axiom □A→□□A, so that GL is exactly K plus Löb — distribution, necessitation, and Löb's law, and nothing besides. That is the entire calculus. Every truth about a system's provability that holds by the bare laws of provability is a theorem of it; and it is generated by a single axiom that no weaker modality — not “necessity,” not “knowledge” — obeys. Löb's law is the fingerprint of provability.

And Gödel's second incompleteness theorem is one instance of it. Put A = ⊥, a contradiction. Löb's axiom becomes □(□⊥ → ⊥) → □⊥. Now □⊥ says “⊥ is provable” — that the system is inconsistent — and □⊥ → ⊥ is just its negation ¬□⊥, the sentence asserting the system's own consistency; call it Con. So the instance reads □Con → □⊥: if the system could prove its own consistency, it could prove a contradiction. Contrapositive: if the system is consistent, it cannot prove its own consistency. That is Gödel's second theorem — and in the calculus it is no separate result demanding its own intricate argument. It is simply what Löb's axiom says when you feed it falsehood. The deepest limitative theorem about a system's reach is a substitution instance of the calculus's one axiom.

Recall what the fixed-point lemma does in arithmetic, and what it leaves undone. Given a property φ(x), it produces a sentence ψ with ⊢ ψ ↔ φ(⌜ψ⌝): a sentence saying of itself that it is φ. The lemma guarantees ψ exists, but it builds it by coding, hands back an opaque object, and does not single it out — many sentences satisfy the equation, and “the” fixed point is a convenient fiction. Now ask the same question in the calculus. Take a modal formula A(p), with p marking the place where the sentence refers to itself, and look for a fixed point — a formula H with GL ⊢ H ↔ A(H).

The de Jongh–Sambin theorem (1975) answers, and the answer is everything the arithmetic lemma is not. Provided p is modalized in A — provided every occurrence of p lies within the scope of a □, which is exactly the condition that the self-reference passes through provability — there is a fixed point H that contains no p, only the other letters of A; that is unique up to provable equivalence in GL; and that is computable from A by an explicit algorithm. The implicit becomes explicit; the opaque becomes a formula on the page; the non-unique becomes the unique answer; and the whole thing becomes mechanical. The lemma's bare existence claim is upgraded, in the calculus, to a construction.

And the constructions are illuminating. Feed the engine the modal Gödel sentence — A(p) = ¬□p, “I am not provable” — and the algorithm returns the fixed point ¬□⊥, which is Con, the statement of consistency. So in the calculus the Gödel sentence is not merely true-but-unprovable; it is, provably, the same sentence as the assertion of consistency — the modal computation makes G ≡ Con an explicit identity. Feed it the Henkin sentence — A(p) = □p, “I am provable” — and the fixed point is ⊤, the trivial truth: by Löb's theorem Henkin's sentence is provable, so it reduces to ⊤. The engine below computes the fixed point for each self-referential reading, and reads off what it means back in arithmetic.

Notice the condition, because it is the same condition twice. The theorem needs p modalized — the self-reference must pass through □. That is no accident; it is the modal echo of the truth-versus-provability hinge the threshold volume turned on. A self-reference that runs through provability — p under a □ — has an explicit, well-behaved fixed point; a self-reference that runs through truth — p bare, outside every □ — does not, and the calculus offers it no fixed-point guarantee at all. The formula □p → p, with its bare p in the consequent, is not modalized, and has no clean fixed point. The very line between the provability twist (tame, explicit, fixed) and the truth twist (wild, ungoverned) that separated Gödel from the Liar reappears here as the precise syntactic condition under which a fixed point can be computed. The hinge is modalized in the calculus.

One question has hung over the whole construction. We abstracted provability into □, kept the laws that seemed to matter, and arrived at GL. But how do we know we kept the right laws — that GL is neither too weak, missing some truth about provability, nor too strong, proving some schema arithmetic does not actually validate? The worry is real: a modal logic is only as good as its fit to the thing it models, and these axioms were chosen by hand. Solovay's theorem settles the fit, and settles it completely.

Call an arithmetical realization any assignment sending □ to PA's provability predicate and each propositional letter to some arithmetic sentence; a modal formula A then translates into an arithmetic sentence f(A). Solovay proved, in 1976: GL ⊢ A if and only if, for every arithmetical realization f, PA ⊢ f(A). The left-to-right direction, soundness, we already hold — it follows from Löb's theorem and the derivability conditions. The right-to-left direction is the deep one, and it is exact: if a modal schema holds under every interpretation of its letters as arithmetic sentences, then GL already proves it. So the calculus captures exactly the schemata about provability that arithmetic can prove — nothing true is missing, nothing false has slipped in. The hand-chosen axioms were the right ones, and provably so. GL is not a model of the logic of provability. It is the logic of provability.

The proof carries an irony worth savouring. Solovay's argument is famously intricate, and it turns on self-reference: for each modal formula GL fails to prove, it builds an arithmetic interpretation that PA fails to prove, by coding a Kripke countermodel into arithmetic with the very fixed-point techniques the calculus was meant to tame. The calculus that distills self-reference is shown to be exactly right by a tour de force of self-reference. And one refinement deserves note. GL captures what arithmetic can prove about its provability — but not everything true about it. The schema □A → A, “what is provable is true,” is sound, hence true under every realization, yet GL does not prove it; to prove it would collapse the system. The logic of the true statements about provability is a second calculus, GLS, which adds □A→A as an axiom but bars necessitation — and Solovay characterized it too. The provable and the true about provability are themselves two calculi: a last echo, at the meta-level, of the very gap the whole collection turns on.

A modal logic acquires a geometry through its Kripke semantics — a class of frames, sets of “worlds” joined by an accessibility relation, on which □A means “A holds at every accessible world.” GL has an austere geometry. Segerberg proved, in 1971, that GL is sound and complete for the finite, transitive, irreflexive frames — and even for finite trees. Transitive: reach v from w and u from v, and you reach u from w. Irreflexive: no world accesses itself. Finite — or at least with no infinite ascending chain. These conditions are exactly what Löb's axiom demands; on frames, Löb's law corresponds to transitivity together with converse well-foundedness — no chain w₁ R w₂ R w₃ … climbs forever. The geometry of provability is the geometry of strict, well-founded order: you may always climb higher, but only finitely far.

The irreflexivity is the frame-level shadow of Gödel's insight. In a reflexive frame — each world seeing itself — the schema □A→A would hold: provability would entail truth. GL's frames are irreflexive precisely because provability does not entail truth; a world need not satisfy what holds at the worlds above it. And the well-foundedness — no infinite ascent — is what makes Löb's law go through: □(□A→A)→□A holds exactly when every climbing chain terminates, so the induction has a top to bottom out on. The two limitative facts — that provability is not truth, that consistency escapes — are written into the shape of the frames: irreflexive, well-founded order.

And from this austere geometry comes decidability — and with it the punchline. Because GL is complete for finite frames and is finitely axiomatized, it is decidable: an algorithm decides, of any modal formula, whether GL proves it — and the decision sits in PSPACE, no worse than the logic of plain necessity. Pause on that against everything before it. The self-referential phenomena are undecidable in arithmetic — no algorithm decides whether an arbitrary sentence is provable, by Turing and the diagonal. Yet the laws of provability — the calculus GL — are perfectly decidable. The undecidability did not vanish; it relocated. It lives entirely in the arithmetical realization — in which sentences you assign to the letters, and what those sentences happen to say — and not at all in the laws the operator obeys. Strip a self-referential sentence to its modal form and “does this hold?” becomes mechanically answerable; restore its arithmetic content and the question is Turing-undecidable once more. The mystery of self-reference was never in its logic. It was in its matter.

Stand back and see what the calculus has done to the engine the threshold volume uncovered. There, the fixed-point construction was a single dark mechanism that the limitative results all turned. Here it has been opened, and every part of it is in view.

Three things the distillation reveals, each a sharpening of an earlier volume. First, the fixed-point lemma's content is modal — what it is really about is the operator □, and its fixed points are computable functions of the modal structure, by de Jongh and Sambin. The threshold's engine has explicit gearing, and the gearing turns on provability alone. Second, the limitative results are axiomatic, not miraculous — Gödel's second theorem is Löb's axiom fed falsehood, and in the calculus the “shocking” theorems are simply what the laws of provability say; the tribunal's rank-one instances become, here, the definition. Third, the undecidability is relocated — the form of self-reference, the modal laws, is tame and decidable; only its matter, which arithmetic sentences, is wild. The obverse showed the diagonal has two faces, limit and power; the calculus adds a third axis — the diagonal has a tame form and a wild matter, and provability logic is the tame form drawn whole.

So the place of the calculus is clear. GL is to provability what Lawvere's theorem is to the diagonal: the level of abstraction at which a sprawling, instance-by-instance phenomenon becomes a single object with laws. The diagonal volume found the one construction behind the six results; the threshold found the precondition that lets it appear; the calculus finds the laws it obeys once it has appeared, and shows them to be few, decidable, and exact. Self-reference, which looked like the wild edge of mathematics — where systems break and truths escape — turns out, at the level of its logic, to be among the most orderly things there is: a finite calculus, complete and decidable, generated by a single axiom, in which the famous catastrophes are theorems you can check by machine. The engine of the limitative results runs, it emerges, on clockwork.