Analogues of Shepherdson's Theorem for a language with exponentiation
Konstantin Kovalyov
TL;DR
The paper extends Shepherdson's theorem to languages with exponentiation and power by establishing criteria that connect discretely ordered rings and their open induction in expanded languages to exponential real closed fields containing the ring as an exponential IP. It proves a forward direction under natural sufficient conditions (Exponential IPs in ExpField+MaxVal with $\exp(1)=2$ and $\forall x(\exp(x)\ge 1+x)$) and introduces a finite axiom set $T_{x^y}$ to capture the $x^y$-IP relation, enabling a reverse-direction criterion via an exponential real closed field. A constructive embedding of $\mathcal{M}$ into a real-closed exponential field $(\mathcal{K}_{\mathcal{M}}, \exp_{\mathcal{M}})$ via $\mathcal{M}$-Cauchy sequences demonstrates $\mathcal{M}^+$ models of $IOpen(\exp)$ (and $IOpen(x^y)$ under suitable theories). The authors build nonstandard models using $\mathbb{R}((t))^{LE}$ to obtain independence results (e.g., irrationality of $\sqrt{2}$ not provable in $IOpen(\exp)$) and discuss open questions on decidability, conservativity, and possible weakenings of the core axioms, linking the work to Khovanskii's theory and o-minimal frameworks.
Abstract
In 1964 Shepherdson \cite{shepherdson:1964} proved that a discretely ordered semiring $\mathcal{M}^+$ satisfies $\sf{IOpen}$ (quantifier free induction) iff the corresponding ring $\mathcal{M}$ is an integer part of the real closure of the quotient field of $\mathcal{M}$. In this paper, we consider open induction schema in the language of arithmetic expanded by exponentiation or by the power function and try to find similar criteria for models of these theories. For several expansions $T$ of the theory of real closed fields we obtain analogues of Shepherdson's Theorem in the following sense: If an exponential field $\mathcal R$ is a model of $T$ and a discretely ordered ring $\mathcal M$ is an (exponential) integer part of $\mathcal R$, then $\mathcal M^+$ is a model of the open induction in the expanded language. The proof of the opposite implication, in general, remains an open question. However, we isolate a natural sufficient condition, related to the well-known Bernoulli inequality, under which this result holds. We define a finite extension $T$ of the usual open induction so that, for any discretely ordered ring $\mathcal M$, the semiring $\mathcal M^+$ satisfies $T$ iff there is an exponential real closed field $\mathcal R$ with the inequality $\exp(x) \geqslant 1 + x$ such that $\mathcal M$ is an exponential integer part of $\mathcal R$. Using these results, we obtain some concrete independence results for these theories.