An Exposition of Goedel's Incompleteness Theorems by John E. Doner UCSB Math. Dept. doner@math.ucsb.edu October 12, 1998 Goedel discussed the formal system presented in Whitehead & Russell's book, but I'll replace that here by first-order Peano's Arithmetic, PA. This is a first-order formal system with a fairly simple set of axioms. These axioms are given in an appendix to this document. The syntax of the formal language for PA has a finite alphabet A, E, |, &, ~, -->, <-->, =, V, ', (, ), <, 0, S, +, *. I intend to use A for "for all", E for "there exists", | for "or", & for "and", ~ for "not", --> for "implies", <--> for "iff", etc. A first-order language needs infinitely many formal variables. To manufacture symbols for these using only a finite alphabet, I use V and ' together: the variables are V, V', V'', V''', ... . But for convenience, I'll use letters u,v,w,x,y,z,... to represent any of these formal variables. You're expected to understand first-order logical formalisms, that x <= y abbreviates ~(y < x), the precedence of symbols, that sometimes + stands for the formal symbol and sometimes it's the real-world "plus" (what else can I do in ASCII?), and much else. But you can probably infer most of these details from what I write. Get a text on mathematical logic if being hazy on some of this troubles you. The simplest expressions in the language of PA are the notations for numbers. Among the symbols of PA are S (for the successor function) and 0 for the number zero. These symbols provide a notation for each natural number, and we call that notation the numeral for the number. I'll use # to signify numerals: #0 is 0, the numeral for zero, and for each natural number n, the numeral for the next number is S(#n). So for example, the numeral for 4 is S(S(S(S(0)))), and we denote it by #4. Now let's look at some examples of formulas. Here's a formula expressing the idea "x is prime": 0 < x & (Ay)(Az)(x = y*z --> y = #1 | y = x) (Remember, #1 abbreviates S(0).) To read it aloud, you say "zero less than x and for all y and z, if x equals y times z then y equals one or y equals x". We'll call that formula Prime(x). Now here's the Goldbach Conjecture: (Ax)((Ey)(x = y+y) & 0 < x --> (Ey)(Ez)(Prime(y) & Prime(z) & x = y+z)) The notation PA |-- F, where F is some formula, is read "PA proves F", and it expresses the idea that there is a proof in the system PA of the formula F. Such a proof is a finite sequence of formulas ending with F, in which each formula is either an axiom or follows from previous ones by a rule of inference. |-- is called the "provability sign". (Again, if any of this troubles you, check that book on logic.) Now Goedel showed that many interesting functions and predicates and relations of arithmetic can be represented inside PA. For example, the number theoretic predicate "prime" is represented by the formula Prime(x): for each n, n is prime implies PA |-- Prime(#n) n not prime implies PA |-- ~Prime(#n) The formulation of representability is slightly different in the case of functions. The exponential function, m^n, isn't included among the primitives of PA. But there is a representing formula Exp(x, y, z) such that for all m, n, p with p = m^n, PA |-- Exp(#m, #n, y) <--> y = #p And so on. In fact, every primitive recursive function is represented in PA this way. (Primitive recursive functions are, intuitively, those which are computable by programs in a minimal programming language, with only the integer data type, assignments to variables, if-then-else, and a simple FORTRAN-style looping construct that allows repetition of a loop body a number of times given in advance of entry; no while, repeat, goto, arrays, pointers, etc.) To illustrate Goedel numbering, let's look at a simple language with only three letters: a,b,c. A word in this language is any sequence of letters, e.g., baabcac. We can adopt any of various systems to code words by numbers. One way would be to regard each letter as a non-zero digit in the base 4 system. Another would be to just number the letters, 1 for a, 2 for b, 3 for c, and then use prime number decompositions: the code for baabcac is 2^2 * 3^1 * 5^1 * 7^2 * 11^3 * 13^1 * 17^3 (This encoding tends to yield bigger numbers than the first method. So what?) We call this number the Goedel number of the word baabcac. The Goedel number of a word w is denoted by [w]. Sometimes we need to talk about sequences of words. We can handle this just by adding another letter, the comma, and then [w_1,w_2,...,w_n] is the Goedel number of the sequence w_1,w_2,...,w_n. Choose some Goedel numbering for the expressions of the language of PA. Given a formula F, its Goedel number is [F]. A PA-proof of F is a sequence of formulas G_1,G_2,...,G_n, with G_n = F, and has a Goedel number [G_1,G_2,...,G_n]. All the usual syntactic operations on formulas and proofs translate to operations on Goedel numbers. What's more, these operations turn out to be primitive recursive, and therefore representable. Thus, there is a formula Sub(w, x, y, z) representing the substitution operation, whereby a term is substituted for a variable in a formula. For example, if G(x) is Prime(x) and F is Prime(#3), then PA |-- Sub(#[G], #[x], #[#3]), z) <--> z = #[F] (Confused by #[#3]? Well, #3 is the numeral for the number three. #3 is the term S(S(S(0))), an expression in the language. It has a Goedel number, [#3]. This number has a numeral, denoted by #[#3]. Therefore, #[#3] is an expression S(S(S(S( ... S(0) ... )))) where the ... stands for some astronomical number of S's.) It's convenient to use a more specialized substitution operation, that of substituting the numeral for a given number for the first free variable in a formula. I call this operation sbn and the formula representing it Sbn (for "substitute numeral"). We have, for any number n and formula H(x), sbn([H(x)],n) = [H(#n)] and PA |-- Sbn(#[H(x)], #n, y) <--> y = #[H(#n)] The key to Goedel's proof is the following Diagonal Lemma: For any formula F(x) with one free variable x, there is a formula G such that PA |-- G <--> F(#[G]) In informal language, PA proves the equivalence of G with the property F applied to the Goedel number of G. The proof of the Diagonal Lemma is easy (once you've seen it already!): Given F(x), let H(x) be the following formula: (Ay)(Sbn(x, x, y) --> F(y)) Let m = [H(x)]. Let G be the formula H(#m). So we have PA |-- G <--> (Ay)(Sbn(#m, #m, y) --> F(y)) Since m = [H(x)], we know that PA |-- Sbn(#m, #m, y) <--> y = #[H(#m)] Thus, PA |-- G <--> F(#[H(#m)]) But G is H(#m). Q.E.D. On to Incompleteness! All the syntactic notions about proofs can be translated into statements about Goedel numbers, leading to primitive recursive functions and predicates that are representable in PA. For example, there is a formula Prf(x, y) such that if m is the Goedel number of a proof of the formula with Goedel number n, then PA |-- Prf(#m, #n) if m is not the Goedel number of a proof of the formula with Goedel number n, then PA |-- ~Prf(#m, #n) It gets tiresome to keep saying "Goedel number of", so in what follows we'll often abbreviate statements like the above to if m is a proof of n, then PA |-- Prf(#m, #n) if m is not a proof of n, then PA |-- ~Prf(#m, #n) (Why don't I just say m is a proof of n iff PA |-- Prf(#m,#n)? Because I want to allow for the possibility that PA is actually inconsistent. I don't know anyone who doubts the consistency of PA, but, hey, this is mathematics! If PA were inconsistent, then it could prove anything at all.) Pr(x), read "x is provable", is the formula (Ey)Prf(y, x) So if we're given a formula F, then decoding all the Goedel numbers, and going through the intended meanings of all the defined formulas, the INTUITIVE meaning of Pr(#[F]) is "F is provable in PA". Actually, though, Pr(#[F]) is just some long formula in the theory of arithmetic making a complicated combinatorial statement about a certain natural number. Now let F be the formula ~Pr(x). Using the Diagonal Lemma, we get a formula G such that PA |-- G <--> ~Pr(#[G]) Now suppose PA |-- G. Then there must be an actual proof, G_1,G_2,...,G_n with G_n = G. Let m = [G_1,G_2,...,G_n]. We have PA |-- Prf(#m, #[G]) and hence PA |-- Pr(#[G]) But from PA |-- G it also follows that PA |-- ~Pr(#[G]) We know (firmly believe?) that PA is consistent, so we conclude that PA |-- G is not true---PA does not prove G, and there is no sequence of formulas G_1,G_2,...,G_n which is a proof of G. Ah, but the intuitive meaning of G is "G is not provable". So, if PA is consistent, then G is both unprovable and true. We have thus proved the FIRST INCOMPLETENESS THEOREM --- Part I If PA is consistent, then there is a true but unprovable formula of PA. Part II of the First Incompleteness Theorem asserts that ~G isn't provable either. It requires a stronger assumption than ordinary consistency. A theory T is w-consistent (read "omega-consistent"; that w is Greek!) if there's no formula F for which this happens: T |-- (Ex)F(x) for each n, T |-- ~F(#n) i.e., T mustn't say on the one hand that there exists something with a certain property, and then on the other hand deny that property to every natural number n. Suppose PA is w-consistent. Suppose PA |-- ~G. Then PA |-- Pr(#[G]) i.e., PA |-- (Ey)Prf(y, #[G]) Now consider any n: it's either a (Goedel number of) a proof of G, or it isn't. So either PA |-- Prf(#n, #[G]) or else PA |-- ~Prf(#n, #[G]). We know the first case doesn't hold (remember---G isn't provable), so the second does hold. We conclude for each n, PA |-- ~Prf(#n, #[G]) All this would imply that PA is not w-consistent. Thus, we have proved FIRST INCOMPLETENESS THEOREM --- Part II If PA is w-consistent, then there is a formula G such that neither G nor ~G is provable. Exercise (Rosser): The same thing is provable without w-consistency. (Hint: The original G intuitively meant something like "I am not provable." Try to find a formula that says "if I am provable, then there is a smaller proof of my negation." You'll need Neg, a formula representing the primitive recursive function neg such that for any formula F, neg([F]) = [~F].) Goedel's Second Incompleteness theorem asserts that a consistent theory embedding PA cannot prove naturally constructed statements of its own consistency. Note that PA |-- F <--> #0=#1 for any refutable sentence F, so we can use #0=#1 (which is just 0=S(0)) as a canonical refutable sentence. Let Con be the sentence ~Pr(#[0=S(0)]) Con has the intuitive meaning "there is no proof in PA of the sentence 0=S(0)". The Second Incompleteness Theorem states, assuming PA is consistent, PA !|-- Con (The "!|--" means "not provable".) Proving this theorem involves, effectively, redoing the proof of the First Incompleteness Theorem (F.I.T.) inside PA. The logician's buzz-word for this process is "formalization." The F.I.T. says If PA is consistent, then PA !|-- G, where G is a sentence constructed with the Diagonal Lemma that has the intuitive meaning "G is not provable in PA". The formalization of the F.I.T. is PA |-- Con --> ~Pr(#[G]) However, G was constructed so that PA |-- G <--> ~Pr(#[G]); thus, PA |-- Con --> G. G isn't PA-provable, so Con must not be either. We have SECOND INCOMPLETENESS THEOREM If PA is consistent, then PA !|-- Con ------------------------------------------ The same development that led earlier to a representing formula Prf for the primitive recursive notion "m is (the Goedel number of) a PA proof of (the formula with Goedel number) n" works to give us such representing formulas for any theory T with a primitive recursive set of axioms. The representing formula for the proof predicate for such a theory is Prf{T}. Thus, if m is a T-proof of n, then PA |-- Prf{T}(#m, #n) if m is not a T-proof of n, then PA |-- ~Prf{T}(#m, #n) Our original formula Prf(x,y) is now Prf{PA}(x,y). We also have Pr{T}, and Pr{PA}. Sometimes we want to consider the result of adding some new axiom F to a theory T---the new theory is T+F, and there are formulas Prf{T+F}(x,y), and so forth. ------------------------------------------ What did I leave out? Well, there's the proof that every primitive recursive function is representable: if f is primitive recursive, then there is a formula F such that for every n, PA |-- F(#n, y) <--> y = #f(n) This is pretty tedious, but not complicated. Choose some nice hierarchical representation of primitive functions, maybe schemes of recursive definitions, or programs in a suitable language. Then prove representability for the lowest level and work your way up by induction on the complexity of the definition of the function. Representability for primitive recursive predicates is easily deduced from the representability of their characteristic functions. To carry out that plan, you'll have to find a way to quantify over sequences of numbers. To do this, one must have a way to code sequences of numbers by single numbers. Of course, the prime decomposition can help with that---unfortunately, exponentiation, ^, isn't a primitive, and defining it requires just such quantification over sequences. You can avoid the problem by throwing it in as an additional primitive. Or, you can use the Chinese Remainder Theorem, showing it's provable in PA, as Goedel did. I didn't tell you exactly what PA is, either. Nor what the rules of inference are. This whole thing is getting pretty long, and I'm tired. Maybe tomorrow I'll post these things. For now, let's just say that PA is a fairly simple system with obviously true axioms that nevertheless expresses and proves a wide range of results in number theory.