Arithmetization of the field of reals with exponentiation extended abstract

Boughattas, Sedki; Ressayre, Jean-Pierre

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 42 (2008) no. 1, pp. 105-119

(1) Shepherdson proved that a discrete unitary commutative semi-ring $A^{+}$ satisfies $I{E}_0$ (induction scheme restricted to quantifier free formulas) iff $A$ is integral part of a real closed field; and Berarducci asked about extensions of this criterion when exponentiation is added to the language of rings. Let $T$ range over axiom systems for ordered fields with exponentiation; for three values of $T$ we provide a theory ${}_{⌞}{T}_{⌟}$ in the language of rings plus exponentiation such that the models ($A$, exp${}_A$) of ${}_{⌞}{T}_{⌟}$ are all integral parts $A$ of models $M$ of $T$ with $A^{+}$ closed under exp${}_M$ and ${exp}_A={exp}_M\upharpoonright A^{+}$. Namely $T$ = EXP, the basic theory of real exponential fields; $T$ = EXP+ the Rolle and the intermediate value properties for all $2^x$-polynomials; and $T$ = $T_{exp}$, the complete theory of the field of reals with exponentiation. (2) ${}_{⌞}$$T_{exp}$${}_{⌟}$ is recursively axiomatizable iff $T_{exp}$ is decidable. ${}_{⌞}$$T_{exp}$${}_{⌟}$ implies $L{E}_0\left(x^y\right)$ (least element principle for open formulas in the language $<,+,\times ,-1,x^y$) but the reciprocal is an open question. ${}_{⌞}$$T_{exp}$${}_{⌟}$ satisfies “provable polytime witnessing”: if ${}_{⌞}$$T_{exp}$${}_{⌟}$ proves ${\forall x\exists y:\left|y\right|<\left|x\right|}^k)R(x,y)$ (where $\left|y\right|:{=}_{⌞}$$log\left(y\right)$${}_{⌟}$, $k<\omega$ and $R$ is an NP relation), then it proves $\forall xR(x,f(x\left)\right)$ for some polynomial time function $f$. (3) We introduce “blunt” axioms for Arithmetics: axioms which do as if every real number was a fraction (or even a dyadic number). The falsity of such a contention in the standard model of the integers does not mean inconsistency; and bluntness has both a heuristic interest and a simplifying effect on many questions - in particular we prove that the blunt version of ${}_{⌞}$$T_{exp}$${}_{⌟}$ is a conservative extension of ${}_{⌞}$$T_{exp}$${}_{⌟}$ for sentences in $\forall {\Delta }_0\left(x^y\right)$ (universal quantifications of bounded formulas in the language of rings plus $x^y$). Blunt Arithmetics - which can be extended to a much richer language - could become a useful tool in the non standard approach to discrete geometry, to modelization and to approximate computation with reals.

Classification : 03H15
Keywords: computation with reals, exponentiation, model theory, o-minimality

[1] S. Boughattas, Trois Théorèmes sur l'induction pour les formules ouvertes munies de l'exponentielle. J. Symbolic Logic 65 (2000) 111-154. | Zbl | MR

[2] L. Fuchs, Partially Ordered Algebraic Systems. Pergamon Press (1963). | Zbl | MR

[3] M.-H. Mourgues and J.P. Ressayré, Every real closed field has an integer part. J. Symbolic Logic 58 (1993) 641-647. | Zbl | MR

[4] S. Priess-Crampe, Angeordnete Strukturen: Gruppen, Körper, projektive Ebenen. Springer-Verlag, Berlin (1983). | Zbl | MR

[5] A. Rambaud, Quasi-analycité, o-minimalité et élimination des quantificateurs. PhD. Thesis. Université Paris 7 (2005). | MR

[6] J.P. Ressayre, Integer Parts of Real Closed Exponential Fields, Arithmetic, Proof Theory and Computational Complexity, edited by P. Clote and J. Krajicek, Oxford Logic Guides 23. | Zbl

[7] J.P. Ressayre, Gabrielov's theorem refined. Manuscript (1994).

[8] J.C. Shepherdson, A non-standard model for a free variable fragment of number theory. Bulletin de l'Academie Polonaise des Sciences 12 (1964) 79-86. | Zbl | MR

[9] L. Van Den Dries, Exponential rings, exponential polynomials and exponential functions. Pacific J. Math. 113 (1984) 51-66. | Zbl | MR

[10] A. Wilkie, Model completeness results for expansions of the ordered field of real numbers by restricted Pfaffian functions and the exponential function. J. Amer. Math. Soc. 9 (1996) 1051-1094. | Zbl | MR