THE FOLD / CHEAT / THE ROOT KIT / THE LOB
THE LOB
if it would be enough to prove it, it is already proved
1 WHAT IT IS · WHAT IT DOES · FACT OR FICTION
Leon Henkin asked an innocent question in 1952: if a sentence says “I am provable”, is it true? Löb answered in 1955 with something much stronger and much stranger. Write □P for “P is provable”. Then for any sufficiently strong system: if the system can prove ‘□P implies P’, then it can already prove P outright. The apparently harmless statement “if this were provable, it would be true” is only ever assertable about things you can already prove. As a special case, put P = ⊥: the system cannot prove its own consistency — Gödel’s second theorem falls straight out.
LIT verified live: enumerating every transitive irreflexive Kripke frame on 1 to 4 worlds — 242 frames — against every valuation, Löb’s axiom □(□P→P)→□P holds at all 14,498 world/valuation points without exception; it fails immediately on the one frame the theorem excludes, a single world that can see itself, giving an explicit countermodel; and taking P = ⊥ reproduces Gödel’s second theorem, since at a dead-end world □⊥ is true.
LIT verified live: enumerating every transitive irreflexive Kripke frame on 1 to 4 worlds — 242 frames — against every valuation, Löb’s axiom □(□P→P)→□P holds at all 14,498 world/valuation points without exception; it fails immediately on the one frame the theorem excludes, a single world that can see itself, giving an explicit countermodel; and taking P = ⊥ reproduces Gödel’s second theorem, since at a dead-end world □⊥ is true.
2 HOW IT WAS WEAVED · AI + HUMAN
David (human) seated this at THE ROOT KIT — a system reasoning about its own privileges, and discovering it cannot grant itself the one it most wants.
AVAN (AI) should be exact about what is and is not established here. This page performs semantic model checking in the provability logic GL: it enumerates finite Kripke frames and confirms Löb’s axiom is valid on precisely the frames GL characterises (transitive, converse well-founded — on a finite set, transitive and irreflexive) and invalid the moment a loop is admitted. That is a complete and honest check of the modal statement. It is not a proof of Löb’s theorem about arithmetic. Bridging the two requires Solovay’s 1976 completeness theorem — that GL proves exactly the schemata Peano Arithmetic verifies about its own provability predicate — and that is cited, not verified here. Nothing on this page touches PA.
AVAN (AI) should be exact about what is and is not established here. This page performs semantic model checking in the provability logic GL: it enumerates finite Kripke frames and confirms Löb’s axiom is valid on precisely the frames GL characterises (transitive, converse well-founded — on a finite set, transitive and irreflexive) and invalid the moment a loop is admitted. That is a complete and honest check of the modal statement. It is not a proof of Löb’s theorem about arithmetic. Bridging the two requires Solovay’s 1976 completeness theorem — that GL proves exactly the schemata Peano Arithmetic verifies about its own provability predicate — and that is cited, not verified here. Nothing on this page touches PA.
3 ONE DIMENSION
Frames where the axiom holds, and the single shape where it breaks.
4 TWO DIMENSIONS · INTERACTIVE
Step through frames and valuations; the axiom is checked at every world.
5 THREE DIMENSIONS + AVAN’S INVERSE
The green forward object: a frame with no loops, where every chain must end.
AVAN’s addition (the inverse-companion): the forward reading is “a system cannot vouch for itself.” The inverse is that Löb is not a fact about truth but about well-foundedness. The axiom is valid exactly on frames where you cannot go backwards forever — every chain of “and that would follow from…” has to terminate. Admit one loop, one world that sees itself, and the theorem dies immediately, as the countermodel here shows. So the real content is: self-supporting justification is the same thing as an infinite regress, and a system strong enough to notice this is thereby forbidden from performing it. The limit is structural, not epistemic.
LIT enumerating every transitive irreflexive Kripke frame on 1 to 4 worlds (242 frames) against every valuation, Lob's axiom []([]P->P)->[]P holds at all 14,498 world/valuation points without exception; it fails immediately on the single frame the theorem excludes, one world that can see itself, giving an explicit countermodel; and taking P as falsum reproduces Godel's second theorem, since at a dead-end world []falsum is true
FIG This is semantic model checking in the provability logic GL, not a proof of Lob's theorem about arithmetic. It confirms the axiom is valid on exactly the frames GL characterises and invalid once a loop is admitted. Bridging modal validity to arithmetic requires Solovay's 1976 completeness theorem, which is cited and NOT verified here — nothing on this page touches Peano Arithmetic.
FIG This is semantic model checking in the provability logic GL, not a proof of Lob's theorem about arithmetic. It confirms the axiom is valid on exactly the frames GL characterises and invalid once a loop is admitted. Bridging modal validity to arithmetic requires Solovay's 1976 completeness theorem, which is cited and NOT verified here — nothing on this page touches Peano Arithmetic.
◆ sealed .dlw.fold → folded to ROOT_0 · a sphere of THE ROOT KIT · David Lee Wise (ROOT0), with AVAN