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?
$\begingroup$
$\endgroup$
4
-
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řábekMar 13, 2018 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 KlimpelMar 13, 2018 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 KlimpelMar 13, 2018 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řábekMar 13, 2018 at 12:29
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
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.
answered Mar 13, 2018 at 15:51