= Recursively inseparable-set proof of Tennenbaum theorem
Let $A,B$ be disjoint <computably enumerable> <recursively inseparable sets>, represented by existential arithmetic formulas with bounded computation witnesses $\alpha(x,y)$ and $\beta(x,z)$. In a <non-standard model of arithmetic> $M\models\mathsf{PA}$, the assertion
$$
\forall x,y,z<c\ \neg(\alpha(x,y)\wedge\beta(x,z))
$$
holds at every standard bound $c$. The <overspill lemma> gives a nonstandard bound where it still holds. This no-clash condition matters: an arbitrarily chosen nonstandard computation stage need not preserve the external disjointness of the two enumerations.
Inside $M$, form the internally finite set $C=\{x<c:\exists y<c\ \alpha(x,y)\}$ and code it by the product of its corresponding <prime numbers>. Its standard trace contains $A$ and avoids $B$, since the finite standard witnesses for either enumeration lie below $c$. If the arithmetic operations of $M$ were computable, division by each standard prime would decide membership in this trace: search for $q$ and a standard remainder $r<p$ satisfying $a=pq+r$, where $a$ is the fixed code. The division algorithm in <Peano arithmetic> guarantees termination. This would give a <computable set> separating $A$ from $B$, a contradiction.<Tennenbaum’s Theorem for Models of Arithmetic by Richard Kaye (2006)>[Internally coded separating set preceding Theorem2.8]{ref}
Back to article page
