Kurt Gödel

Kurt Gödel

Logician, 1906–1978. Study focus: effective proof systems, arithmetic encodings, and the precise meanings of completeness.

Gödel proved both a completeness theorem for first-order logic and incompleteness theorems for sufficiently strong arithmetic theories. The results are compatible because they answer different questions. Learning the distinction is more valuable than the slogan that mathematics cannot be certain.

Historical setting

Born in Brno, then in Austria-Hungary, Gödel studied in Vienna under Hans Hahn. His dissertation work established completeness for first-order logic; his 1931 paper established the incompleteness results. He later worked at the Institute for Advanced Study in Princeton. His other research included constructible sets, functional interpretations of arithmetic, and solutions of the equations of general relativity. MacTutor biography, 1931 paper record

This lesson concerns the logical results. Stories about his health, private conversations, or citizenship interview do not explain their proofs. They should not be used to turn his life into a metaphor for an allegedly self-defeating mathematics. Likewise, claims that the theorems establish human superiority over computers go beyond what the mathematical statements prove.

Four definitions that must stay separate

A theory is consistent when it does not prove both a sentence and its negation. It is sound for an intended interpretation when everything it proves is true in that interpretation. Consistency alone does not imply soundness. A theory is syntactically complete when for each sentence it proves that sentence or its negation. Effective axiomatization supplies a mechanical way to enumerate axioms, with an effective proof system.

In a standard modern form incorporating Rosser's strengthening, every consistent effectively axiomatized theory containing sufficient elementary arithmetic is incomplete. Gödel's second theorem concerns a suitable arithmetized consistency statement and sufficiently strong theories satisfying the relevant derivability conditions. A consistent such theory cannot prove that statement about itself. Neither theorem says that every formal system is incomplete. Precise statements and hypotheses

Consider the original teaching theory consisting of one propositional axiom p with ordinary classical inference. It is consistent, and it is sound in valuations where p is true. It is not sound in the valuation where p is false. This elementary example already refutes the inference “no contradiction, therefore all statements are true in the intended world.” We need not invoke any sophisticated arithmetic to see the distinction.

Worked mechanism: encode syntax as arithmetic

Assign symbol codes 0↦1, =↦2, and S↦3. For a nonempty symbol sequence with positive codes a1,...,an, define its code as 2^a1 × 3^a2 × ... × pn^an, using consecutive primes. Reserve 1 for the empty sequence. This is an original simplified encoding, not Gödel's exact historical numbering.

Then 0=0 has code 2^1×3^2×5^1=90. The sequence S0=0 has code 2^3×3^1×5^2×7^1=4200. Unique prime factorization recovers the sequence: the exponents of 2, 3, 5, and 7 are 3, 1, 2, and 1. Positive exponents ensure an unambiguous end. A number with a missing intermediate prime can be rejected as an invalid sequence code.

Encoding does not make every string a formula or every formula a theorem. The parser still checks the grammar. A proof checker still checks that each line is an axiom or follows by a permitted inference. The crucial further work is to represent such finite syntactic computations within arithmetic. The integer is a representation of the text, not a magical statement about its truth.

Finding a proof versus checking a proof

Suppose a proof checker terminates on every finite candidate proof. Enumerate candidate strings by length and then lexicographic order, check each, and print the conclusions of valid proofs. Every finite proof eventually appears. Therefore this procedure eventually finds a proof of any theorem in that system.

If a proposed statement is not a theorem, however, searching longer has no built-in stopping rule. At every stage a longer proof might remain. This does not contradict effective proof checking: checking a supplied certificate and deciding whether any certificate exists are different tasks.

For a finite example, imagine that proofs of length at most three have been exhausted without finding q. That establishes only a bounded result. It does not establish that q lacks a proof of length four or four million. A theorem can justify a finite search bound in a restricted problem, but the bound must be proved, not inferred from impatience.

What diagonalization adds

An arithmetized provability predicate expresses that some number encodes a proof of a given formula. A diagonal or fixed-point construction produces a sentence related to its own provability. This is not accomplished by writing an informal English liar sentence. The proof must establish that substitution and proof checking are representable and then use the specified assumptions about the theory.

Adding a previously undecidable sentence as an axiom can settle that sentence in an extended theory. If the extension remains consistent, effective, and arithmetically strong, the theorem applies again. The new undecidable sentence belongs to the new theory's situation. “Unprovable” is relative to a particular theory, not a claim that no mathematical argument could ever discuss the sentence. Diagonalization and extensions

Why completeness is still possible

Semantic completeness of first-order logic says: if a sentence follows in every model of a collection of axioms, there is a formal derivation from those axioms. Incompleteness of arithmetic says that a particular effective theory cannot decide every arithmetic sentence. Its axioms can have models that disagree on a sentence even though the intended natural numbers assign that sentence a definite truth value. The two quantifications are different.

A useful finite analogy is an axiom saying “exactly one of p and q holds.” Its models include (true,false) and (false,true). A sound and complete proof calculus cannot derive p from that axiom, because p is false in the second model. That failure to derive p is a feature of the calculus, not a defect. The analogy clarifies semantic consequence; it is not a proof of arithmetic incompleteness.

Formal verification remains useful. One can prove a particular sorting implementation correct relative to a specification, arithmetic model, and proof system. Gödel's theorem does not turn every such proof into an unresolved philosophical problem. It warns against promising one effective, consistent, sufficiently strong system that settles everything.

Exercises

1. Under the encoding above, decode 2^3×3^3×5^1×7^2×11^1. Does a valid decoding by itself establish a true equation?
2. Explain why a prover that has checked all proofs up to length 1000 cannot generally return “false” merely because it has not proved a sentence. Distinguish false, unproved, and refuted.
3. A consistent effective arithmetic theory T cannot decide A. A researcher adds A as an axiom, obtaining a consistent T', and claims incompleteness has been defeated. Identify what changed and what theorem still applies.

Compare your reasoning with the worked solutions

1. The exponent sequence is 3,3,1,2,1, decoding to SS0=0. Under the usual successor interpretation, this says 2 equals 0 and is false. It remains a well-formed equation. Coding, parsing, and semantic evaluation are distinct stages; the existence of an integer encoding is not evidence of truth.
2. The search proves only the absence of a proof within the chosen length bound. “Unproved” describes the search's current result; “refuted” requires a proof of the negation in the specified theory; “false” concerns an interpretation. A longer proof may exist, or neither side may be derivable. An honest bounded prover reports its bound or an unknown outcome unless it has additional justified reasoning.
3. A is now trivially provable in T', but the axiom set has changed. Because the extension is assumed consistent and remains effective and sufficiently strong, another sentence is undecidable in T'. This does not mean the same sentence stays undecidable after becoming an axiom. The theorem concerns each system under its own axioms and proof relation.