Arithmetization of the field of reals with exponentiation extended abstract
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}↾{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 $<,+,×,-1,{x}^{y}$) but the reciprocal is an open question. ${}_{⌞}$${T}_{exp}$${}_{⌟}$ satisfies “provable polytime witnessing”: if ${}_{⌞}$${T}_{exp}$${}_{⌟}$ proves ${\forall x\exists y:|y|<|x|}^{k}\right)R\left(x,y\right)$ (where $|y|:{=}_{⌞}$$log\left(y\right)$${}_{⌟}$, $k<\omega$ and $R$ is an NP relation), then it proves $\forall x\phantom{\rule{4pt}{0ex}}R\left(x,f\left(x\right)\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.

DOI : https://doi.org/10.1051/ita:2007048
Classification : 03H15
Mots clés : computation with reals, exponentiation, model theory, o-minimality
@article{ITA_2008__42_1_105_0,
author = {Boughattas, Sedki and Ressayre, Jean-Pierre},
title = {Arithmetization of the field of reals with exponentiation extended abstract},
journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications},
pages = {105--119},
publisher = {EDP-Sciences},
volume = {42},
number = {1},
year = {2008},
doi = {10.1051/ita:2007048},
zbl = {1144.03027},
mrnumber = {2382546},
language = {en},
url = {http://www.numdam.org/articles/10.1051/ita:2007048/}
}
TY  - JOUR
AU  - Boughattas, Sedki
AU  - Ressayre, Jean-Pierre
TI  - Arithmetization of the field of reals with exponentiation extended abstract
JO  - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
PY  - 2008
DA  - 2008///
SP  - 105
EP  - 119
VL  - 42
IS  - 1
PB  - EDP-Sciences
UR  - http://www.numdam.org/articles/10.1051/ita:2007048/
UR  - https://zbmath.org/?q=an%3A1144.03027
UR  - https://www.ams.org/mathscinet-getitem?mr=2382546
UR  - https://doi.org/10.1051/ita:2007048
DO  - 10.1051/ita:2007048
LA  - en
ID  - ITA_2008__42_1_105_0
ER  -
Boughattas, Sedki; Ressayre, Jean-Pierre. Arithmetization of the field of reals with exponentiation extended abstract. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 42 (2008) no. 1, pp. 105-119. doi : 10.1051/ita:2007048. http://www.numdam.org/articles/10.1051/ita:2007048/

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

 L. Fuchs, Partially Ordered Algebraic Systems. Pergamon Press (1963). | MR 171864 | Zbl 0137.02001

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

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

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

 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 0791.03018

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

 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. | MR 161798 | Zbl 0132.24701

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

 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. | MR 1398816 | Zbl 0892.03013

Cité par Sources :