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 nonstandard models) for EFA which states that EFA has no "subsuperexponential" nonstandard models? (Here "subsuperexponential" should mean something like "only finitely iterated exponential" space complexity.) Can one say even more, like that EFA has no primitive recursive nonstandard models?

5$\begingroup$ Tennenbaum's theorem holds literally for EFA, or even for the much weaker theory $IE_1$: that is, the theory has no recursive nonstandard models. Totality of functions has nothing to do with it. After all, most recursive functions are not provably total in PA either. $\endgroup$ – Emil Jeřábek 3.0 Mar 13 '18 at 10:31

$\begingroup$ @EmilJeřábek I guessed this, especially after reading this comment by Noah Schweber. But despite this, I didn't manage to find an explicit reference spelling out this fact. So I would like to have something more than a comment, which still doesn't allow me to verify this fact. $\endgroup$ – Thomas Klimpel Mar 13 '18 at 11:12

$\begingroup$ I guess $IE_1$ is Q (Robinson arithmetic) plus induction for formulas with just one block of bounded quantifiers, i.e. a really weak theory just slightly stronger than Q. $\endgroup$ – Thomas Klimpel Mar 13 '18 at 11:47

1$\begingroup$ I will write an answer with more context later, but the basic reference for Tennenbaum’s theorem for $IE_1$ is G. Wilmers, Bounded existential induction, JSL 50 (1985), 72–90. jstor.org/stable/2273790 $\endgroup$ – Emil Jeřábek 3.0 Mar 13 '18 at 12:29
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 quantifierfree 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 nonstandard 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.