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

Résumé

(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.

Détail

DOI : 10.1051/ita:2007048

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