] > Tennenbaum's Theorem

Tennenbaum's Theorem

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.


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 TPA 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


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 wiwj 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 TPA 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 AC and BC=.

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


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:


This happens in the particular case when η(n,x) is a first-order formula in the language of PA equivalent to y(pny=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:aM 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 xM 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.


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,


So by the overspill lemma there is some nonstandard ζM with


Now let C be the set C=n:My<ζα(n,y). By preservation of Σ1 formulas and the nonstandardness of ζ, we see immediately that CA, and the above property of ζ also shows that CB=. 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.


Let CSSy(M) be nonrecursive. Then by remarks made earlier there is aM such that


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 yM 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 nC, and nC 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:MTr1(σ) 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 MIE1 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 MPA, 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 MIΔ0 (Cegielski et al (MR0673785)) and for nonstandard MIE1 (Wilmers (MR780526)).

Home page: Tennenbaum's theorem

Author: Richard Kaye, School of Mathematics, University of Birmingham