(1) Shepherdson proved that a discrete unitary commutative semi-ring satisfies (induction scheme restricted to quantifier free formulas) iff 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 range over axiom systems for ordered fields with exponentiation; for three values of we provide a theory in the language of rings plus exponentiation such that the models (, exp) of are all integral parts of models of with closed under exp and . Namely = EXP, the basic theory of real exponential fields; = EXP+ the Rolle and the intermediate value properties for all -polynomials; and = , the complete theory of the field of reals with exponentiation. (2) is recursively axiomatizable iff is decidable. implies (least element principle for open formulas in the language ) but the reciprocal is an open question. satisfies “provable polytime witnessing”: if proves (where , and is an NP relation), then it proves for some polynomial time function . (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 is a conservative extension of for sentences in (universal quantifications of bounded formulas in the language of rings plus ). 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.
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] 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] Partially Ordered Algebraic Systems. Pergamon Press (1963). | MR | Zbl
,[3] Every real closed field has an integer part. J. Symbolic Logic 58 (1993) 641-647. | MR | Zbl
and ,[4] Angeordnete Strukturen: Gruppen, Körper, projektive Ebenen. Springer-Verlag, Berlin (1983). | MR | Zbl
,[5] Quasi-analycité, o-minimalité et élimination des quantificateurs. PhD. Thesis. Université Paris 7 (2005). | MR
,[6] 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] Gabrielov's theorem refined. Manuscript (1994).
,[8] 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] Exponential rings, exponential polynomials and exponential functions. Pacific J. Math. 113 (1984) 51-66. | MR | Zbl
,[10] 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 :