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 for zero.
* A unary function symbol for the successor operation and two binary function symbols + and × for addition and multiplication.
* Three symbols for logical conjunction, , disjunction, , and negation, ¬.
* Two symbols for universal, , and existential, , quantifiers.
* Two symbols for binary relations, = and <, for equality and order (less than).
* Two symbols for left, and right, parentheses for establishing precedence of quantifiers.
* A single variable symbol, and a distinguishing symbol 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 is well formed while 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 such that both and its negation are provable. ω-consistency is a stronger property than consistency. Suppose that is a formula with one free variable . In order to be ω-consistent, the theory cannot prove both while also proving for each natural number .

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 is constructed such that for any two numbers and holds if and only if represents a sequence of formulas that constitutes a proof of the formula that 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'':Hofstadter, D. R. (1979). Gödel, escher, bach. Hassocks, Sussex: Harvester press.

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 . Hence any formula may be correctly recovered from its Gödel number. Let denote the Gödel number of the formula .

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

:

(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

:

translates to "", which is not well-formed.

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

: .

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 has a Gödel number . A second fact that the theory must prove is that given any Gödel number of a formula with one free variable and any number , there is a Gödel number of the formula obtained by replacing all occurrences of in with , and that this second Gödel number can be effectively obtained from the Gödel number of as a function of . To see that this is in fact possible, note that given the Gödel number of , one can recreate the original formula , make the substitution of with , and then find the Gödel number of the resulting formula . 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 , by which one can move from the formulas to a new formula . Then the relation corresponding to this deduction rule says that is related to (in other words, holds) if is the Gödel number of the list of formulas containing and and is the Gödel number of the list of formulas containing , and . Because each deduction rule is concrete, it is possible to effectively determine for any natural numbers and 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: . Let 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 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 . Thus one can define the Gödel number of a proof. Moreover, one may define a statement form , which for every two numbers and is provable if and only if is the Gödel number of a proof of the statement and .

is in fact an arithmetical relation, just as "" is, though a much more complicated one. Given such a relation , for any two specific numbers and , either the formula , or its negation , 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 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 and every formula , where is a free variable, we define , a relation between two numbers and , such that it corresponds to the statement " is not the Gödel number of a proof of ". Here, can be understood as with its own Gödel number as its argument.

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

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

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

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

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

Consider the formula . This formula concerning the number corresponds to "there is no proof of ". 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, says: "I am not provable".

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

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

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

Suppose the negation of , , is provable. Proving both , and , for all natural numbers , violates ω-consistency of the formal theory. Thus if the theory is ω-consistent, 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 or its negation) then they can be manipulated to produce a proof of a contradiction. This makes no appeal to whether 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 in the standard model $\mathbb$ of natural numbers. As just seen, is provable for each natural number , and is thus true in the model $\mathbb$. Therefore, within this model,

: $P(G(P)) = \forall y\,q(y, G(P))$

holds. This is what the statement " 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 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 abbreviate successive applications of the successor function, starting from . Boolos then asserts (the details are only sketched) that there exists a defined predicate that comes out true iff an arithmetic formula containing symbols names the number . This proof sketch contains the only mention of Gödel numbering; Boolos merely assumes that every formula can be so numbered. Here, a formula ''names'' the number if and only if the following is provable:

: $\forall x (F(x) \leftrightarrow x=n)$

Boolos then defines the related predicates:

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

formalizes Berry's paradox. The balance of the proof, requiring but 12 lines of text, shows that the sentence is true for some number , but no algorithm 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.

Citations

External links

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

{{DEFAULTSORT:Proof sketch for Godel's first incompleteness theorem
Mathematical logic
Mathematical proofs