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.