7Incompleteness*
II Logic and Set Theory
7 Incompleteness*
The big goal of this (non-examinable) chapter is to show that PA is incomplete,
i.e. there is a sentence p such that PA ⊢ p and PA ⊢ ¬p.
The strategy is to find a p that is true in N, but PA ⊢ p.
Here we say “true” to mean “true in
N
”, and “provable” to mean “PA proves
it”.
The idea is to find a
p
that says “I am not provable”. More precisely, we
want a
p
such that
p
is true if and only if
p
is not provable. We are then done:
p
must be true, since if
p
were false, then it is provable, i.e.
PA ⊢ p
. So
p
holds
in every model of PA, and in particular,
p
holds in
N
. Contradiction. So
p
is
true. So p is not provable.
We’ll have to “code” formulae, proofs etc. inside PA, i.e. as numbers. But
this doesn’t seem possible — it seems like, in any format, “
p
is not provable”
must be longer than p. So p cannot say “p is not provable“!
So be prepared for some magic to come up in the middle for the proof!
Definability
We first start with some notions of definability.
Definition (Definability). A subset
S ⊆ N
is definable if there is a formula
p
with one free variable such that
∀m ∈ N : m ∈ S ⇔ p(m) holds.
Similarly, f : N → N is definable if there exists a formula p(x, y) such that
∀m, n ∈ N : f(m) = n ⇔ p(m, n) holds.
Example. The set of primes is definable: p(x) is
x = 1 ∧(∀y)(∀z)(yz = x ⇒ (y = 1 ∨z = 1)).
We can say “m is prime” is definable.
How about powers of 2? We don’t have exponentiation here. What can we
do? We can take p(x) to be
(∀y)((y is prime ∧ y | x) ⇒ y = 2),
where 2 is a shorthand for
s
(
s
(0)), and
y | x
is a shorthand for (
∃z
)(
yz
=
x
). So
this is also definable.
The function m 7→ m
2
is also definable: take p(x, y) to be yy = x.
Here we will assume:
Fact. Any function given by an algorithm is definable.
Proof will not be given here. See, eg, PTJ’s book for detailed proof.
Example. m 7→ 2
m
is definable.
Coding
Our language has 12 symbols:
s,
0
, ×,
+
, ⊥, ⇒,
(
,
)
,
=
, x,
′
, ∀
(where the variables
are now called x, x
′
, x
′′
, x
′′′
.
We assign values to them, say
v
(
s
) = 1
, v
(0) = 2
, ··· , v
(
∀
) = 12. To code a
formula, we can take
2
v(first symbol)
· 3
v(second symbol)
···(nth prime)
v(nth symbol)
.
For example, (∀x)(x = x) is coded as
2
7
3
12
5
10
7
8
11
7
13
10
17
9
23
8
.
Not every
m
codes a formula, e.g. 2
7
3
12
5
10
is translated to (
∀x
, which is clearly
nonsense. Similarly, 2
7
7
3
or 2
100
can’t even be translated at all.
However, “
m
codes a formula” is definable, as there is an algorithm that
checks that.
Write
S
m
for the formula coded by
m
(and set
S
m
to be “
⊥
” if
m
does not
code a formula). Similarly, write c(p) for the code of p.
Given a finite sequence p
1
, ···p
n
for formulae, code it as
2
c(p
1
)
3
c(p
2
)
···(nth prime)
c(p
n
)
.
Alternatively, we can add a separator character to our 12 symbols and concatenate
the sequence of formulae with the separator character.
Now, “
m
codes an axiom (either logical or axiom of PA)” is definable, as
there exists an algorithm to check it. For example, an instance of the first logical
axiom can be validated by the following regex:
^\([s0()=x’\+×⊥ ⇒ ∀]+\)⇒([s0()=x’\+×⊥ ⇒ ∀]+ ⇒ \1)$
(after translating to a sentence and verifying it is a valid logical formula)
Also,
ϕ(ℓ, m, n) =“S
n
obtained from S
ℓ
, S
m
via MP”
is definable, and similarly for generalization.
So
Θ(m, n) = “n codes a proof of S
m
”
is definable.
Thus
Ψ(m) = “S
m
is provable”
is definable as
Ψ(m) ⇔ (∃n)Θ(m, n).
So far, everything is rather boring. We all know that strings of symbols can be
coded into numbers — that’s what computers do!
Clever bit
Consider the statement χ(m) that states
“m codes a formula S
m
with one free variable, and S
m
(m) is not provable.”
This is clearly definable. Suppose this is defined by p. So
χ(n) ⇔ p[n/x]
Suppose c(p) = N . Then χ(N) asserts
“N codes a formula S
N
with one free variable and S
N
(N) is not provable.”
But we already know that
N
codes the formula
χ
. So
χ
(
N
) asserts that
χ
(
N
) is
not provable.
So
Theorem (G¨odel’s incompleteness theorem). PA is incomplete.
Maybe that’s because PA is rubbish. Could we add some clever axiom
t
(true
in
N
) to PA, so that PA
∪{t}
is complete? No! Just run the same proof with
“PA” replaced by “PA∪{t}” to show that PA∪{t} is incomplete.
But we can certainly extend PA to a complete theory — let
T
=
{p
:
p holds in N}. What will go wrong in our proof? It can only be because
Theorem. “Truth is not definable”
T = {p : p holds in N} is not definable. This officially means
{m : m codes a member of T }
is not a definable set.
Next question: we proved that our clever statement
p
is true but not provable.
Why doesn’t this formalize into PA? The answer is, in the proof, we also used
the fact that PA has a model,
N
. By completeness, this means that we used the
statement con(PA), i.e. the statement that PA is consistent, or
(∀m)(m does not code a proof of ⊥).
With this statement, the proof does formalize to PA. So PA
∪{con(PA)} ⊢ p
.
Hence
Theorem. PA ⊢ con(PA).
The same proof works in ZF. So ZF is incomplete and ZF does not prove its
own consistency.