What this is
In 1931, Kurt Goedel proved that any formal system powerful enough to express basic arithmetic
contains statements that are true but unprovable.
This tool lets you see that theorem — not as an abstract proof, but as a measurement.
Pick two theories below: a base theory and a comparison theory.
The machine enumerates all well-formed sentences, classifies each one, and shows you the
Goedel Rest (what the base theory cannot decide) and the
Goedel Bonus
(what the comparison theory resolves that the base theory could not).
The theories
- Robinson Q — The weakest theory sufficient for Goedel's theorem. 7 axioms about 0, successor, addition, multiplication. No induction. Can verify any specific equation (1+1=2) but cannot prove universal statements (for-all-x: x+0=x).
- Peano PA — Q plus the induction schema. Can prove universal statements by checking the base case and inductive step. Resolves ~35% of Q's undecidable sentences.
- Q + extensions — Q with individual axioms added (commutativity, multiplicative identity). Shows that not all axioms are equally powerful.
What the colors mean
- Red = Provable — the base theory can derive this sentence from its axioms.
- Blue = Refutable — the negation is provable in the base theory.
- Gold = Undecidable — the base theory can neither prove nor refute it. This is the Goedel Rest.
- Green = Bonus — undecidable in the base theory, but resolved by the comparison theory.
Formal basis: Richard Zach, Incompleteness and Computability, Open Logic Project.
Engine: goedel-machine (pure Python, zero dependencies).