RAIRO - Theoretical Informatics and Applications (RAIRO: ITA)

| Abstract | PDF (227.7 KB) | References |

RAIRO-Theor. Inf. Appl. 42, 105-119 (2008)
DOI: 10.1051/ita:2007048

Arithmetization of the field of reals with exponentiation extended abstract

Sedki Boughattas and Jean-Pierre Ressayre

CNRS and Paris 7 University, France; bougatas@logique.jussieu.fr

(Published online: 18 January 2008)

Abstract

(1) Shepherdson proved that a discrete unitary commutative semi-ring A⁺ satisfies IE₀ (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₀(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:\vert y\vert<\vert x\vert^k)R(x,y)$ (where $\vert y\vert:=_{\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.

Mathematics Subject Classification. 03H15

Key words: Computation with reals -- exponentiation -- model theory -- o-minimality

© EDP Sciences 2007