The second mechanism, opened
The dissection of the reductions found three mechanisms where the collection saw two, and put Gödel in the second: a fixed point that exists, made limitative not by any refusal but by a separate fact about the framework. That second mechanism was named only by what it is not. It has a positive theory, and the theory is exact — the meta-asymmetry is governed by a logic, the modal logic GL of the provability box, which is sound and complete for what arithmetic can prove about its own proofs. And that logic contains its own fixed-point theorem. The diagonal does not stop at the sentences; it recurs into the logic that governs them.
three laws · Löb & GL · the fixed point, again · the second theorem in one line · completeness · the recursion
This goes one level below the last. The Anatomy took the collection's reductions and split them by mechanism: refusal (a free twist forbids the naming), asymmetry (the fixed point exists; the meta-level convicts it), construction (the fixed point is built with). The middle one, M2, is where Gödel was relocated — out of the negation-and-limit column and into the company of Löb, Rosser, and Curry, on the grounds that its sentence is a perfectly good fixed point whose limitative force comes from somewhere else: consistency, the derivability conditions, contraction. The Anatomy left it there, characterized by a lack. But "the meta-level convicts the fixed point" is not a shrug — it is a precise, complete, decidable theory, and unfolding it is the natural next cut. What does the framework's reasoning about its own provability actually obey? The answer is a logic with four laws and one shocking consequence: it proves its own incompleteness as a one-line corollary, and it has, sitting inside it, a second copy of the very fixed-point theorem that produced the sentences in the first place.
Read □σ as "σ is provable in T." It is not an arbitrary predicate: it obeys three laws, and those three laws are a modal logic already named.
Fix a consistent, recursively axiomatized T ⊇ PA and write □σ for the arithmetized sentence ProvT(⌜σ⌝). The whole of the second mechanism rides on three facts about □ — the Hilbert–Bernays–Löb derivability conditions — discovered in the course of making Gödel's proof rigorous, and each is a sentence T can prove about itself.
If T proves σ, then T proves that it proves σ — a proof can be exhibited and checked, and that check is itself a proof. The bridge from truth-of-proof to provability-of-proof.
If a conditional is provable and its hypothesis is provable, so is its conclusion — concatenate the two proofs. This is the modal axiom K; with it, □ is a normal modal operator.
Provability is provably Σ₁-complete: if σ is provable, that fact — itself a Σ₁ truth — is provable. This is the modal axiom 4. The box can iterate inside itself.
The fourth law is Löb's, and it is the strangest principle in logic: a system can only prove a thing is true-if-provable by proving it outright. Adding it to K4 gives the logic GL.
Henkin asked in 1952: a sentence that asserts its own provability, H ↔ □H — is it true? Is it provable? The diagonal lemma guarantees such an H exists, but says nothing about its status. Löb answered in 1955, and the answer is a law about the box that no amount of staring at □ in isolation would suggest.
Read it slowly. □σ → σ is a reflection instance — "if σ is provable, then σ" — the soundness one would think any honest system could grant itself for free. Löb says it cannot: the only sentences whose reflection instance T proves are the ones T already proves. Soundness is never free; to assert it for σ is to assert σ. The proof is the diagonal lemma again, now aimed at the box.
Now the missing law is in hand. Add Löb's schema to K and the result — call it GL, for Gödel and Löb — is a complete modal logic. The fourth law 4 is not even needed as a separate axiom; it follows from Löb's. And here is the feature that makes GL the right object: its defining axiom is itself self-referential. □(□p → p) → □p is a statement about the box applied to a statement about the box. The logic of self-reference is, in its single distinguishing law, self-referential. That is not decoration; it is the reason the next section's theorem exists.
GL = K + □(□p→p)→□p. Sound for provability: the three laws give K4, Löb's theorem gives the Löb axiom, so every GL-theorem is a provable schema about ProvT. The interesting direction — that it captures everything provable about the box — is Solovay's, and it waits in §V.
The mechanism that produced the self-referential sentences has a logic; and that logic, astonishingly, contains the same theorem that produced them — a fixed-point theorem, now with uniqueness the original could not give.
The diagonal lemma is Lawvere's power direction in the syntactic category: every operation on sentences has a fixed point. One would not expect that structure to reappear inside the modal logic of the box. It does — and in a sharper form.
This is a fixed-point theorem internal to the logic: every boxed operator on the algebra of formulas has a fixed point, and the box pays for two things the bare Lawvere theorem leaves open. Well-definedness: modalization is the guardedness that keeps the recursion from spinning — p may only be consulted "through a proof," never raw. Uniqueness: Lawvere hands back a fixed point; GL hands back the fixed point, the same one up to provable equivalence, and an algorithm to write it down. The shadow is not just present; it is improved.
And the two most famous sentences in logic are simply its two simplest cases — no longer mysterious self-referential constructions, but the unique computable fixed points of the two one-symbol boxed operators.
Gödel's sentence is consistency. The unique fixed point of ¬□p computes to ¬□⊥ — the statement that ⊥ is unprovable. So T ⊢ G ↔ Con(T): the sentence that says "I am unprovable" is provably equivalent to "this system is consistent." Gödel's first theorem and his second are the same sentence, read two ways.
Henkin's sentence is just true. The unique fixed point of □p computes to ⊤ — so the Henkin sentence is provable, ⊢ H. This is Löb's theorem in fixed-point form: a sentence asserting its own provability is provable, because the fixed point of "provable" is truth itself. The question Henkin asked and the law Löb found are one fact.
Look at what the table says. The collection's first mechanism gives the self-referential sentence; this theorem identifies it — strips the self-reference and returns a plain formula in the base language (Con(T), or ⊤). The fixed-point structure that the Anatomy traced through Cantor, Gödel, and the Y-combinator does not terminate at the sentence level. It runs again, one storey up, in the logic that adjudicates those sentences — and there it is even better behaved, because the box enforces the discipline that makes fixed points unique. Self-reference is not a feature of the sentences; it is a feature of the box, and the box is a fixed-point operator.
The Anatomy could only say M2 was "existence plus a meta-fact." Now the meta-fact has a name and a shape: it is membership in GL, and GL's own organizing theorem is a fixed-point theorem. M2 is not the absence of M1's freeness; it is the presence of a second diagonal — the one the box draws on itself.
Gödel's second theorem — that a consistent system cannot prove its own consistency — is not a separate result. It is Löb's law at a single substitution.
Once the box obeys GL, the second incompleteness theorem requires no further machinery — no new diagonalization, nothing about arithmetic beyond the three laws. Take Löb's schema and set σ = ⊥.
That is the whole proof. The second theorem is the Henkin sentence's law evaluated at falsehood: the one reflection instance a system would most like to prove about itself — that it will never prove a contradiction — is exactly the one Löb forbids, because proving it would be proving the contradiction. Note what was not used: no second appeal to the diagonal lemma, no ω-consistency, no detail of the arithmetic. Everything happened inside GL. The second incompleteness theorem is a modal triviality once the modal law is in place — which is the strongest possible evidence that the law, not the arithmetic, is where the content lives.
Soundness says GL proves only true things about provability. Solovay's theorem says it proves them all — and is decidable. The second mechanism is not just lawful; its law is complete.
A logic sound for provability is useful; a logic complete for it is final. The question is whether GL captures every schematic principle the provability box obeys, or merely some. Solovay settled it, and the answer is the strongest available.
So GL is precisely the propositional logic of provability — not a model of it, not an approximation, but its complete theory. Every schema PA validates about its own provability predicate is a GL-theorem, and every non-theorem of GL fails under some interpretation. And GL is decidable: there is an algorithm that, given a schematic claim about provability, settles whether PA proves all its instances. The second mechanism — the one the Anatomy could name only by what it lacked — turns out to have a complete, decidable, finitely axiomatized logic. The asymmetry that distinguishes Gödel from Cantor is not a vague "meta-fact." It is GL, in full, and we possess it entirely.
M1's freeness is a one-line phenomenon; M3's construction is a feat of category theory. M2 sat between them, defined by a negation. Solovay closes the account: M2 has the richest theory of the three — an entire complete modal logic, with its own fixed-point theorem and the second incompleteness theorem as a corollary. The middle mechanism is not the dull one. It is the one with a logic.
What the descent into M2 finally shows is that the collection's thesis is truer than it states: self-reference is not a property of the sentences. It is a property of the operator, and it recurs.
Stand back from the three sections. The first mechanism produces a self-referential sentence by feeding a name to itself — the diagonal, Lawvere's construction, the one organ the Anatomy isolated. Descend into the second mechanism and the same structure is waiting: the logic that governs those sentences, GL, has its own fixed-point theorem, by which each self-referential sentence is the unique fixed point of a boxed operator and is computed back down to a plain formula — G to Con(T), H to ⊤. The diagonal at the level of sentences is governed by a diagonal at the level of the logic. And the logic's single distinguishing axiom, □(□p→p)→□p, is itself a sentence about the box turned on the box. There is self-reference in the objects, and self-reference in the law that governs the objects, and the law is the reason the objects behave.
This is the collection's own wager, returned with interest. Quodlibet holds that one construction underlies the reach and the boundary of formal reasoning, and that a map of self-reference must, being self-referential, contain itself. The descent into the second mechanism makes the second half literal. The map contains itself not once but at every level: the construction that draws the boundary is the construction that the boundary's own logic is built from. Pull the thread marked "Gödel is not a refusal but an asymmetry," follow it down past the three laws and Löb's law into the fixed-point theorem of the box, and you arrive back at Lawvere — one storey up, sharper, with uniqueness. The diagonal has no floor either. It has a recurrence.
One organ, dissected; then one tissue of that organ, dissected again. Each cut found the same figure waiting at the bottom — which is, after all, exactly what a theorem about self-reference should predict about the study of itself.
The first mechanism draws the diagonal. The second mechanism has a logic — and the logic draws the diagonal again, on itself, with a steadier hand. The box is a mirror, and it is provably so.