EFA can prove the exponential function to be total, but it cannot prove the superexponential function to be total. Is there an analog of Tennenbaum's theorem (which states the PA has no recursive non-standard models) for EFA which states that EFA has no "sub-superexponential" non-standard models? (Here "sub-superexponential" should mean something like "only finitely iterated exponential" space complexity.) Can one say even more, like that EFA has no primitive recursive non-standard models?



Analog of Tennenbaum's theorem for EFA
Tennenbaum’s theorem applies unrestricted to EFA, and even to the much weaker theory $IE\_1$ (Robinson’s arithmetic + induction for bounded existential formulas):


* $IE\_1$ has no recursive nonstandard models (Wilmers [1]).


On the other hand, $\mathit{IOpen}$ (induction for quantifier-free formulas) does have recursive nonstandard models (Shepherdson [2]), and the same also holds for extensions of $\mathit{IOpen}$ by certain “algebraic” axioms: Berarducci and Otero [3] prove this for $\mathit{IOpen}$ + “normality” (= integral closure), and Mohsenipour [4] sketches a proof for $\mathit{IOpen}+\mathit{GCD}$.


In fact, there seems to be a kind of dividing line between $\mathit{IOpen}$ and its mild extensions on the one side, and $IE\_1$ or theories of similar strength on the other side, with several results strengthening Tennenbaum’s theorem to the effect that nonstandard models of theories behind the line are very complicated:


* Every nonstandard model of $IE\_1$ has a nonstandard cut that is a model of Peano arithmetic (Paris [5]). More generally, let $T$ be any $\Sigma\_1$-sound recursively axiomatizable extension of $I\Sigma\_1$. Then every nonstandard model of $IE\_1$ has a nonstandard cut that is a model of $T$ ([5] + McAloon [6]).
* The additive reduct $(M,+,{\le})$ of any model of $IE\_1$ is recursively saturated (Wilmers [1]).
* The real closure of [the fraction field of] a nonstandard model is recursively saturated. This is not actually known to hold for $IE\_1$, but it is true for “unbounded” models of $IE\_2$, and models of $\mathit{PV}\_1$ or $\Sigma^b\_1\text-\mathit{LLLLLIND}$ (J and Kołodziejczyk [7]).


**References:**


[1] George Wilmers, *Bounded existential induction*, Journal of Symbolic Logic 50 (1985), no. 1, pp. 72–90.


[2] John C. Shepherdson, *A non-standard model for a free variable fragment of number theory*, Bulletin de l’Académie Polonaise des Sciences, Série des Sciences Mathématiques, Astronomiques et Physiques 12 (1964), no. 2, pp. 79–86.


[3] Alessandro Berarducci and Margarita Otero, *A recursive nonstandard model of normal open induction*, Journal of Symbolic Logic 61 (1996), no. 4, pp. 1228–1241.


[4] Shahram Mohsenipour, *A recursive nonstandard model for open induction with GCD property and confinal primes*, Logic in Tehran (A. Enayat, I. Kalantari, M. Moniri, eds.), Lecture Notes in Logic, no. 26, Association for Symbolic Logic, 2006, pp. 227–238.


[5] Jeff B. Paris, *O struktuře modelů omezené $E\_1$-indukce*, Časopis pro pěstování matematiky 109 (1984), no. 4, pp. 372–379 (in Czech).


[6] Kenneth McAloon, *On the complexity of models of arithmetic*, Journal of Symbolic Logic 47 (1982), no. 2, pp. 403–415.


[7] Emil Jeřábek and Leszek Kołodziejczyk, *Real closures of models of weak arithmetic*, Archive for Mathematical Logic 52 (2013), no. 1–2, pp. 143–157.


