8
$\begingroup$

Suppose $K$ is an exponential real closed field, i.e. there is an isomorphism, say exp, between the additive group of $K$ and the multiplicative group of its positive elements. Assume further that $Z$ is an integer part of $K$ whose positive cone $Z^{\geq 0}$ is closed under exp.

(1) Does it follow (for any of the standard phrasings of $EXP$) that $Z^{\geq 0}\models IOpen+EXP$?

(2) What if we further assume that $I\models I\Delta_{0}$ (so that the possible dependence on the choice of phrasing is eliminated)?

Edit: $IOpen$ refers to the axiom system of arithmetic with induction restricted to quantifier-free formulas. EXP denotes the arithmetical statement that exponentiation is total. (In the language of arithmetic, exponentiation can e.g. be expressed by stating that $x^{y}=z$ iff there is a number coding a sequence $s$ such that $s_{0}=1$, $s_{y}=z$ and, for all integers $i$ strictly less than $y$, we have $s_{i+1}=xs_{i}$.) Shepherdson's result shows that the positive cone of an $IP$ of an $RCF$ will always be a model of $IOpen$, but $IOpen$ does not prove $EXP$ (nor does even $I\Delta_{0}$). The existence of exp for $K$ ensures that, for some $a\in I$, there is a function $f:I\rightarrow I$ such that $f(0)=1$ and $f(k+1)=af(k)$ for all $k\in I$, but that does not make it obvious (at least to me) that $I$ is 'aware' of this fact (e.g. contains the coding sequences etc.).

$\endgroup$
6
  • 2
    $\begingroup$ Just to be certain, by IOpen you mean induction for "open" formulas in the language including exp? And what exactly is the sentence EXP? The statement that exp is an isomorphism? And if the answers are yes and yes, then doesn't Shepherdson's proof for plain old IOpen work here? If I remember right, it just uses the fact that K is o-minimal. $\endgroup$ Oct 29, 2012 at 15:02
  • $\begingroup$ Yes, that is what I meant. I have added a clarification to my addmitedly not very self-contained post. $\endgroup$
    – M Carl
    Oct 29, 2012 at 15:28
  • $\begingroup$ Sorry, I misread your first question. 'exp' is not supposed to be included in the language. $\endgroup$
    – M Carl
    Oct 29, 2012 at 15:30
  • 2
    $\begingroup$ I’m afraid your definition of EXP is not specific enough. There are many possible definitions of exponentiation; in the context of $I\Delta_0$, any two $\Delta_0$ definitions which provably satisfy some basic recurrence axioms will be provably equivalent, hence it is not necessary to specify the axiom exactly, but these definitions will be no longer equivalent in IOpen. (E.g., in your proposed wording, different coding schemes for sequences may lead to different definitions.) $\endgroup$ Oct 29, 2012 at 16:33
  • $\begingroup$ Having said that, since exp is not necessarily definable in $Z$, I would expect the answer to be negative due to phenomena like mathoverflow.net/questions/94928, but I’m not sure (the situation here is more delicate). $\endgroup$ Oct 29, 2012 at 16:37

1 Answer 1

5
$\begingroup$

The answer to both questions is negative. Every countable model $\def\sM{\mathfrak M}\sM$ of $\mathit{VTC}^0$ (a very weak fragment of $I\Delta_0+\Omega_1$) is an exponential integer part of a real-closed exponential field by [1,2], hence if this property has any first-order consequences besides $\mathit{IOpen}$ at all, they are included in $\mathit{VTC}^0$.

The basic idea is to take for $K$ the completion $\mathbf R^\sM$ of the fraction field $\mathbf Q^\sM$ of $\sM$. This is a real-closed field as $\sM\models\mathit{IOpen}$, and with some effort, one can show that the usual exponential function $2^n\colon\mathbf L^\sM\to\sM$ (where its domain $\mathbf L^\sM$ is the set of logarithmic natural numbers of $\sM$) extends to an isomorphism $2^x\colon(\mathbf R_{\mathbf L}^\sM,+,{<})\simeq(\mathbf R_{>0}^\sM,\cdot,{<})$, where $\mathbf R_{\mathbf L}^\sM=\{x\in\mathbf R^\sM:\exists n\in\mathbf L^\sM\,|x|\le n\}$ is the set of logarithmically bounded reals of $\sM$. Moreover, if $\sM$ is nonstandard, then $(\mathbf Q^\sM,\mathbf Z^\sM,\mathbf Q_{\mathbf L}^\sM,+,{<})$ is recursively saturated, where $\mathbf Z^\sM$ is the extension of $\sM$ with negative numbers. If $\sM$ is countable, one can use this to construct an isomorphism $(\mathbf R^\sM,\mathbf Z^\sM,+,{<})\simeq(\mathbf R_{\mathbf L}^\sM,\mathbf Z_{\mathbf L}^\sM,+,{<})$, whose composition with $2^x$ yields the desired exponential on $\mathbf R^\sM$.

References

[1] Emil Jeřábek: Elementary analytic functions in $\mathit{VTC}^0$, arXiv:2206.12164 [cs.CC], 55 pp., 2022.

[2] Emil Jeřábek: Models of $\mathit{VTC^0}$ as exponential integer parts, arXiv:2209.01197 [math.LO], 21 pp., 2022.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.