2 Tennenbaum's Theorem
I will give a presentation of Tennenbaum's theorem and
some variations on it here. All models considered here will
be countable models of at least PA-,
the theory of the nonnegative part of discretely ordered rings.
Except where explicitly stated otherwise, we will regard the
standard model ℕ as an initial segment of each
nonstandard model of arithmetic M. We shall assume some
basic theory from models of arithmetic, such as coding techniques,
etc., and to allow us to switch views from recursion theory on
ℕ and recursive sets of formulas we identify a
formula with its Gödel-number via some natural Gödel-numbering.
All notation not explained here is as in
Models of Peano Arithmetic (MR1098499).
A structure M=(M,+,⋅,0,1,<) is recursive if there
is a 1–1 correspondence f:ℕ→M such that,
identifying ℕ with the domain of M via f,
the functions +,⋅ and relation < on ℕ are recursive on
ℕ. Note that these functions and relation do not need to
correspond to the usual ones on ℕ. The structure M
is non-recursive if there is no such 1–1 correspondence.
The standard model (ℕ,+,⋅,0,1,<) with the
usual addition, multiplication and order is recursive, via the identity
map ℕ→ℕ. Tennenbaum showed that this is the only such
recursive model of arithmetic.
Theorem 2.1 (Tennenbaum, 1959)
Let M=(M,+,⋅,0,1,<) be a countable model of PA, and
not isomorphic to the standard model (ℕ,+,⋅,0,1,<).
Then M is not recursive.
It turns out that the choice of theory here is rather inessential.
Indeed Tennenbaum doesn't bother state which theory
is taken here, simply writing in his abstract provable
,
which presumably meant provable in PA
.
The theory PA may be replaced by much weaker sub-theories, including
some finitely axiomatized sub-theories. How far one can go in this
direction is an interesting question that will be discussed later.
Tennenbaum's theorem improved on Mostowski's attempts
at proving similar results. The key technique was a suitable choice of coding
mechanism in arithmetic.
I will present a proof of Tennenbaum's theorem shortly.
Before I do so, I would like to indicate at least one aspect of what it says:
in some precise sense Tennenbaum's theorem is a model-theoretic
version of the Gödel–Rosser incompleteness theorem.
Definition 2.2
For a theory T in the language of arithmetic, denote
by Π1-Th(T) the set of Π1 consequences
of T, i.e., the set of sentences
σ∈Π1:T⊢σ.
Similarly Πn-Th(T), Σn-Th(T),
etc.
Theorem 2.3 (Rosser)
There is no consistent extension T of PA for which
Π1-Th(T) is recursive.
Proof
I shall sketch a proof assuming Tennenbaum's theorem
as stated earlier but for the set of
Π2-consequences of PA, rather than PA itself.
First, assume that T⊇PA is consistent and
Π1-Th(T) is recursive. We make a model in
the usual Henkin-style using model-theoretic forcing with
Δ0 conditions. That is, at stage k of the construction
we have a Δ0 condition, i.e.,
a Δ0 formula λk(w0,…,wnk)
in special witnessing
constants wi which is a conjunction of
several Δ0 formulas that we want to make true (including all
previous conditions in the construction) such that
T+λk(w0,…,wnk) is consistent.
The resulting model M will be formed from the wi, and by usual
techniques we can ensure that M is a Σ1-elementary
submodel of a model N of T together with all the
λk(w0,…,wnk), so in particular
M⊧Π2-Th(T).
The assumption that Π1-Th(T) is recursive
allows us to ensure that the whole construction can be carried out recursively.
This is because during the construction, we need only decide questions such as,
given λk(w0,…wnk) and a
new Δ0 formula θ(w¯,x¯), is
T+λk(w0,…,wnk)+θ(w¯,x¯)
consistent? This amounts to asking if
T⊢∀w0,…,wnk,x¯(λk(w0,…,wnk)→¬θ(w¯,x¯)),a question that can be effectively decided by looking at
Π1-Th(T). Thus the construction is recursive, and
indeed the sequence of conditions produced by the construction is also
a recursive sequence of Δ0 formulas in the witnessing constants.
This means that the resulting model M is recursive, since it is
built from an enumerated set of witnesses wi modulo the recursive
equivalence relation wi∼wj when wi=wj
is a conjunct of some condition in the construction. The truth of any Σ1
sentence ∃xθ(x) can also be determined: on the one hand by
seeing if θ(wi) is a conjunct of a condition for some wi;
and on the other hand by seeing if some other condition
λk(w0,…,wnk) together with
T implies ∀x¬θ(x). Thus the model M
is nonstandard because the truth of Σ1 sentences
in the standard model ℕ is well-known not to be decidable.
We conclude that if T⊇PA is consistent and
Π1-Th(T) is recursive there is a recursive nonstandard model
of Π2-Th(T), and as T extends PA this
contradicts Tennenbaum's theorem for Π2-Th(PA) .
The Gödel–Rosser Theorem is well-known to be related to the following
classical result of recursion theory, which we will use to prove
Theorem 2.1.
Theorem 2.4
There exist r.e. sets A,B⊆ℕ
which are recursively inseparable, i.e., there is no recursive
set C⊆ℕ such that A⊆C and
B∩C=∅.
To prove Theorem 2.1, we will follow Tennenbaum and separate
the problem into two subproblems: firstly of saying something about which
sets A⊆ℕ are coded in a model M, and
secondly on the consequences of having nonrecursive sets coded.
Definition 2.5
Let M be a nonstandard model of arithmetic. We define
SSy(M), the standard system of sets coded in M
to be the set of all A⊆ℕ such that
A=n∈ℕ:M⊧η(n,a¯)for some formula η and some a¯∈M.
In most cases, we may fix a particular formula η
appropriately and all sets in the standard system appear for
this η and a suitable choice of parameters a¯.
By the induction axioms, this will work in PA for any
η for which the following statement is provable
for all pairs of finite disjoint sets A,B⊆ℕ:
∃x¯(⋀i∈Aη(i,x¯)∧⋀j∈B¬η(j,x¯))This happens in the particular case when
η(n,x) is a first-order formula in the language of
PA equivalent to ∃y(pn⋅y=x), where
p0=2, p1=3, p2=5, and
so on, enumerating the standard primes. Thus, for nonstandard
models M of PA, we have
SSy(M)=A⊆ℕ:∃a∈M A=n∈ℕ:M⊧η(n,a)This formulation of SSy(M) is particularly
useful when studying the complexity of addition in a model.
The following lemma is a straightforward application of induction.
Lemma 2.6 (Robinson's overspill lemma)
Let M be a nonstandard model of Peano arithmetic, and suppose
a¯∈M and θ(x,y¯) is a formula such that
M⊧θ(n,a¯) for each n∈ℕ. Then
there is a nonstandard x∈M such that M⊧θ(n,a¯).
The traditional approach to Tennenbaum's theorem now splits into two parts.
Theorem 2.7
Let M be a nonstandard model of Peano arithmetic. Then
SSy(M) contains a nonrecursive set.
Proof
Let A,B⊆ℕ be r.e., recursively inseparable sets,
given by Theorem 2.3. Then these sets are defined
(in ℕ) by Σ1 formulas
∃y α(x,y) and ∃z β(x,z), respectively,
where α and β are Δ0. We regard
the standard model ℕ as an initial segment of M
and note that Σ1 formulas are preserved upwards from
initial segments to the larger model. So, by this and the
disjointness of A,B we have, for each k∈ℕ,
M⊧∀x,y,z<k ¬(α(x,y)∧β(x,z)).So by the overspill lemma there is some nonstandard ζ∈M
with
M⊧∀x,y,z<ζ ¬(α(x,y)∧β(x,z)).Now let C⊆ℕ be the set
C=n∈ℕ:M⊧∃y<ζ α(n,y).
By preservation of Σ1 formulas and the nonstandardness
of ζ, we see immediately that C⊇A, and the
above property of ζ also shows that C∩B=∅.
So by our choice of A and B, C is nonrecursive, as
required.
Theorem 2.8
Let M be a model of Peano arithmetic for which
SSy(M) contains a nonrecursive set. Then
(M,+) is not recursive.
Proof
Let C∈SSy(M) be nonrecursive. Then by remarks made earlier
there is a∈M such that
C=n∈ℕ:M⊧η(n,a)for the formula η(n,x) which is
∃y(pny=x).
Then if + in M were recursive so would C
be, since on input n∈ℕ we may compute
pn (which is the nth prime in M
just as it is in ℕ by preservation between M and
ℕ) and search for y∈M and r<pn
such that (y+y+⋯+y)+r=a (pn ys).
This search is guaranteed to terminate and both y and r
are uniquely determined by n and a, by Euclidean
division in PA. If r=0 we conclude n∈C,
and n∉C otherwise.
It is natural to ask how far this argument can be pushed, replacing
the theory PA by weaker theories. In the form that I have just given it,
overspill is only required for Δ0 relations, and
the subtheory IΔ0 consisting of some base axioms
and induction on Δ0 formulas is strong enough to
prove enough facts about Euclidean division, primes (including
a formula for the nth prime for all standard and
sufficiently small nonstandard n, though it is still not known if this
theory proves the infinitude of primes) for the above argument to
go through. This was observed by Cegielski et al (MR0673785)
and is essentially the proof given in my
Models of Peano Arithmetic (MR1098499).
Note too that the subtheory mentioned earlier,
Π2-Th(PA)
of the Π2 consequences of PA, contains
IΔ0. Indeed all axioms of IΔ0
are Π1 and also axioms of PA; in fact
IΔ0 is very much weaker than
Π2-Th(PA).
A much sharper result using essentially the same ideas was achieved by
Wilmers (MR780526) who showed the same result for the subtheory
IE1 of IΔ0 where induction axioms are only
allowed for bounded existential formulas, i.e., formulas of the
form ∃y¯<p(x¯)q(x¯,y¯)=r(x¯,y¯)
where p,q,r are polynomials with nonnegative integer coeficients.
Wilmers achieved some improvements on the above argument, firstly by
taking A,B to be disjoint r.e., recursively inseparable sets of primes,
but more particularly by using the MRDP theorem on the diophantine
representation of r.e. sets (MR0258744). Interestingly, Wilmers did not ever
need to use the provability of the MRDP theorem, just its truth for
the standard model ℕ, to get the required sets represented and
to achieve the necessary overspill arguments in IE1.
Two other methods for showing SSy(M) contains non-recursive
sets come to mind. The first is to use a formalization of a (necessarily partial)
truth definition in the model M. For example, there is a Π1
formula Tr1(x) expressing x is the Gödel-number
of a true Π1 sentence
. This formula behaves as expected, and
in particular is correct
on standard formulas, in all models of PA. Then
in such a model M the set
C=σ∈Π1:M⊧Tr1(σ)
of true standard Π1 sentences is coded, consistent, and
(by the Gödel–Rosser theorem) therefore non-recursive. This method is straightforward
and uses well-known results, but because as it relies on a formalization
inside the theory of arithmetic, it is not applicable to weaker systems.
No such truth definition is known for IΔ0, for instance.
The second method goes back to Scott (MR0141595), and uses overspill again.
By an overspill argument, SSy(M) has the property that it is a boolean
subalgebra of P(ℕ) closed under relative recursion and König's lemma.
(In modern terminology, it is a Scott set.) It follows that every
first-order theory (such as PA itself) coded in M
(i.e., in SSy(M)) has a coded complete
extension, and of course such sets will not themselves be recursive.
(Details are given in Models of Peano Arithmetic (MR1098499).)
This argument works very well in contexts where overspill is available,
and Wilmers (MR780526) shows that SSy(M) is a Scott set whenever
M⊧IE1 is nonstandard. For weaker theories we still seem to need
alternative arguments.
In closing this section, I should mention two other strengthenings of Tennenbaum's
theorem that have been considered. The first is to start with a nonstandard
model M of some weak theory of arithmetic T and find a nonstandard initial
segment I of M satisfying PA. Then Tennenbaum's theorem for
the initial segment readily implies Tennenbaum's theorem for the original model
M by the absoluteness of Euclidean division. For T=IΔ0
a result of this kind was discovered by Cegielski et al (MR0673785)
and for T=IE1 nonstandard initial segments satisfying PA were
discovered by Paris (MR774279). The other strengthening is to consider
the reduct of the model M to addition alone. For M⊧PA, this
reduct is a model of Presburger arithmetic and is recursively saturated. Such models
are necessarily nonrecursive by similar reasons: Euclidean division gives a notion
of standard system, which (by recursive saturation) is a Scott set and therefore
contains nonrecursive sets. The same result also holds for nonstandard
M⊧IΔ0 (Cegielski et al (MR0673785))
and for nonstandard M⊧IE1 (Wilmers (MR780526)).