Zero Paradox · interactive map

The Diagonal Family — one engine, two fates

One diagonal fixed point sits behind Cantor, Russell, Gödel, Tarski, Turing and the recursion theorem (Lawvere 1969). The same engine forks by a single question — can self-reference close? On the wall side (μ) it cannot: the argument runs as a proof that no fixed point exists. On the floor side (ν) it does: the fixed point is produced — and at ⊥ it is the framework’s own.

the diagonal engine no reflexive object carries a fixed-point-free map · axiom-free μ WALL · CANNOT CLOSE ν FLOOR · DOES CLOSE Cantor no onto its power set Russell membership not onto Turing no self-halting decider Tarski no internal truth Curry no naming surjection Quine atom ⊥={⊥} · the floor Kleene quine a self-printing program Löb □A→A yields A Gödel 2nd no self-consistency proof Rice exists, yet undecidable Gödel 1st the undecidable diagonal sentence Lawvere 1969 · Yanofsky 2003 — one scheme behind them all
Why does each argument sit where it does?
Hover or tap any node — the family tells you which fate it takes and why, with the checkable Lean witness.
The diagonal engineone fixed-point lemma behind every argument (Lawvere)
μ wall — cannot closethe argument IS a proof that no fixed point exists
ν floor — does closethe fixed point is genuinely produced
The Quine atom ⊥the floor face that is the framework’s own bottom
Carries Classical.choiceKleene, Rice — inherited from Mathlib recursion theory
Gödel’s firstthe undecidable diagonal sentence, built by the engine

One engine, two fates. Every argument here is the same diagonal fixed point under one question — can self-reference close on itself? On the μ wall side the answer is no, and the classical argument (Cantor, Russell, Turing, Tarski, Curry) is the proof that no fixed point exists. On the ν floor side the answer is yes: the fixed point is produced (the Quine atom, the Kleene quine, Löb, Gödel’s second, Rice). Gödel’s first theorem sits between — the diagonal sentence the engine builds. The μ wall faces plus Löb and Gödel’s second are axiom-free; the two computability floor faces (Kleene quine, Rice) carry Classical.choice from Mathlib’s recursion theory.

What is drawn vs. what is claimed. The unification is Lawvere’s (1969), restated by Yanofsky (2003) — the arguments as one scheme is prior art, cited not claimed. This figure is a placement of the framework’s ⊥ among these recognized arguments, not a new theorem; the cross-face identity stays a type boundary — the same shape, provably distinct carriers. The one floor face that is the framework’s own bottom is the Quine atom ⊥={⊥}, the seam the Bottom Family tree grows from.

← The Bottom Element