The standard proof of Tennenbaums's theorem uses the existence of recursively enumerable inseparable sets and is presented e.g. in Kaye [1, 2], Smith [3].

In the following, $\mathcal{M}$ will always designate a model of $\mathsf{PA}$. It will be called enumerable if there is a surjection $e : \mathbb{N} \to \mathcal{M}$ (also called the enumerator) and computable if its domain is $\mathbb{N}$ and addition as well as multiplication in the model are computable (e.g. by a Turing machine). I will also use the following two abreviations: $$ \mathbb{N} \mid d := \{ \, n \in \mathbb{N} : \mathcal{M} ⊨ \overline n \mid d \, \} ~~\text{for } d \in \mathcal{M} \\ \mathbb{N} \mid \mathcal{M} := \{ \, (n, d) \in \mathbb{N} \times \mathcal{M} : \mathcal{M} ⊨ \overline n \mid d \, \} $$

There are two important facts used in the usual proof of the theorem:

Fact 1 : If $\mathcal{M}$ is computable, then $\mathbb{N} \mid \mathcal{M}$ is recursive.

Proof Idea: Given there is a enumerator $e$ for $\mathcal{M}$; we can search through all tuples $(n,r) \in \mathbb{N}^2$ and check whether the equation $d = e_n \cdot \overline n + \overline r$ is satisfied (here we make use of computability and discreteness). By the Euclidean lemma we are guaranteed that the search must succeed at some point, since there are $q \in \mathcal{M}, r \in \mathbb{N}$ with $d = q \cdot \overline n + \overline r$. Once $(n, r)$ is found, we then simply check whether $r = 0$.

Fact 2 : If $\mathcal{M}$ is non-standard, then for every formula $\alpha(x)$ there is a code $C \in \mathcal{M}$ with $\forall n \in \mathbb{N} : ~\mathcal{M} \vDash \alpha(\overline n) \leftrightarrow \overline{\pi_n} \mid C$.

Proof Idea: There is a non-standard element $\mathbb{N} < e \in \mathcal{M}$. Morally the code we construct is then the infinite product $C := \prod_{n < e, \, \mathcal{M} \vDash \alpha(\overline n)} \overline{\pi_n}$.

For an alternative proof, I will use a result from the theory of computation:

Representability Theorem : If $A \subset \mathbb{N}$ is recursive, then there is a unary formula $\varphi(x)$ s.t. $n \in A \Rightarrow \mathsf{Q} \vdash \varphi(\overline n)$ and $n \not \in A \Rightarrow \mathsf{Q} \vdash \neg \varphi(\overline n)$.

Here is then the intuition behind the main part of the argument: Assuming we have an enumeration $e_1, e_2, \dots$ of all elements in $\mathcal{M} \vDash \mathsf{PA}$, we can check whether the $n$-th prime number $\overline{\pi_n}$ divides $e_n$. By combining the above two facts we can find an element $C \in \mathcal{M}$ which is divisible by $\overline{\pi_n}$ if and only if $\neg \, \overline{\pi_n} \mid e_n$. But $C$ also appears as some $e_c$ in the enumeration, leading us to the now problematic question: Is it divisible by $\pi_c$ or not?

Lemma : Given $\mathcal{M}$ is enumerable, we have that $\mathbb{N} \mid \mathcal{M}$ is recursive if and only if $\mathcal{M}$ is isomorphic to $\mathbb{N}$.

Proof: Assume $\mathcal{M}$ were non-standard.

  • By enumerability, there is a surjective function $e : \mathbb{N} \to \mathcal{M}$.
  • From the second assumption we conclude that the set $\mathsf{Diag} := \{ \, n \in \mathbb{N} : \neg \, \mathcal{M} ⊨ \overline{\pi_n} \mid e_n \, \}$ is recursive, and by the representability theorem we have a corresponding formula $\varphi(x)$ for it.
  • Using Fact 2 we get a code $C \in \mathcal{M}$ coding $\varphi$, and by surjectivity a $c \in \mathbb{N}$ with $e_c = C$.
  • We now have : $$ c \in \mathsf{Diag} \stackrel{\text{repr.}}{\Rightarrow} \mathsf{Q} \vdash \varphi(\overline c) \stackrel{\text{sound}}{\Rightarrow} \mathcal{M} ⊨ \varphi(\overline c) \stackrel{\text{coding}}{\Rightarrow} \mathcal{M} ⊨ \overline{\pi_c} \mid e_c \stackrel{\text{def.}}{\Rightarrow} c \not \in \mathsf{Diag} \\ c \not \in \mathsf{Diag} \Rightarrow \mathsf{Q} \vdash \neg \varphi(\overline c) \Rightarrow \neg \mathcal{M} ⊨ \varphi(\overline c) \Rightarrow \neg \mathcal{M} ⊨ \overline{\pi_c} \mid e_c \Rightarrow c \in \mathsf{Diag} $$ Giving us the contradictory statement $c \in \mathsf{Diag} \Leftrightarrow c \not \in \mathsf{Diag}$. $~\Box$

The usual theorem now follows by usage of Fact 1 :

Tennenbaum's Theorem : Every computable model of $\mathsf{PA}$ is standard.

I should also note that I verified the above proof in a proof assistant, so I am quite certain about the correctness.


The proof to me seems more straight forward then the proofs using inseparable sets, and I am currently trying to find out whether it is to be found somewhere in the existing literature. Apart from the standard literature I listed above, I also checked some constructive treatments (Plisko [4], McCarty [5] [6]).

Are there any references that come to your mind that I have been overlooking?

It also seems to me that the proof via inseparable sets does have its own merits when it comes to the final result. Some refinement of the original proof leads to the conclusion:

Theorem : $\mathcal{M}$ is standard if and only if $\mathbb{N} \mid d$ is recursive for every $d \in \mathcal{M}$.

Is there some good intuition for why the usage of inseparable sets eliminates the need for enumerability?

[1] Dimitracopoulos, C. "Richard Kaye, Models of Peano Arithmetic." Journal of Symbolic Logic 58.1 (1993)

[2] Kaye, Richard. "Tennenbaum’s theorem for models of arithmetic." Set Theory, Arithmetic, and Foundations of Mathematics. Ed. by J. Kennedy and R. Kossak. Lecture Notes in Logic. Cambridge (2011): 66-79.

[3] Smith, Peter. "Tennenbaum’s Theorem." (2014).

[4] Plisko, Valerii Egorovich. "Constructive formalization of the Tennenbaum theorem and its applications." Mathematical notes of the Academy of Sciences of the USSR 48.3 (1990): 950-957.

[5] McCarty, Charles. "Variations on a thesis: intuitionism and computability." Notre Dame journal of formal logic 28.4 (1987): 536-580.

[6] McCarty, Charles. "Constructive validity is nonarithmetic." The Journal of Symbolic Logic 53.4 (1988): 1036-1041.

  • $\begingroup$ See also the arguments at mathoverflow.net/q/12426/1946. $\endgroup$ Jan 17, 2022 at 14:30
  • $\begingroup$ This is an interesting argument, but I’m having a hard time trying to understand the question. What exactly do you mean by “enumerable”, and how do you define “computable” for things that are not “enumerable”? And what do you mean by “discrete”, for that matter? $\endgroup$ Jan 17, 2022 at 15:31
  • $\begingroup$ Also, it seems that you intend $\mathcal M$ to be a model of PA in the whole discussion, even though this is only mentioned in passing halfway through. This should be clearly stated at the outset. $\endgroup$ Jan 17, 2022 at 16:04
  • $\begingroup$ @EmilJeřábek Those are some good remarks, thank you! I have made an edit which hopefully addressed them. $\endgroup$
    – Léreau
    Jan 18, 2022 at 14:21
  • 1
    $\begingroup$ A reference which might be useful for your purposes is the following one: Schmerl, James H., Tennenbaum's theorem and recursive reducts. Set theory, arithmetic, and foundations of mathematics: theorems, philosophies, 112–149, Lect. Notes Log., 36, Assoc. Symbol. Logic, La Jolla, CA, 2011. $\endgroup$
    – Ali Enayat
    Feb 14, 2022 at 21:08

1 Answer 1


It turns out that the same proof idea can be found in the fifth edition of Computability and Logic by Boolos, Burgess and Jeffrey:



Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.