Are there signatures escaping from Tennenbaum's Theorem? By Tennenbaum's Theorem all recursive models of $\mathsf{PA}$ are isomorphic to the standard model. And by a result of Wilmer this holds even for models of the theory $\mathsf{IE}_1\subseteq \mathsf{I}\Delta_0$.
However, all the proofs of the result that I know are sensitive to the signature of the theory. So it is natural to ask what will happen for theories definitionally equivalent to $\mathsf{PA}$. Recall that theories $T$ and $U$ are definitionally equivalent if there is a theory $V$ that is a definitional extension of both $T$ and $U$. (For this definition we assume that the signatures of $T$ and $U$ are disjoint: otherwise we first rename symbols from signatures of $T$ and $U$ to make them disjoint.)
In particular it isn't clear to me if Tennenbaum’s theorem holds for the models of the following theory definitionally equivalent to $\mathsf{PA}$: $$(\mathsf{ZFC}-\mathsf{Infinity})+\mathsf{TransitiveClosure}+\lnot\mathsf{Infinity}.$$
So my questions are:

*

*Is there a theory $T$ definitionally equivalent to $\mathsf{PA}$ such that $T$ has a non-standard recursive model?

*Are there any natural examples of such theories?

*Could such a theory have computable signature in the sense that $\mathsf{PA}$-definitions of the symbols of $T$ are $\Delta_1$-predicates and $\Sigma_1$-functions?


Edit: As pointed by Ali Enayat in the comments, Tennenbaum's Theorem holds for the theory $(\mathsf{ZFC}-\mathsf{Infinity})+\mathsf{TransitiveClosure}+\lnot\mathsf{Infinity}$, i.e. all its recursive models are isomorphic to the standard model $\mathsf{HF}$ (see [1, Theorem 3.11]).
[1] A. Enayat, J. Schmerl, and A. Visser. "$\omega$-models of finite set theory". In J. Kennedy and R. Kossak, editors, Set Theory, Arithmetic and Foundations of Mathematics:Theorems, Philosophies, number 36 in ASL Lecture Notes in Logic, pages 43–65. ASL and Cambridge University Press, New York, 2010, ISBN 978-1-107-00804-5, MR2882651, Zbl 1261.03121.
 A: I solved the questions 1. and 3. myself. There is a theory $T$ definitionally equivalent to $\mathsf{PA}$ such that all its consistent c.e. extensions have computable models, which in particular implies that there are non-standard computable models of $T$ [1].
The idea is instead of working with $\mathsf{PA}$ to work with definitionally equivalent $\mathsf{ZF}_{\mathsf{fin}}^+=(\mathsf{ZF}-\mathsf{Infinity})+\mathsf{TransitiveClosure}+\lnot\mathsf{Infinity}$. There I define a ternary predicate $S(x,y,z)$ such that

*

*$x\in y\iff \forall z \;S(x,y,z)$;

*if we have finite set $A$ and finite structure $B$ in the language with $\in$ and $S$, s.t. $B$ extends $(A,\in,S)$ by exactly one element $v$, $B\models \forall x,y (x\in y \mathrel{\leftrightarrow} \forall z(S(x,y,z))$, and $B\models \forall x(x\not\in v\land v\not\in x)$, then there is an embedding of $B$ into $(V,\in,S)$ that keeps $A$ in place  (the embedding preserves both predicates and their negations).

Essentially I show that for any $S$ satisfying this two properties and any consistent c.e. extension $T'$ of $\mathsf{ZF}_{\mathsf{fin}}^+$ there is a model of $T'$, where $S$ is computable. Which, since $\in$ could be first-order defined from $S$ by 1., resolves the question.
The technically complicated part of the paper is the construction of models with computable $S$. It is achieved by a priority argument. Basically the idea is to start with a complete $\Delta_2$ theory with Henkin constants $T\supseteq \mathsf{ZF}_{\mathsf{fin}}^+$. And then build a computable isomorphic copy $M$ of the $S$ part of the corresponding Henkin model of $T$. The point here is that the correspondence between elements of $M$ and Henkin constants is not computable and is recovered only as the limit of guesses. The property 2. allows to have Henkin constants with any possible designated $S$-connection with given finite set of Henkin constants. This allows to assign some Henkin constants to elements of $M$ that have been created to correspond to some other Henkin constants, but at some point in the process of building $M$ this correspondence have been scraped.
Unfortunately, this $S$, although being $\Delta^0_1$, clearly couldn't be called natural. So I leave the question open in the case if someone actually finds a natural example of this nature or gives some kind of convincing argument, why it isn't possible to construct natural examples of this kind.
[1] Fedor Pakhomov. How to escape Tennenbaum's theorem. arXiv:2209.00967, https://arxiv.org/abs/2209.00967
