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), p. 105-119 / Harvested from Numdam

Résumé

(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 $_{\llcorner } T _{\lrcorner }$ in the language of rings plus exponentiation such that the models ($A$, exp$_A$) of $_{\llcorner } T _{\lrcorner }$ 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) $_{\llcorner }$${T_{\exp }}$$_{\lrcorner }$ is recursively axiomatizable iff $T_{\exp }$ is decidable. $_{\llcorner }$$ {T_{\exp }}$$_{\lrcorner }$ implies $LE_0(x^y)$ (least element principle for open formulas in the language $<,+,\times ,-1,x^y$) but the reciprocal is an open question. $_{\llcorner }$$ {T_{\exp }}$$_{\lrcorner }$ satisfies “provable polytime witnessing”: if $_{\llcorner } $$ {T_{\exp }}$$_{\lrcorner }$ proves $\forall x\exists y:|y|<|x|^k)R(x,y)$ (where $|y|:=_{\llcorner }$$ {\log (y)}$$_{\lrcorner }$, $k<\omega $ and $R$ is an NP relation), then it proves $\forall x\ R(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 $_{\llcorner } $${T_{\exp }}$$_{\lrcorner }$ is a conservative extension of $_{\llcorner } $$ {T_{\exp }} $$_{\lrcorner }$ for sentences in $\forall \Delta _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.

Détail

Publié le : 2008-01-01

MR 2382546 | Zbl 1144.03027

DOI : https://doi.org/10.1051/ita:2007048
Classification:  03H15

Bibliographie

[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 1782110 | Zbl 0959.03023

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

[3] 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

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

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

[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 0791.03018

[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 161798 | Zbl 0132.24701

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

[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 1398816 | Zbl 0892.03013