Can a Rulebook Prove Every Truth It Can State?

Imagine a mathematical referee with a modest job. Give the referee a proposed proof, and it checks every line against an exact rulebook. The referee never tires, never overlooks a missing premise, and never accepts “you know what I mean.”

Now give the referee a larger assignment: for every sentence written in its mathematical language, eventually print either proved or disproved.

Kurt Gödel showed why that second assignment can be impossible even when proof-checking works perfectly.

What kind of rulebook is at stake?

A formal theory consists of a precisely defined language, starting statements called axioms, and rules that produce new sentences from earlier sentences. Call one such theory $T$. The notation

$$T\vdash \varphi$$

means that the sentence $\varphi$ has a finite formal proof from the axioms and rules of $T$.

Three conditions determine whether today’s theorem applies:

• Consistency: $T$ never proves both a sentence $\varphi$ and its negation $\neg\varphi$.
• Effective axiomatization: a mechanical procedure can recognize or systematically list the axioms and check proposed proofs.
• Enough arithmetic: $T$ can express a small core of facts about natural-number addition and multiplication. The usual technical threshold is a seven-axiom theory called Robinson arithmetic, written $Q$.

A theory is complete when, for every sentence $\varphi$ in its language, either $T\vdash\varphi$ or $T\vdash\neg\varphi$. A sentence for which neither proof exists makes the theory incomplete.

J. Barkley Rosser’s 1936 strengthening of Gödel’s result has a compact modern statement:

If a consistent, effectively axiomatized formal theory $T$ contains Robinson arithmetic $Q$, then some sentence $R_T$ can be neither proved nor disproved in $T$.

In symbols, there is an $R_T$ such that

$$T\nvdash R_T \qquad\text{and}\qquad T\nvdash\neg R_T.$$

The subscript on $R_T$ matters. The undecidable sentence is constructed for the particular theory $T$; Gödel did not uncover one magic sentence that defeats every possible collection of axioms.

How arithmetic learns to inspect a proof

The interactive diagram introduces four objects in order. Select a stage to see what it contributes. The final stage depends on all three stages before it.

Interactive proof map

Four moves let arithmetic inspect its own proofs

1Rules2Encode3Inspect4Reflect

Stage 1 of 4

Fix a checkable rulebook

Choose a formal theory T: a list of axioms and inference rules whose alleged proofs can be checked by a mechanical procedure.

The second stage is the hinge. Gödel assigned natural numbers to the symbols and expressions of a formal language. Once formulas and proofs have number codes, a theory of arithmetic can make statements about those codes without adding a mysterious word such as “truth” to its language.

A worked toy encoding

Here is a miniature version of that numerical trick. Assign four token codes:

Token	$1$	$+$	$=$	$2$
Code	$1$	$2$	$3$	$4$

The expression $1+1=2$ therefore produces the code sequence

$$(1,2,1,3,4).$$

Use successive prime numbers as places and the token codes as exponents:

$$\begin{aligned} N &=2^1\cdot 3^2\cdot 5^1\cdot 7^3\cdot 11^4\\ &=2\cdot 9\cdot 5\cdot 343\cdot 14{,}641\\ &=451{,}967{,}670. \end{aligned}$$

The fundamental theorem of arithmetic says that a positive integer has a unique prime factorization. Factoring $451,967,670$ recovers the exponent sequence $1,2,1,3,4$, and the token table recovers $1+1=2$. The numerical code is enormous compared with the expression, but compactness is irrelevant. Gödel needed an unambiguous translation between syntax and arithmetic.

His 1931 construction handles variables, parentheses, quantifiers, complete formulas, and sequences of formulas. The same idea lets arithmetic express a relation

$$\operatorname{Prf}_T(p,s),$$

which means: the natural number $p$ codes a valid $T$-proof whose final sentence has code $s$. Define

$$\operatorname{Prov}_T(s)\;\equiv\;\exists p\,\operatorname{Prf}_T(p,s).$$

Thus $\operatorname{Prov}_T(s)$ means that at least one natural number codes a proof of the sentence numbered $s$.

Where the blind spot enters

A result called the diagonal lemma constructs a sentence $G_T$ whose relationship to its own code can be proved inside $T$:

$$T\vdash G_T\leftrightarrow \neg\operatorname{Prov}_T(\ulcorner G_T\urcorner).$$

The corner marks $\ulcorner G_T\urcorner$ mean “the natural-number code of $G_T$.” The displayed equivalence is the careful mathematical content behind the loose paraphrase “this sentence is not provable.” The Stanford Encyclopedia of Philosophy warns that the paraphrase should not be mistaken for a literal English sentence hidden inside arithmetic.

Now follow one side of the argument step by step.

1. Suppose $T\vdash G_T$.
2. A finite proof of $G_T$ would have a definite natural-number code, say $p$.
3. Because $T$ can check encoded proofs, $T$ could verify $\operatorname{Prf}_T(p,\ulcorner G_T\urcorner)$ and derive $\operatorname{Prov}_T(\ulcorner G_T\urcorner)$.
4. The defining equivalence for $G_T$ would also let $T$ derive $\neg\operatorname{Prov}_T(\ulcorner G_T\urcorner)$.
5. The two conclusions contradict each other. If $T$ is consistent, the supposition in step 1 must fail: $T\nvdash G_T$.

Proving that $T\nvdash\neg G_T$ requires more care. Gödel’s original 1931 argument assumed a stronger condition called $\omega$-consistency. In 1936, Rosser replaced $G_T$ with a sentence $R_T$ that compares a proposed proof with shorter proofs of its negation. Rosser proved that ordinary consistency alone forces both $T\nvdash R_T$ and $T\nvdash\neg R_T$. The formal theorem stated above uses Rosser’s strengthened version.

If $T$ is sound—meaning its theorems are true about the ordinary natural numbers—then the Gödel sentence $G_T$ is true there. The theorem’s strictly formal conclusion, however, concerns provability relative to a specified theory. Keeping truth and formal proof separate prevents many exaggerated interpretations.

Try the boundary yourself

Problem 1

Which one of these rulebooks is forced into incompleteness by the theorem?

1. A truth-table system containing only two propositional variables, $P$ and $Q$.
2. Peano arithmetic, provided Peano arithmetic is consistent.
3. An arithmetic rulebook that proves both $0=1$ and $0\ne1$.

Reveal the solution

Rulebook 2. Peano arithmetic is effectively axiomatized and contains more than enough natural-number arithmetic. If it is consistent, Gödel–Rosser applies.

The finite truth-table system in rulebook 1 does not express the required arithmetic and can be complete. Rulebook 3 fails the consistency condition; in classical logic, a contradiction allows every sentence to be proved, so “complete” would become vacuous rather than useful.

Problem 2

Suppose $R_T$ is undecidable in $T$, and a mathematician creates $T_1$ by adding $R_T$ as a new axiom. Has the mathematician escaped incompleteness?

Reveal the solution

The new theory $T_1=T+R_T$ can prove $R_T$, so one specific gap has been filled. If $T_1$ remains consistent, effectively axiomatized, and strong enough for arithmetic, the theorem applies to $T_1$. It supplies a new sentence $R_{T_1}$ that $T_1$ can neither prove nor disprove.

The next diagram separates the settled sentence from the new sentence created for each enlarged theory.

Extending the rulebook

One new axiom settles one sentence, then a new boundary appears

Why anyone tried to complete mathematics

In the late nineteenth and early twentieth centuries, set-theoretic paradoxes had exposed trouble inside the foundations of mathematics. Bertrand Russell and Alfred North Whitehead attempted an enormous logical reconstruction in Principia Mathematica, published from 1910 to 1913. David Hilbert’s program in the 1920s pursued a related but distinct ambition: formalize mathematics and establish its consistency using tightly controlled methods. The history of Hilbert’s program explains why proof itself became an object of mathematical study.

Gödel entered the University of Vienna intending to study physics, switched to mathematics, and attended discussions associated with the Vienna Circle. His doctoral work proved a completeness theorem for first-order logic: every logically valid first-order sentence has a proof. The apparent clash with his later incompleteness theorem disappears once the subjects are named. Logical completeness concerns first-order logic itself; arithmetic incompleteness concerns particular effectively axiomatized theories written in that logic.

Gödel’s incompleteness paper was received on November 17, 1930, and published on December 1, 1931, when he was 25. The paper did not make formal reasoning worthless, and Gödel explicitly resisted that reading. It proved that no one consistent, mechanical axiomatic package of the required strength can settle every sentence it can formulate.

The theorem arose from a mathematical dispute, not from the political violence that followed. That distinction matters because Vienna’s intellectual world was soon broken apart. The Institute for Advanced Study’s biography records that Jewish students and students with socialist sympathies were forcibly removed from classes during the 1930s. Moritz Schlick, whose seminar helped draw Gödel toward logic, was murdered in 1936. Gödel was not Jewish, but a gang attacked him as if he were; his application for a paid Vienna position was rejected in 1938. Fearing conscription after Nazi Germany absorbed Austria, Kurt and Adele Gödel escaped by the long route across the Soviet Union and Pacific, arriving in San Francisco on March 4, 1940.

What the theorem touches now

Modern proof assistants make the referee from the opening concrete. Lean’s kernel checks whether a proof term follows Lean’s formal rules, and its documentation emphasizes that a theorem using custom axioms is valid only relative to those axioms’ soundness. The Lean proof-validation guide even provides a command for listing which axioms a theorem depends on. The Rocq Prover supports machine-checked mathematical proofs and proofs that programs meet formal specifications.

Incompleteness does not diminish those tools. It explains their contract. A proof assistant can catch an invalid derivation with extraordinary reliability without becoming an automatic oracle for every statement expressible in its logic.

Gödel’s coding and diagonal strategy also belongs to the ancestry of theoretical computer science. Alonzo Church and Alan Turing gave equivalent mathematical accounts of mechanical computation in 1936, and undecidable problems such as the halting problem established limits on what algorithms can settle. The Stanford Encyclopedia’s account of the Church–Turing thesis distinguishes a procedure that always decides from one that merely keeps finding positive cases. Gödel’s theorem and the halting problem are different results, but both expose a boundary created when a sufficiently expressive symbolic system can encode computation or syntax.

Speculative application: future artificial-intelligence theorem provers may discover new axioms, switch theories, or help mathematicians choose stronger assumptions. No single consistent, effectively axiomatized engine strong enough for arithmetic can certify every sentence in its own language. That limitation concerns universal reach, not how many valuable proofs such a system might find.

One idea to remember

For every consistent, mechanical rulebook strong enough to describe elementary arithmetic, there is a sentence the rulebook can state but can neither prove nor refute:

$$\exists R_T\;\bigl(T\nvdash R_T\;\land\;T\nvdash\neg R_T\bigr).$$

The boundary belongs to the chosen rulebook. Add an axiom and the boundary moves; under the same conditions, it does not disappear.

Useful next directions are the diagonal lemma, Gödel’s second incompleteness theorem, the halting problem, and concrete independence results such as Goodstein’s theorem.

Sources

• Kurt Gödel, “Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I”, Monatshefte für Mathematik und Physik 38, 173–198, 1931.
• Panu Raatikainen, “Gödel’s Incompleteness Theorems”, Stanford Encyclopedia of Philosophy, substantive revision April 9, 2025.
• Richard Zach, “Hilbert’s Program”, Stanford Encyclopedia of Philosophy.
• J. Barkley Rosser, “Extensions of Some Theorems of Gödel and Church”, Journal of Symbolic Logic 1(3), 87–91, 1936.
• Institute for Advanced Study, “Kurt Gödel: Life, Work, and Legacy”, biographical essay and archive materials.
• Lean project, “Validating a Lean Proof”; Rocq project, Rocq Prover overview.
• B. Jack Copeland, “The Church–Turing Thesis”, Stanford Encyclopedia of Philosophy.