Gödel's Incompleteness Theorems

Part 10, Chapter 10: Foundations, Cardinality, Choice, and Incompleteness

Learning objectives

State Godel's First and Second Incompleteness Theorems precisely
Sketch the role of Godel numbering and self-reference in the proof
Connect incompleteness to the Halting Problem (Turing 1936)
Distinguish the independence of CH from incompleteness

In 1931, Kurt Godel proved that the entire programme of formalizing mathematics is bounded by an internal limit. Any consistent formal system rich enough to express elementary arithmetic contains statements that are TRUE but UNPROVABLE within the system itself. Moreover, no such system can prove its own consistency. These results, the First and Second Incompleteness Theorems, are not exotic special cases; they apply to ZFC, to Peano arithmetic, to Robinson arithmetic, to every reasonable formal system. The companion result for computation, the undecidability of the Halting Problem (Turing 1936), shows the same phenomenon from the computational side: most questions about programs cannot be answered by any algorithm.

Godel's First Incompleteness Theorem

(Godel, 1931) Let $T$ be a consistent, effectively axiomatized (recursively enumerable) formal theory that includes Robinson arithmetic (or any system capable of expressing elementary recursive functions). Then there exists a sentence $G_T$ T in the language of $T$ such that

$G_T$ T is TRUE in the standard model of arithmetic;
$G_T$ T is NOT provable in $T$ ;
$\neg G_T$ T is also NOT provable in $T$ (assuming $T$ is $\omega$ -consistent, a technical strengthening of consistency).

The sentence $G_T$ T is independent of $T$ : neither it nor its negation can be derived. Hilbert's 1900 dream, to find a complete axiomatization of all true arithmetic statements, is mathematically impossible. The set of true sentences of arithmetic is not even recursively enumerable, let alone recursively axiomatizable.

Godel numbering and self-reference

The proof rests on a remarkable trick: Godel numbering. Assign a unique natural number to every symbol, every formula, and every finite proof in the formal language. Concretely, assign:

each symbol a small positive integer (e.g. $0 \mapsto 1, S \mapsto 2, + \mapsto 3, = \mapsto 4$ );
a formula like $S(0) = S(0)$ as the sequence of symbol codes;
encode the sequence as a unique number via prime-power coding: $2^{c_1} \cdot 3^{c_2} \cdot 5^{c_3} \cdots$ .

Once everything has a Godel number, the system can talk about its own syntax: " $\text{Prov}_T(n)$ T(n)" can be made a formula in $T$ meaning "the formula with Godel number $n$ has a proof in $T$ ."

Godel then constructs a sentence $G_T$ T that effectively asserts "I am not provable in $T$ ." Specifically, via the diagonal lemma, there exists a formula $G_T$ T such that $T \vdash G_T \iff \neg \text{Prov}_T(\ulcorner G_T \urcorner)$ TiffnegtextProvT(ulcornerGTurcorner), where $\ulcorner G_T \urcorner$ Turcorner is the Godel number of $G_T$ T itself. The metalevel argument is then:

If $T \vdash G_T$ T, then by consistency $T \nvdash \neg G_T$ T, so the asserted unprovability claim is false, but then $T$ proved a false sentence, contradicting soundness.
So $T \nvdash G_T$ T. That makes the unprovability claim TRUE, so $G_T$ T is true.

Hence $G_T$ T is true and unprovable.

The Venn-style widget can illustrate the relationships: provable sentences $\subset$ true sentences (always, by soundness), but the inclusion is STRICT (Godel), there is an excluded region of true-but-unprovable sentences.

Godel's Second Incompleteness Theorem

(Godel, 1931) Under the same hypotheses as the First Theorem, if $T$ is consistent then $T$ cannot prove its own consistency: $T \nvdash \text{Con}(T)$ , where $\text{Con}(T)$ is the formal statement (expressed via Godel numbering) "no contradiction is derivable in $T$ ."

This is the most philosophically pungent of Godel's results. ZFC cannot prove that ZFC is consistent. To establish ZFC's consistency, you need a strictly stronger system (typically ZFC + an inaccessible cardinal). But then THAT system's consistency requires an even stronger one. There is no formal foothold for absolute certainty about the consistency of mathematics, we believe ZFC is consistent because of long experience and structural intuition, not because of a finite proof.

The Halting Problem and the computational mirror

The computational analogue, due to Turing (1936), is the undecidability of the Halting Problem. Theorem: there is no algorithm $H$ which, given an arbitrary program $P$ and input $x$ , determines in finite time whether $P$ halts on $x$ .

The proof is also a diagonalization. Suppose $H$ existed. Construct a new program $D$ that does the opposite of what $H$ predicts when $H$ is asked about $D$ 's behaviour on its own description. Whatever $D$ does contradicts $H$ 's prediction. Therefore $H$ cannot exist.

The two theorems mirror each other. Godel: there is no complete axiomatization of arithmetic truth. Turing: there is no algorithm deciding all questions about programs. Both establish hard limits on formal mathematics and on what algorithms can ever achieve.

Where this shows up

Computer science (verification): Rice's theorem (1953) is a vast generalization of the Halting Problem: any non-trivial semantic property of programs is undecidable. This is why software verification is fundamentally hard, there is no general-purpose tool that always succeeds.
Foundations of mathematics: The independence of the Continuum Hypothesis (Godel 1940, Cohen 1963) and the independence of the Axiom of Choice from ZF are precise applications of incompleteness-style techniques. ZFC has many non-isomorphic models, the same axioms describe genuinely different mathematical universes.
Theoretical computer science (P vs NP): Some authors speculate that P vs NP might itself be independent of ZFC. While not proved either way, the question is one of the central open problems in CS, and the techniques used to show independence (forcing, ultrapowers) all descend from Godel and Cohen.
Diophantine equations (Hilbert's 10th): The Davis-Putnam-Robinson-Matiyasevich theorem (1970) shows there is no algorithm to decide whether a polynomial equation $p(x_1, \ldots, x_n) = 0$ 0 has an integer solution. This is incompleteness in the language of Diophantine arithmetic.
Penrose's philosophy of mind: Roger Penrose has argued that Godel's theorem implies human mathematical insight cannot be reduced to algorithmic computation. Most logicians find the argument unconvincing, but the debate has generated rich philosophical literature on the limits of formal systems and AI.

Pause and think: Godel's First Theorem says there exist TRUE statements unprovable in ZFC. How do we know they are true if we cannot prove them in ZFC? The answer involves a META-mathematical viewpoint: we step outside ZFC, look at the standard model of arithmetic, and verify the truth there. The unprovability is INSIDE the system; the truth is OUTSIDE.

Try it

Explain in plain English why the Godel sentence "I am not provable" is true. (Hint: it is unprovable for purely logical reasons, assuming consistency forces unprovability, and unprovability is exactly what it asserts.)
Sketch why the Halting Problem implies Godel's First Theorem. (Hint: if every true arithmetic statement were provable, we could decide whether $P$ halts by searching for a proof of " $P$ halts" in parallel with a proof of " $P$ does not halt"; one search would succeed in finite time. This contradicts undecidability.)
The Continuum Hypothesis is independent of ZFC. Is it a Godel sentence? (Answer: not in the strict sense, the standard Godel sentence is a specific arithmetic statement; CH is a statement about cardinals. But both are examples of independent sentences, established by similar logical techniques: Godel's constructible universe $L$ and Cohen's forcing.)
True or false: the Second Incompleteness Theorem implies we should distrust ZFC. (Answer: false. It just means we cannot prove ZFC's consistency INSIDE ZFC. Our confidence in ZFC rests on its long track record of consistency in practice.)

A trap to watch for

People often paraphrase Godel's theorem as "some things are true but unknowable" or "there are truths beyond the reach of mathematics." Both are misleading. What Godel actually proved: for any FIXED consistent formal system $T$ (rich enough to express arithmetic), there exists a true sentence $G_T$ T unprovable IN $T$ . The sentence $G_T$ T becomes provable in a stronger system $T' = T + G_T$ T (or $T + \text{Con}(T)$ ). It is NOT a sentence that is unprovable in every system; it is unprovable in the specific system being considered, but knowable to us via metamathematical reasoning. Godel's theorem is a statement about formal systems, not a metaphysical claim about hidden truths. The popular Penrose-style use of Godel to argue for non-algorithmic intuition rests on a strong philosophical extra premise that most logicians do not accept.

What you now know

You can state Godel's First and Second Incompleteness Theorems, sketch the role of Godel numbering and diagonal self-reference, distinguish independence from outright unknowability, and recognize the Halting Problem as the computational mirror of incompleteness. This concludes the chapter and Garrity's sweep through graduate-level mathematics: from analysis to algebra, complex analysis, set theory, and the foundational limits of formal reasoning itself.

Mark section complete →

References

Garrity, T. (2002). All the Mathematics You Missed: But Need to Know for Graduate School. Cambridge University Press, §10.6.
Godel, K. (1931). "Uber formal unentscheidbare Satze der Principia Mathematica und verwandter Systeme." Monatshefte fur Mathematik und Physik, 38, 173-198.
Smullyan, R. M. (1992). Godel's Incompleteness Theorems. Oxford University Press.
Enderton, H. B. (2001). A Mathematical Introduction to Logic (2nd ed.). Academic Press, ch. 3.
Jech, T. (2003). Set Theory: The Third Millennium Edition. Springer, ch. 14-15 (Forcing and independence).
Hrbacek, K., Jech, T. (1999). Introduction to Set Theory (3rd ed.). CRC Press, ch. 11.