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.
Questions
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.
