Deep apparatus · IV — the refinement
The instances gave a fixed point; the refinement makes it the only one. When provability is treated as a modal operator — the box □, read "it is provable that" — the schematic laws of proof become a logic, GL, in which Löb's theorem is an axiom. And in that logic the diagonal sharpens beyond recognition: every self-referential sentence built from the box has a fixed point that is unique up to provable equivalence and explicitly computable. The most famous consequence is a single equation. The sentence "I am unprovable" is not merely some fixed point of negated provability; it is provably equal to "this theory is consistent." Self-reference, read through the box, has no slack at all.
The earlier deep-dives worked at the level of sentences: the diagonal lemma built a sentence asserting a property of itself, and Lawvere's theorem guaranteed such a fixed point exists. This one moves up one storey — not to reason in the theory T about numbers and sentences, but to reason about T's own provability, using a modality. Write □A for "A is provable in T." The principles that □ obeys — that proof respects implication, that what is proved is provably proved, and Löb's law — are not about any particular sentence; they are schematic, and they form a complete and decidable modal logic. That logic is GL, the Gödel–Löb logic of provability.
Four movements. First the operator and its logic GL, with what it asserts and the one thing it pointedly refuses. Then the semantics — finite, transitive, irreflexive frames — in which Löb's law becomes the geometric fact of well-foundedness, and Gödel's second theorem becomes a single world at the end of a chain. Then Löb's theorem itself, proved from the diagonal, and shown to be the axiom GL is named for. And then the fixed-point theorem of de Jongh and Sambin — existence, uniqueness, and an algorithm — which is the precise sense in which the refinement refines: among all the instances of the construction, the provability one carries a rigidity the others lack, and that rigidity is exactly the Löb structure.
The schematic laws of provability are three: distribution, necessitation, and Löb. Together they are GL — and what makes GL the logic of provability rather than of truth is precisely the axiom it does not have.
A modality is an operator on propositions. Here the operator is □, intended as "provable in T," with its dual ◇A = ¬□¬A reading "consistent with T." The language is ordinary propositional logic with □ added; the laws governing □ are read off the derivability conditions of §III, lifted to schemata.
Two consequences fix the character of GL. First, the transitivity axiom 4 : □A → □□A is a theorem, not a postulate — it follows from L alone. Second, and decisively, GL does not contain the reflection axiom T : □A → A. Provability does not imply truth; if it did, □⊥ → ⊥ would make consistency provable, which §III forbade. The whole gap between ⊢ and ⊨ is encoded in the single missing axiom — GL is what remains of the logic of necessity when truth is withheld and only Löb's weakened reflection survives.
The box has a geometry. GL is sound and complete for finite, transitive, irreflexive frames — and on such a frame Löb's law is the fact that there are no infinite ascents, while Gödel's second theorem is a single terminal world that believes everything is provable.
A Kripke frame is a set of worlds W with an accessibility relation R; the box quantifies forward along it. The content of GL is carried entirely by which frames it requires.
The terminal worlds are where Gödel lives. At a world with no successors, □A is vacuously true for every A — there are no accessible worlds at which A could fail — so in particular □⊥ holds there. Such a world "believes" that even ⊥ is provable; it sits at the end of every chain and sees nothing beyond. Consequently ¬□⊥ — consistency — fails at that world, so it is not valid, so it is not a theorem of GL. Gödel's second incompleteness theorem is that one terminal world. Evaluate it yourself.
Löb's theorem says something that sounds too strong to be true: if a theory can prove that the provability of A would already give A, then it can prove A outright. Its proof is the diagonal once more, and its conclusion is the defining axiom of GL.
In 1955 Leon Henkin asked whether a sentence asserting its own provability — H ↔ □H — is true, or provable, or neither. The question has the same self-referential shape as Gödel's, but with the negation removed, and intuition gives no clear answer. Martin Löb answered it by proving a general principle, from which Henkin's sentence falls out at once: such a sentence is provable, hence true.
Every step of that proof can be carried out under a box, which is to say T can prove it about itself: T ⊢ □(□A → A) → □A. That is Löb's axiom L — the formalized theorem — and it is what makes GL the logic it is. Two corollaries fall out immediately. Taking A = ⊥, the axiom reads □(□⊥ → ⊥) → □⊥, i.e. □Con(T) → □⊥; contrapositively a consistent T cannot prove its own consistency — Gödel's second theorem, in one line. And Henkin's sentence H ↔ □H gives □H → H trivially, so by Löb T ⊢ H: the sentence asserting its own provability is provable. Where Gödel's sentence flees provability, Henkin's embraces it — and Löb's law decides both.
Notice what just happened to Henkin's sentence. It was self-referential, built from the box, and it turned out to be provably equivalent to ⊤ — pinned to a value with no freedom at all. That was not luck. It is the first instance of a general phenomenon: in GL, every self-referential sentence built from the box has its truth-value determined, uniquely and computably. That theorem is the heart of the refinement.
The instances gave existence; this gives everything. For any self-referential pattern built from the box, the fixed point exists, is unique up to provable equivalence, and is produced by an algorithm. The diagonal, in the provability setting, has no remaining freedom.
Call a formula A(p) modalized in p if every occurrence of p lies within the scope of a □ — as it does whenever p stands for a sentence reached only through "is provable." For such patterns the self-reference resolves completely.
The algorithm — Sambin's — computes the fixed point by recursion on the boxes of A, and always terminates. Its outputs are startling in their definiteness. Compute a few.
The first row is the one to dwell on. Gödel's sentence satisfies G ↔ ¬□G; the calculator's fixed point of ¬□p is ¬□⊥; so GL ⊢ G ↔ ¬□⊥, and by Solovay PA ⊢ G ↔ Con(PA). The sentence that says "I am not provable" is provably the same sentence as "this theory is consistent." The verification is pure Löb: since ¬□⊥ = (□⊥ → ⊥), the axiom gives □¬□⊥ → □⊥, while □⊥ → □¬□⊥ is trivial, so GL ⊢ □⊥ ↔ □¬□⊥ and hence GL ⊢ ¬□⊥ ↔ ¬□¬□⊥ — ¬□⊥ is a fixed point of ¬□p, and uniqueness makes it the one. The most famous self-referential sentence in mathematics was, all along, a statement about consistency wearing a disguise the box removes.
The same construction gave a unique fixed point in GL and a multitude in the recursion theorem. The difference is exactly Löb's law — well-foundedness — and naming it precisely is what keeps the refinement honest.
Set the two fixed-point results of this corpus side by side. Kleene's recursion theorem (§III) produces, for a transformation f, an index e with φ_e = φ_{f(e)} — and then infinitely many others, since every function has infinitely many indices and the construction can be padded without end. There is no canonical fixed point; the quine is one of legion. The de Jongh–Sambin theorem (§IV) produces, for a modalized pattern, a fixed point that is unique up to provable equivalence. There is exactly one Gödel sentence up to equivalence, and it is consistency. Same construction; opposite verdicts on uniqueness.
Frames are converse well-founded; Löb's law holds. Every modalized pattern has a unique, computable fixed point. "I am unprovable" is Con; "I am provable" is ⊤. Pinned, with no freedom.
Self-reference is fully determined. The disguise comes off and there is exactly one face beneath.
No well-foundedness on indices; no Löb's law. The recursion theorem gives a fixed point and then infinitely many more — padding, re-indexing, endless variants. No quine is canonical.
Self-reference exists but is not located. The face beneath the disguise is one of uncountably many that would do.
It would overclaim to say that GL generalizes Lawvere's theorem, or that provability logic is "the construction one storey up." Neither is true, and the corpus's discipline is to say so. What is true is precise and narrower: among the instances of §III, the provability instance alone satisfies Löb's law, and Löb's law is exactly the extra structure that converts the construction's existence of a fixed point into uniqueness and computability. The refinement refines one case. But it is the deepest case — the one where self-reference meets a theory reasoning about its own proofs — and there the diagonal is shown to have no slack: the fixed point is not a fixed point but the fixed point, and an algorithm hands it over. That is as sharp as the phenomenon ever becomes.
The box, then, is not a new construction but the old one stripped of its freedom. Provability is the diagonal made rigid; Löb's law is the rigidity; and the unique computable fixed point is what the diagonal looks like when the structure reasoning about it is well-founded. The next deep-dives ask what holds the instances together as instances — the formal theory of reduction — and where the construction's reach finally ends. But the refinement is the high-water mark of definiteness: nowhere else in the corpus is the self-referential object pinned so completely to a single, nameable thing.
One storey up, the diagonal loses its slack. Treat provability as the box, accept Löb's law as an axiom, and every self-referential sentence built from it has a fixed point that is unique and computed — the Gödel sentence revealed as consistency, Henkin's sentence as ⊤, each disguise lifted to show the single thing beneath. The refinement adds nothing to the construction except the one structure that makes it rigid: well-foundedness, which is Löb's law, which is the box. Existence was the instances; uniqueness is the refinement.