Proof sketch for Gödel's first incompleteness theorem

This article gives a sketch of a proof of Gödel's first incompleteness theorem. This theorem applies to any formal theory that satisfies certain technical hypotheses, which are discussed as needed during the sketch. We will assume for the remainder of the article that a fixed theory satisfying these hypotheses has been selected.

Throughout this article the word "number" refers to a natural number (including 0). The key property these numbers possess is that any natural number can be obtained by starting with the number 0 and adding 1 a finite number of times.

Hypotheses of the theory

Gödel's theorem applies to any formal theory that satisfies certain properties. Each formal theory has a signature that specifies the nonlogical symbols in the language of the theory. For simplicity, we will assume that the language of the theory is composed from the following collection of 15 (and only 15) symbols:

• A constant symbol Template:Math for zero.
• A unary function symbol Template:Math for the successor operation and two binary function symbols + and × for addition and multiplication.
• Three symbols for logical conjunction, Template:Math, disjunction, Template:Math, and negation, ¬.
• Two symbols for universal, Template:Math, and existential, Template:Math, quantifiers.
• Two symbols for binary relations, = and <, for equality and order (less than).
• Two symbols for left, Template:Math and right, Template:Math parentheses for establishing precedence of quantifiers.
• A single variable symbol, Template:Math and a distinguishing symbol Template:Math that can be used to construct additional variables of the form x*, x**, x***, ...

This is the language of Peano arithmetic. A well-formed formula is a sequence of these symbols that is formed so as to have a well-defined reading as a mathematical formula. Thus Template:Math is well formed while Template:Math is not well formed. A theory is a set of well-formed formulas with no free variables.

A theory is consistent if there is no formula Template:Math such that both Template:Math and its negation are provable. ω-consistency is a stronger property than consistency. Suppose that Template:Math is a formula with one free variable Template:Math. In order to be ω-consistent, the theory cannot prove both Template:Math while also proving Template:Math for each natural number Template:Math.

The theory is assumed to be effective, which means that the set of axioms must be recursively enumerable. This means that it is theoretically possible to write a finite-length computer program that, if allowed to run forever, would output the axioms of the theory (necessarily including every well-formed instance of the axiom schema of induction) one at a time and not output anything else. This requirement is necessary; there are theories that are complete, consistent, and include elementary arithmetic, but no such theory can be effective.

Outline of the proof

The sketch here is broken into three parts. In the first part, each formula of the theory is assigned a number, known as a Gödel number, in a manner that allows the formula to be effectively recovered from the number. This numbering is extended to cover finite sequences of formulas. In the second part, a specific formula Template:Math is constructed such that for any two numbers Template:Math and Template:Math holds if and only if Template:Math represents a sequence of formulas that constitutes a proof of the formula that Template:Math represents. In the third part of the proof, we construct a self-referential formula that, informally, says "I am not provable", and prove that this sentence is neither provable nor disprovable within the theory.

Importantly, all the formulas in the proof can be defined by primitive recursive functions, which themselves can be defined in first-order Peano arithmetic.

Gödel numbering

The first step of the proof is to represent (well-formed) formulas of the theory, and finite lists of these formulas, as natural numbers. These numbers are called the Gödel numbers of the formulas.

Begin by assigning a natural number to each symbol of the language of arithmetic, similar to the manner in which the ASCII code assigns a unique binary number to each letter and certain other characters. This article will employ the following assignment, very similar to the one Douglas Hofstadter used in his Gödel, Escher, Bach:

Number Symbol Meaning 666 0 zero 123 Template:Math successor function 111 = equality relation 212 < less than relation 112 + addition operator 236 × multiplication operator 362 ( left parenthesis 323 ) right parenthesis

Number Symbol Meaning 262 Template:Math a variable name 163 * star (used to make more variables) 333 ∃ existential quantifier 626 ∀ universal quantifier 161 ∧ logical and 616 ∨ logical or 223 ¬ logical not

The Gödel number of a formula is obtained by concatenating the Gödel numbers of each symbol making up the formula. The Gödel numbers for each symbol are separated by a zero because by design, no Gödel number of a symbol includes a Template:Math. Hence any formula may be correctly recovered from its Gödel number. Let Template:Math denote the Gödel number of the formula Template:Math.

Given the above Gödel numbering, the sentence asserting that addition commutes, Template:Math translates as the number:

Template:Math

(Spaces have been inserted on each side of every 0 only for readability; Gödel numbers are strict concatenations of decimal digits.) Not all natural numbers represent a sentence. For example, the number

Template:Math

translates to "Template:Math", which is not well-formed.

Because each natural number can be obtained by applying the successor operation Template:Math to Template:Math a finite number of times, every natural number has its own Gödel number. For example, the Gödel number corresponding to Template:Math, is:

Template:Math.

The assignment of Gödel numbers can be extended to finite lists of formulas. To obtain the Gödel number of a list of formulas, write the Gödel numbers of the formulas in order, separating them by two consecutive zeros. Since the Gödel number of a formula never contains two consecutive zeros, each formula in a list of formulas can be effectively recovered from the Gödel number for the list.

It is crucial that the formal arithmetic be capable of proving a minimum set of facts. In particular, it must be able to prove that every number Template:Math has a Gödel number Template:Math. A second fact that the theory must prove is that given any Gödel number Template:Math of a formula Template:Math with one free variable Template:Math and any number Template:Math, there is a Gödel number of the formula Template:Math obtained by replacing all occurrences of Template:Math in Template:Math with Template:Math, and that this second Gödel number can be effectively obtained from the Gödel number Template:Math of Template:Math as a function of Template:Math. To see that this is in fact possible, note that given the Gödel number of Template:Math, one can recreate the original formula Template:Math, make the substitution of Template:Math with Template:Math, and then find the Gödel number Template:Math of the resulting formula Template:Math. This is a uniform procedure.

The provability relation

Deduction rules can then be represented by binary relations on Gödel numbers of lists of formulas. In other words, suppose that there is a deduction rule Template:Math, by which one can move from the formulas Template:Math to a new formula Template:Math. Then the relation Template:Math corresponding to this deduction rule says that Template:Math is related to Template:Math (in other words, Template:Math holds) if Template:Math is the Gödel number of the list of formulas containing Template:Math and Template:Math and Template:Math is the Gödel number of the list of formulas containing Template:Math, Template:Math and Template:Math. Because each deduction rule is concrete, it is possible to effectively determine for any natural numbers Template:Math and Template:Math whether they are related by the relation.

The second stage in the proof is to use the Gödel numbering, described above, to show that the notion of provability can be expressed within the formal language of the theory. Suppose the theory has deduction rules: Template:Math . Let Template:Math be their corresponding relations, as described above.

Every provable statement is either an axiom itself, or it can be deduced from the axioms by a finite number of applications of the deduction rules. A proof of a formula Template:Math is itself a string of mathematical statements related by particular relations (each is either an axiom or related to former statements by deduction rules), where the last statement is Template:Math. Thus one can define the Gödel number of a proof. Moreover, one may define a statement form Template:Math, which for every two numbers Template:Math and Template:Math is provable if and only if Template:Math is the Gödel number of a proof of the statement Template:Math and Template:Math.

Template:Math is in fact an arithmetical relation, just as "Template:Math" is, though a much more complicated one. Given such a relation Template:Math, for any two specific numbers Template:Math and Template:Math, either the formula Template:Math, or its negation Template:Math, but not both, is provable. This is because the relation between these two numbers can be simply "checked". Formally this can be proven by induction, where all these possible relations (whose number is infinite) are constructed one by one. The detailed construction of the formula Template:Math makes essential use of the assumption that the theory is effective; it would not be possible to construct this formula without such an assumption.

Self-referential formula

For every number Template:Math and every formula Template:Math, where Template:Math is a free variable, we define Template:Math, a relation between two numbers Template:Math and Template:Math, such that it corresponds to the statement "Template:Math is not the Gödel number of a proof of Template:Math". Here, Template:Math can be understood as Template:Math with its own Gödel number as its argument.

Note that Template:Math takes as an argument Template:Math, the Gödel number of Template:Math. In order to prove either Template:Math, or Template:Math, it is necessary to perform number-theoretic operations on Template:Math that mirror the following steps: decode the number Template:Math into the formula Template:Math, replace all occurrences of Template:Math in Template:Math with the number Template:Math, and then compute the Gödel number of the resulting formula Template:Math.

Note that for every specific number Template:Math and formula Template:Math is a straightforward (though complicated) arithmetical relation between two numbers Template:Math and Template:Math, building on the relation Template:Math defined earlier. Further, Template:Math is provable if the finite list of formulas encoded by Template:Math is not a proof of Template:Math, and Template:Math is provable if the finite list of formulas encoded by Template:Math is a proof of Template:Math. Given any numbers Template:Math and Template:Math, either Template:Math or Template:Math (but not both) is provable.

Any proof of Template:Math can be encoded by a Gödel number Template:Math, such that Template:Math does not hold. If Template:Math holds for all natural numbers Template:Math, then there is no proof of Template:Math. In other words, Template:Math, a formula about natural numbers, corresponds to "there is no proof of Template:Math".

We now define the formula Template:Math, where Template:Math is a free variable. The formula Template:Math itself has a Gödel number Template:Math as does every formula.

This formula has a free variable Template:Math. Suppose we replace it with Template:Math, the Gödel number of a formula Template:Math, where Template:Math is a free variable. Then, Template:Math corresponds to "there is no proof of Template:Math", as we have seen.

Consider the formula Template:Math. This formula concerning the number Template:Math corresponds to "there is no proof of Template:Math". We have here the self-referential feature that is crucial to the proof: A formula of the formal theory that somehow relates to its own provability within that formal theory. Very informally, Template:Math says: "I am not provable".

We will now show that neither the formula Template:Math, nor its negation Template:Math, is provable.

Suppose Template:Math is provable. Let Template:Math be the Gödel number of a proof of Template:Math. Then, as seen earlier, the formula Template:Math is provable. Proving both Template:Math and Template:Math violates the consistency of the formal theory. We therefore conclude that Template:Math is not provable.

Consider any number Template:Math. Suppose Template:Math is provable. Then, Template:Math must be the Gödel number of a proof of Template:Math. But we have just proved that Template:Math is not provable. Since either Template:Math or Template:Math must be provable, we conclude that, for all natural numbers Template:Math is provable.

Suppose the negation of Template:Math, Template:Math, is provable. Proving both Template:Math, and Template:Math, for all natural numbers Template:Math, violates ω-consistency of the formal theory. Thus if the theory is ω-consistent, Template:Math is not provable.

We have sketched a proof showing that:

For any formal, recursively enumerable (i.e. effectively generated) theory of Peano Arithmetic,

if it is consistent, then there exists an unprovable formula (in the language of that theory).

if it is ω-consistent, then there exists a formula such that both it and its negation are unprovable.

The truth of the Gödel sentence

The proof of Gödel's incompleteness theorem just sketched is proof-theoretic (also called syntactic) in that it shows that if certain proofs exist (a proof of Template:Math or its negation) then they can be manipulated to produce a proof of a contradiction. This makes no appeal to whether Template:Math is "true", only to whether it is provable. Truth is a model-theoretic, or semantic, concept, and is not equivalent to provability except in special cases.

By analyzing the situation of the above proof in more detail, it is possible to obtain a conclusion about the truth of Template:Math in the standard model $\mathbb{N}$ of natural numbers. As just seen, Template:Math is provable for each natural number Template:Math, and is thus true in the model $\mathbb{N}$. Therefore, within this model,

$P(G(P))=\mathrm{\forall }yq(y,G(P))$

holds. This is what the statement "Template:Math is true" usually refers to—the sentence is true in the intended model. It is not true in every model, however: If it were, then by Gödel's completeness theorem it would be provable, which we have just seen is not the case.

Boolos's short proof

George Boolos (1989) vastly simplified the proof of the First Theorem, if one agrees that the theorem is equivalent to:

"There is no algorithm Template:Math whose output contains all true sentences of arithmetic and no false ones."

"Arithmetic" refers to Peano or Robinson arithmetic, but the proof invokes no specifics of either, tacitly assuming that these systems allow '<' and '×' to have their usual meanings. Boolos proves the theorem in about two pages. His proof employs the language of first-order logic, but invokes no facts about the connectives or quantifiers. The domain of discourse is the natural numbers. The Gödel sentence builds on Berry's paradox.

Let Template:Math abbreviate Template:Math successive applications of the successor function, starting from Template:Math. Boolos then asserts (the details are only sketched) that there exists a defined predicate Template:Math that comes out true iff an arithmetic formula containing Template:Math symbols names the number Template:Math. This proof sketch contains the only mention of Gödel numbering; Boolos merely assumes that every formula can be so numbered. Here, a formula Template:Mathnames the number Template:Math iff the following is provable:

$\mathrm{\forall }x(F(x)\leftrightarrow x=n)$

Boolos then defines the related predicates:

• Template:Math. (English: Template:Math comes out true if Template:Math can be defined in fewer than Template:Math symbols):
• Template:Math. (English: Template:Math comes out true if Template:Math is the smallest number not definable in fewer than Template:Math symbols. More awkwardly, Template:Math holds if Template:Math cannot be defined in fewer than Template:Math symbols, and all numbers less than Template:Math can be defined using fewer than Template:Math symbols);
• Template:Math. Template:Maththe number of symbols appearing in Template:Math.

Template:Math formalizes Berry's paradox. The balance of the proof, requiring but 12 lines of text, shows that the sentence Template:Math is true for some number Template:Math, but no algorithm Template:Math will identify it as true. Hence in arithmetic, truth outruns proof. QED.

The above predicates contain the only existential quantifiers appearing in the entire proof. The '<' and '×' appearing in these predicates are the only defined arithmetical notions the proof requires. The proof nowhere mentions recursive functions or any facts from number theory, and Boolos claims that his proof dispenses with diagonalization. For more on this proof, see Berry's paradox.

References

• 1931, "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I." Monatshefte für Mathematik und Physik 38: 173–98.
• English translations of the preceding:
  • Jean van Heijenoort, 1967. From Frege to Gödel: A Source Book on Mathematical Logic. Harvard University Press: 596–616.
  • Hirzel, Martin (trans.), 2000, "On formally undecidable propositions of Principia Mathematica and related systems I.".
• 1951, "Some basic theorems on the foundations of mathematics and their implications" in Solomon Feferman, ed., 1995. Collected works / Kurt Gödel, Vol. III. Oxford University Press: 304–23.
• George Boolos, 1998, "A New Proof of the Gödel Incompleteness Theorem" in Boolos, G., Logic, Logic, and Logic. Harvard Univ. Press.

External links

• A concise proof of Gödel's Incompleteness Theorem.