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 IE 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 LE 0 (x y ) (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 xy:|y|<|x| k )R(x,y) (where |y|:= log(y) , k<ω and R is an NP relation), then it proves xR(x,f(x)) 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 Δ 0 (x y ) (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 : 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},
     mrnumber = {2382546},
     zbl = {1144.03027},
     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
SP  - 105
EP  - 119
VL  - 42
IS  - 1
PB  - EDP-Sciences
UR  - http://www.numdam.org/articles/10.1051/ita:2007048/
DO  - 10.1051/ita:2007048
LA  - en
ID  - ITA_2008__42_1_105_0
ER  - 
%0 Journal Article
%A Boughattas, Sedki
%A Ressayre, Jean-Pierre
%T Arithmetization of the field of reals with exponentiation extended abstract
%J RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
%D 2008
%P 105-119
%V 42
%N 1
%I EDP-Sciences
%U http://www.numdam.org/articles/10.1051/ita:2007048/
%R 10.1051/ita:2007048
%G en
%F ITA_2008__42_1_105_0
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/

[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. | MR | Zbl

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

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

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

[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. | MR | Zbl

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

[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. | MR | Zbl

Cité par Sources :