Where the fixed point goes quiet
The fourth and final reception is the strangest. The Knot showed the diagonal detonating over genuine truth; here the very same construction, aimed at a slightly weaker target, neither detonates nor builds nor is forbidden. It is absorbed — and the system, asked the one question the fixed point poses, simply falls silent. The Gödel sentence is true and unprovable; the consistency statement is true and unprovable; and a system that tries to trust its own proofs proves everything. This is incompleteness, and read through the diagonal it is not a defect bolted onto arithmetic but the precise behaviour of a self‑referential system whose codomain tracks proof rather than truth. The explosion of the Knot, cooled by one missing principle, becomes a silence the system can never break from within.
component VI of the diagonal · the absorbed face, isolated and deepened — Gödel's first and second theorems from the fixed point; the derivability conditions and the single principle provability lacks; Löb's theorem, which subsumes the second theorem; the provability logic GL and Solovay's arithmetical completeness; the de Jongh–Sambin fixed point, where the diagonal becomes unique and computable; and the Löbian obstacle to self‑trust
The Knot ended on a hinge: truth detonates, provability does not. That hinge is now the whole subject. One construction, one negation, one forced fixed point — and a codomain just weak enough that the contradiction never forms.
the same sentence, a weaker mirror Build, by the diagonal lemma, the sentence that denies its own provability: G ↔ ¬Prov(⌜G⌝). In form this is the Liar exactly — a fixed point of negation composed with a self‑applied predicate. Over truth, as the Knot showed, such a fixed point is a contradiction, because truth obeys True(⌜φ⌝) ↔ φ and the equivalence closes into True ↔ ¬True. But Prov is not True. It is a proxy — a predicate that tracks what the system can derive, not what is so — and the proxy is missing the one principle that would let the equivalence detonate. The result is not a contradiction but a sentence stranded between proof and refutation: true, because it correctly says it is unprovable, and unprovable, because proving it would make it false. The diagonal still forces its fixed point. The codomain simply has room to hold it without breaking.
absorption, not explosion This is the fourth and quietest fate. The Ceiling forbade the fixed point — no host, an impossibility. The Floor built it — a least solution, the engine of computation. The Knot let it explode — a contradiction over genuine truth. Here the system absorbs it: the fixed point exists, is perfectly consistent, and marks a place the system cannot reach — a true sentence it cannot prove, and, as the second theorem will show, its own consistency among them. Where the Knot was loud, this is silent. The diagonal asks the system whether G is provable, and the system can give no answer: not yes, for then G would be false and provable, collapsing consistency; not no, for the system cannot certify its own limits. The fixed point does not detonate the system. It opens a hole in it — and names the system's blindness to its own soundness.
Everything in this volume turns on a single asymmetry, so it is worth stating with care before it is proved. Truth satisfies the full T‑schema, and in particular reflection: True(⌜φ⌝) → φ, "if it is true, then it holds." Provability satisfies almost everything truth does — it is closed under the rules, it respects implication, it certifies its own operations — but it does not, as an internal theorem, satisfy Prov(⌜φ⌝) → φ. The system cannot prove, in general, that what it proves is so. That one missing conditional is the entire difference between the Knot and the Silence. With reflection, the fixed point of ¬Prov would be a contradiction and the system would explode exactly as the Liar does. Without it, the fixed point is merely undecided, and — by a theorem of Löb we will reach in §IV — the system cannot even add reflection without proving the very thing reflection was supposed to certify. The Silence is what a reflexive system sounds like when its codomain can say "provable" but never, of itself, "therefore true."
The first incompleteness theorem is the diagonal's fixed point, read over provability. Its proof is short, and its two halves need different strengths — a small asymmetry that is itself a clue to how truth and proof come apart.
truth outruns proof Read what has happened. Standing outside the system, we can see that G is true — its unprovability, which we have just demonstrated, is precisely what it asserts. Yet the system cannot prove it. The gap between what is true of arithmetic and what arithmetic can prove is not closed by adding G as an axiom, because the new system has its own Gödel sentence, and the gap reopens one level up — the conservation phenomenon again, the fixed point relocating rather than vanishing. This is the precise sense in which the Silence is a hole and not a wound. Nothing is broken; T remains consistent. But there is a true thing it cannot say, and the diagonal has named it. The asymmetry of the two halves is the tell: unprovability follows from consistency alone, but irrefutability requires the system to be not merely consistent but honest about its existential claims — and honesty, as the second theorem will show, is something no sufficiently strong system can fully certify of itself.
To see why the diagonal cools rather than explodes, one must know exactly which laws the provability predicate satisfies. Three conditions make it a modal operator; a fourth, which truth has and proof lacks, is the whole of incompleteness.
the three conditions Write □φ for Prov(⌜φ⌝). The Hilbert–Bernays–Löb derivability conditions say that provability behaves, internally, like a modal necessity. D1, necessitation: if T ⊢ φ then T ⊢ □φ — what is proved is provably proved. D2, distribution: T ⊢ □(φ → ψ) → (□φ → □ψ) — provability respects modus ponens. D3, the formalised D1: T ⊢ □φ → □□φ — provability of a thing is itself provable. Together these are the modal system K4: a necessity operator that distributes over implication and is transitive. Every step of the second theorem and of Löb's theorem is built from exactly these three, and from nothing about truth.
The natural reflex is to add reflection — to extend the system with □φ → φ, "everything I prove is true," and so close the gap. It cannot be done, and the reason is the deepest result in this volume, proved in the next section. A consistent system that proves □φ → φ for a given φ can already prove φ outright — so adding the uniform reflection principle either changes nothing it could not already do or, taken to its limit, proves its own consistency and collapses. Reflection is not a missing lemma the system overlooked; it is a power the system structurally cannot have over itself. Provability and truth agree on three conditions and part on the fourth, and the fourth is not negotiable. This is why the diagonal, which detonates over the factive codomain of truth, can only go quiet over the non‑factive codomain of proof. K4 with reflection is the logic of truth; K4 with reflection denied, in the precise form Löb discovered, is the logic of proof — and the two are not variants of one system but opposites, as far apart as a thing and its shadow.
Formalise the first theorem and the system is shown unable to prove its own consistency. Then Löb's theorem reveals that this is no isolated fact but a special case of a single, sweeping limitation on self‑certification.
Gödel II The proof of the first theorem — "if T is consistent then G is unprovable" — uses only the derivability conditions, so it can itself be carried out inside T. Formalised, it reads T ⊢ Con(T) → ¬Prov(⌜G⌝), that is, T ⊢ Con(T) → G. Now suppose T could prove its own consistency, T ⊢ Con(T). Then T ⊢ G — contradicting the first theorem. Therefore T ⊬ Con(T): a consistent system strong enough to formalise its own syntax cannot prove that it is consistent. The consistency statement joins the Gödel sentence in the silence — true, and beyond the system's reach.
Löb's theorem — the general law Gödel II looks like a fact about consistency, but it is the shadow of something larger. Ask: for which φ can the system prove the reflection instance □φ → φ — "if φ is provable, then φ"? Löb's astonishing answer (1955): only for those φ it can already prove outright. If T ⊢ □φ → φ, then T ⊢ φ. The system can certify the soundness of its own proofs only where it does not need to — only for theorems it already has. The formalised version, T ⊢ □(□φ → φ) → □φ, is a theorem schema of T itself, and it is the engine of everything here. Gödel II falls out by setting φ = ⊥: then □⊥ → ⊥ is exactly Con(T), and Löb says proving it would prove ⊥. The second theorem is Löb's theorem aimed at the empty target.
Löb's proof — and Gödel II as the case φ = ⊥
Löb's theorem is the precise statement of the Silence, and its content is almost vertiginous. A formal system cannot consistently trust itself. The principle "whatever I prove is true," applied to any particular claim, either is idle — because the claim was already provable — or, taken across the board, proves the system's own consistency and so, by Gödel II, cannot be had at all. There is no safe amount of self‑reflection: the instant a system can prove □φ → φ for a φ it could not otherwise reach, it has overreached, and only consistency‑failure lies that way. This is why reflection cannot be added (§III), why consistency cannot be proved (Gödel II), and why the Gödel sentence stays unprovable (Gödel I) — three faces of the one fact that a reflexive system's grasp of its own soundness is structurally, permanently incomplete. The diagonal does not merely leave a true sentence unproved. It proves that the system can never close the gap by trusting itself, because self‑trust, formalised, is self‑refutation.
All of it — Gödel I, Gödel II, Löb — is one modal axiom. The absorbed fate is not a collection of clever tricks but a single, decidable modal logic, and Solovay's theorem proves it captures provability exactly.
one axiom for everything Treat □ as a primitive modal operator and ask what propositional principles it obeys. The answer is the logic GL — Gödel–Löb — built from ordinary propositional logic plus the distribution axiom K and a single, strange‑looking schema, the Löb axiom:
This is Löb's theorem, frozen into an axiom. From it the transitivity condition □p → □□p is derivable, so GL needs nothing else — and, crucially, the reflection axiom □p → p is not among its theorems and cannot be added without collapse. The entire behaviour of arithmetical provability, every incompleteness phenomenon of this volume, is the propositional consequence of that one line.
the shape of the models GL is sound and complete for a vivid class of Kripke frames: the finite, transitive, irreflexive ones — equivalently, finite strict orderings with no infinite ascending chains. Irreflexivity is the semantic face of the missing reflection: no world sees itself, so □p → p can fail, and the Löb axiom is precisely what these converse‑well‑founded frames validate. In such a frame, □⊥ — "everything is provable," the mark of inconsistency — is true exactly at the leaves, the worlds that see nothing, where every claim holds vacuously. The frame below is one such model; toggle the valuation and watch where provability, the empty box, and consistency fall.
a finite GL frame — click a world to toggle p
In general the diagonal lemma produces a fixed point but never says it is the only one. Inside GL the situation transforms: every self‑reference through the box has a unique, computable fixed point — and computing it dissolves the Gödel sentence's mystery entirely.
de Jongh and Sambin Call a variable p modalised in a formula φ(p) if every occurrence of p sits inside a □. The de Jongh–Sambin theorem says: whenever p is modalised, there is a formula ψ not containing p with GL ⊢ ψ ↔ φ(ψ) — a fixed point — and it is unique up to provable equivalence and explicitly computable from φ. The diagonal lemma, which over raw arithmetic gives a fixed point dependent on the coding and canonical in no particular way, becomes inside GL a deterministic operation returning the fixed point. Self‑reference through provability is not just possible but algorithmic.
compute the fixed point — self-reference collapses to consistency
The headline computation deserves to be dwelt on, because it removes the last of the mysticism that clings to incompleteness. The Gödel sentence is the fixed point of ¬□p, and de Jongh–Sambin returns it uniquely: GL ⊢ G ↔ ¬□⊥. That is, G is provably equivalent to Con — the Gödel sentence does not say something eerie and self‑involved about its own unprovability; it says, in effect, this theory is consistent. And of course it does: a true, unprovable arithmetical sentence equivalent to consistency is exactly what Gödel II already told us must exist. The two theorems fuse. The first produces a true unprovable sentence; the second identifies it, up to GL‑equivalence, as the consistency statement; and the fixed‑point theorem makes the identification a one‑line calculation. Far from being a paradoxical curio, G is the most natural unprovable truth there is — the system's inability to see that it does not prove a falsehood. Self‑reference, run through the box, has nowhere to go but consistency, because □⊥ is the only thing the box can say about itself.
With the absorbed fate built, the four are whole. The same diagonal, run against four kinds of answer‑space, gives the four great phenomena of the foundations — and which one it gives is never up to the diagonal.
the fate is the codomain's to decide Stand back and the architecture is complete. One construction — the diagonal, forcing a fixed point of a twist in a self‑naming system — meets four kinds of codomain and yields four destinies. Where the codomain is a complete domain, with a bottom and its suprema, the twist has a fixed point and it is built: recursion, the Floor. Where the twist is fixed‑point‑free and a naming's existence hangs on it, the fixed point is forbidden: limitation, the Ceiling. Where the codomain is factive truth, the missing fixed point is a contradiction and explodes: paradox, the Knot. And where the codomain is a proxy — provability, with the derivability conditions but no reflection — the missing fixed point is merely undecided and is absorbed: incompleteness, the Silence. The diagonal does the same thing every time. It forces the point. What becomes of the point is decided entirely by what the codomain can hold — completeness, rigidity, factivity, or the careful weakness of a proxy. Four readings of one theorem, and the reading is always the host's.
Löb's theorem is not a museum piece; it is a live obstacle wherever a system must reason about its own reliability. Consider an agent that acts only on conclusions it can prove, and that would like to trust its own future proofs — to adopt the principle "if my successor proves it, it is so," a reflection schema. By Löb, any such agent that can prove □φ → φ for a new φ thereby proves φ, and an agent that trusts itself across the board proves its own consistency and is therefore inconsistent. This is the Löbian obstacle to self‑trust, and it is the central difficulty in the theory of self‑modifying and self‑verifying systems — the reason a reflective agent cannot simply endorse the soundness of the very reasoning it is using. The Silence, first heard as a limitation on arithmetic, returns as a limitation on any sufficiently expressive reasoner that turns to face itself: it may be sound, but it cannot certify its own soundness without ceasing to be sound. The gap the diagonal opened in PA is the same gap that opens in any mind, formal or otherwise, that tries to stand fully inside its own trust.
conservation, completed And the law that ran through every volume holds to the last. The diagonal never destroys its fixed point; it relocates it according to the host. Forbidden, the point climbs a hierarchy and reappears one level up (the Ceiling). Built, it is assembled from ⊥ as the least solution (the Floor). Exploding, it is moved into a gap or a glut or a higher language, and the act of repair regenerates it above (the Knot). Absorbed, it stands as a true sentence the system cannot reach — its own consistency, by the fixed‑point calculation — and adding it as an axiom only opens the gap again one storey higher (the Silence). Four fates, four relocations, never once a deletion. The forced fixed point is conserved across the whole of the foundations, and the diagonal's single, indifferent act — force the point to exist — is refracted by the codomain into limitation, recursion, paradox, and incompleteness. What remains is to state the conservation itself as a law, and to draw the trilemma that says no system can escape all four fates at once. That is the work of the final volume. Here the quartet is complete, and the Silence is its quietest and most far‑reaching member — the sound a reflexive system makes when asked, in its own voice, whether it can be trusted.
The fourth reception is the quietest. The same fixed point that detonates over truth, aimed instead at provability — a predicate that tracks proof and not fact, obeying every law of truth but reflection — neither explodes nor builds nor is forbidden. It is absorbed: a sentence true and unprovable, and, as the fixed‑point calculation reveals, equivalent to the system's own consistency. Gödel's first theorem produces it; the second locates it; Löb's theorem generalises the second into a single sweeping bar on self‑trust; and the modal logic GL, complete and decidable by Solovay's theorem, captures the whole of it in one axiom. The system, asked whether it proves a falsehood, cannot answer — not from defect but from structure, because to certify its own soundness would be to refute itself. The diagonal opens a hole exactly where the system tries to see itself, and names it. □(□p → p) → □p — the law that lets a system prove its proofs sound only for what it already proves, and so condemns it to a permanent, dignified silence about its own consistency.