Arithmetization of the field of reals with exponentiation extended abstract

Issue		RAIRO-Theor. Inf. Appl. Volume 42, Number 1, January-March 2008 A nonstandard spirit among computer scientists: a tribute to Serge Grigorieff at the occasion of his 60th birthday


Page(s)		105 - 119
DOI		10.1051/ita:2007048
Published online		18 January 2008

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

What is OpenURL?

The OpenURL standard is a protocol for transmission of metadata describing the resource that you wish to access. An OpenURL link contains article metadata and directs it to the OpenURL server of your choice. The OpenURL server can provide access to the resource and also offer complementary services (specific search engine, export of references...). The OpenURL link can be generated by different means.

If your librarian has set up your subscription with an OpenURL resolver, OpenURL links appear automatically on the abstract pages.
You can define your own OpenURL resolver with your EDPS Account. In this case your choice will be given priority over that of your library.
You can use an add-on for your browser (Firefox or I.E.) to display OpenURL links on a page (see http://www.openly.com/openurlref/). You should disable this module if you wish to use the OpenURL server that you or your library have defined.