Hilbert hoped that mathematics could be secured by proving, with finitary means, that its formal systems cannot lead to contradiction. Gödel did not merely find a technical limitation; he showed that sufficiently strong formal systems contain truths they cannot prove from within.
Arithmetization of syntax
Gödel's decisive move was to encode formulas, proofs, and provability statements as natural numbers. Once syntax becomes arithmetic, a formal system can speak indirectly about its own proofs.
Definition. A Gödel numbering assigns natural numbers to symbols, formulas, and finite proof sequences so that syntactic relations become arithmetically definable relations.
First incompleteness theorem
Theorem. Every consistent, effectively axiomatized formal system strong enough to express elementary arithmetic is incomplete: there is an arithmetic sentence \(G\) such that neither \(G\) nor \(\neg G\) is provable in the system.
Proof sketch. Using diagonalization, construct a sentence \(G\) that says, in arithmetic coding, "\(G\) is not provable." If the system proved \(G\), it would prove a false claim about its own provability. If it proved \(\neg G\), then under the usual consistency assumptions it would again misrepresent provability.
Second incompleteness theorem
Theorem. Such a system cannot prove its own consistency, provided it is in fact consistent and represents enough arithmetic about proofs.
This struck Hilbert's program at its center. Consistency proofs remain possible, but they must use principles stronger than the system being justified.
What changed
Gödel did not make mathematics irrational. He made formalism more honest. Formal systems are powerful instruments, but no single sufficiently rich system can be both the whole mathematical universe and its own final certificate.
Diagonalization as a historical thread
Gödel's argument belongs to a lineage of diagonal ideas. Cantor diagonalized against lists of real numbers; Russell diagonalized against naive self-membership; Gödel diagonalized against lists of provable statements. In each case, the method builds an object that escapes a proposed total enumeration or classification.
The afterlife of the theorem reaches computability. Church and Turing clarified effective procedure, Tarski separated truth from definability, and proof theory studied which consistency statements can be proved by which stronger systems. Incompleteness therefore became a map of formal strength, not a reason to abandon rigor.
Proof, truth, and computability
Hilbert posed the program of formal security; Gödel transformed logic through incompleteness; Herbrand, Gentzen, Tarski, Church, and Turing extended the surrounding landscape of proof, truth, computability, and formal language.
Arithmetizing syntax
G?del's decisive move was to make formulas and proofs into integers. Assign prime-power codes to finite symbol strings; then relations such as “\(x\) codes a valid proof of the formula coded by \(y\)” become arithmetical. A sufficiently expressive theory can therefore talk about its own formal proofs without adding a semantic truth predicate.
The diagonal lemma states that for every formula \(\varphi(x)\), there is a sentence \(G\) such that \[ T\vdash G\leftrightarrow\varphi(\ulcorner G\urcorner). \] Taking \(\varphi(x)\) to mean “\(x\) is not provable in \(T\)” constructs a sentence asserting its own unprovability.
The two incompleteness theorems
First incompleteness theorem. Every consistent, effectively axiomatized theory strong enough to represent elementary arithmetic is incomplete: there is a sentence \(G\) such that neither \(G\) nor, under the appropriate soundness hypothesis, \(\neg G\) is provable in the theory.
If \(T\vdash G\), then \(T\) also verifies that \(G\) has a proof, contradicting what \(G\) says. If \(T\vdash\neg G\), suitable consistency or \(\omega\)-consistency conditions again conflict with the represented proof relation. Rosser's refinement reduces the hypothesis to ordinary consistency.
Second incompleteness theorem. Under the same effective and expressive hypotheses, a consistent theory \(T\) cannot prove its own formal consistency statement \(\operatorname{Con}(T)\).
Inside \(T\), one proves that \(\operatorname{Con}(T)\) implies its G?del sentence. If \(T\) proved \(\operatorname{Con}(T)\), it would prove \(G\), contradicting the first theorem when \(T\) is consistent.
Hilbert's program after 1931
Incompleteness blocked a universal finitary consistency proof formalizable inside the very system being justified. It did not make proof theory futile. Gentzen proved consistency of Peano arithmetic using transfinite induction up to \(\varepsilon_0\), revealing exactly which extra principle was required. Modern proof theory measures the strength of theories, extracts computational content, and compares formal systems. Hilbert's demand for clarity survived, but the hoped-for absolute endpoint did not.