Symbolic Logic:

Curtis Brown

This is a quick overview of some of the high points of Gdel's first incompleteness theorem. My presentation closely follows that in Ernest Nagel and James R. Newman, Gdel's Proof (New York: NYU Press, 1958; Revised Edition, ed. Douglas R. Hofstadter, 2001).

We've discussed the fact that we can add axioms to FOL to capture logical relations between predicates (and functions) that are not themselves included in FOL, such as adding axioms for shape to the Tarski's World language. Gdel showed that if we do this for the arithmetic of the natural numbers, no set of axioms can possibly be complete (in the sense that there will necessarily be true propositions about the natural numbers which are not consequences of the axioms).  [It should be noted that this is a different sense of the word "incomplete" than when we say that FOL is complete. To say that a deductive system for FOL is complete is to say that whenever a conclusion is a first-order consequence of a set of premises, it is derivable from those premises using the deductive system.]

One set of axioms for the arithmetic of the natural numbers, a version of the Peano axioms, is given in our text (section 16.4). Gdel uses a slightly different version of the Peano axioms.  His version involves two axioms, an axiom schema, and recursive definitions of + and * (addition and multiplication). The axioms and axiom schema are:

x (s(x) = 0)
xy ((s(x) = s(y)) x = y)
(0) x (Φ(x) Φ(s(x)))) xΦ(x)

The first axiom says that 0 is not the successor of any number; the second says that if the successor of x is the same as the successor of y, then x = y; and the third is a schema, an instance of which would substitute a particular formula for the placeholder Φ

Then addition and multiplication are introduced by recursive definitions. For addition, we have:

x + 0 = x
x + s(y) = s(x + y)

(This definition is regarded as a recipe for translating a statement about addition into the official language of FOL plus the name '0' and the function symbol 's'.  If we wanted to, we could instead also add the symbol '+' to the official language, close the two clauses of the recursive definition above with universal quantifiers, and regard them as axioms.  Similar remarks hold for the definition of multiplication to follow.)

For multiplication, we have:

x * 0 = 0
x * s(y) = (x * y) + x

(In a way, the precise details of the axioms do not matter all that much, because Gdel's incompleteness theorem gives a recipe for finding a true but unprovable sentence of arithmetic for any consistent set of axioms that allow the derivation of some basic arithmetic facts. Since any adequate set of axioms for arithmetic would need to allow the derivation of these basic facts plus a lot more, he shows that every consistent set of axioms that has any hope of capturing the truths of arithmetic will be incomplete.)

Gdel's proof depends on the fact that we can associate with every sentence, and sequence of sentences of FOL (plus '0' and 's') a natural number, its "Gdel number," in such a way that we can also, given a Gdel number, determine the sentence it is the Gdel number (GN) of. (So we have a function from sentences and sequences of sentences into the natural numbers, and a partial function from the natural numbers into sentences and sequences of sentences in FOL.)

Here is one strategy for Gdel numbering (following Nagel and Newman's presentation). This involves assigning numbers to symbols in the language of FOL, as follows:

symbol code number
= 5
0 6
s 7
( 8
) 9
, 10
x 11
y 13
z 17

Symbols that are not explicitly included can be defined in terms of those that are; e.g. 'x' can be replaced by 'x'; 'P Q' can be replaced by '(P Q)', and '+' and '*' can be replaced according to the recursive definitions above. (Gdel also includes numbers for propositional and predicate variables but I have not included those: first-order languages do not include such variables, and Gdel's result can also be obtained for first-order languages.)

Now, we can think of a formula as a sequence of characters: c1, c2, . . ., cn. Each of these characters has an associated code number, as given in the table above; call these g1, g2, . . ., gn.  Then the Gdel Number of the formula is 2g1 * 3g2 * . . . * pngn, where pn is the nth prime number.

We can repeat the same trick to get the "super-Gdel number" of a sequence of n formulas: just take the first n primes, raise them to the powers of the GN's of the n formulas, and multiply the results to get the SGN of the sequence.

Now one crucial thing Gdel shows, which for our purposes we pretty much just need to accept on faith, is that various metamathematical relations between sentences of FOL correspond to purely arithmetic relations between GN's. Gdel defines, in particular, the following purely arithmetic relation between Gdel numbers: 

Dem(x, z)

which is true of two natural numbers x and z just in case x is the GN of a sequence of sentences which constitutes a proof of the sentence of which z is the GN.

He also defines the function 

sub(x, y, z) 

which takes three natural numbers as arguments and returns a natural number as its value.  The number it returns is the GN of the formula that results from starting with the formula with GN x, and replacing any occurrence in that formula of the element with GN y by (the standard numeral for) the natural number z.

Now we notice that formula 

Dem(x, z)

essentially says that the sequence of sentences with GN x is not a proof of the sentence with GN z, and so

x Dem(x, z)

amounts to the claim that there is no proof of the sentence with GN z.

Now we consider the following formula (not a sentence, since the occurrences of y are not bound by a quantifier):

(1)     x Dem(x, sub(y, 13, y))

This formula says that there is no proof of the sentence which results from taking the formula with GN y, and replacing the element with GN 13 (which happens to be the variable 'y') with the standard numeral for the number y.

Now, (1) has a GN (or rather, its translation into FOL plus '+' and '0' has a GN).  Call this GN n. And in the language of FOL plus '0' and 's', there is a standard numeral that stands for n. (For example, if n were the number 3, then the standard numeral would be s(s(s(0))).) Let's call this standard numeral for the GN of the formula (1) n.

Now we consider this sentence:

(G)     x Dem(x, sub(n, 13, n))

This "says that" there is no proof of the sentence that results from taking the formula with GN n and replacing all occurrences of 'y' (the element with GN 13) by the standard numeral for the number n, that is, by n. (It doesn't literally "say this," of course: it's just a sentence about mathematical relations between natural numbers.)

But what sentence is it that results from that operation? What sentence is sub(n, 13, n) the GN of?  Well, n is the GN of (1) above.  So sub(n, 13, n) is the GN of the sentence that results from taking (1) and replacing every occurrence of 'y' by n.

But that sentence just is (G)! So in effect (G) "says that" there is no proof of (G).

Now, if we could prove (G) in our formal system, then at least one of the axioms we started with would have to be false. (This is because, since (G) is true if and only if it's not provable, then if we could prove it, it would have to be false. Since FO logic is sound, if you start with true axioms, you can't prove a falsehood. So if we could prove (G), and it was false, then the axioms couldn't all be true.) So if the axioms are true, then we cannot prove (G) from them.

[An aside: Gdel actually shows something even stronger, but trickier to prove. He doesn't assume that the axioms are true, but only that they are consistent (or more precisely, ω-consistent), and he shows that even on that more minimal assumption neither G nor ~G can be proven, so that the axioms are incomplete.]

But if we cannot prove (G) in the system, then what (G) says is true! (Well, not exactly "what it says": (G), recall, is really just a complicated sentence in FOL supplemented by the successor function and a name for 0. Remember that Dem(x,y) and sub(x,y,z) are just abbreviations for a relation and a function expressed in that language. So what (G) actually says is something about the arithmetic of the natural numbers. But given the way Gdel has defined Dem and sub, (G) is true if and only if there is no proof of (G).) So we have a proof that there is at least one sentence expressible in the language of our formal system which is true but not provable.

(Want to see the details? One more-or-less accessible presentation that works through nearly all the details of defining Dem(x, y), sub(x, y, z), etc. is Christopher C. Leary, A Friendly Introduction to Mathematical Logic (Prentice-Hall, 2000). However, the system of Gdel numbering Leary uses is rather different from the one given in Nagel and Newman and on this page. Another excellent introduction which provides nearly all the gory details is Peter Smith, An Introduction to Gdel's Theorems (Cambridge: Cambridge University Press, 2007). If you have the urge to consult Gdel's original paper in German, here is a reference: "ber formal unentscheidbare Stze der Principia Mathematica und verwandter Systeme I,"  Monatshefte fr Mathematik und Physik, v.38, p.173-198 (1931). This is also available in English translation: On formally undecidable propositions of Principia mathematica and related systems. Translated by B. Meltzer. With introd. by R. B. Braithwaite. New York:  Basic Books, 1962. A number of other related books can be found in the library by searching under the subject heading "Gdel's theorem.")

Last update: April 29, 2013. 
Curtis Brown | Symbolic Logic | Philosophy Department | Trinity University