# Arithmetization of the field of reals with exponentiation extended abstract

Sedki Boughattas; Jean-Pierre Ressayre

RAIRO - Theoretical Informatics and Applications (2008)

- Volume: 42, Issue: 1, page 105-119
- ISSN: 0988-3754

## Access Full Article

top## Abstract

top## How to cite

topBoughattas, Sedki, and Ressayre, Jean-Pierre. "Arithmetization of the field of reals with exponentiation extended abstract." RAIRO - Theoretical Informatics and Applications 42.1 (2008): 105-119. <http://eudml.org/doc/250355>.

@article{Boughattas2008,

abstract = {
(1) Shepherdson proved that a discrete unitary commutative semi-ring
A+ satisfies IE0 (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, expA) of $_\{\llcorner\} T _\{\lrcorner\}$ are all integral parts A of models
M of T with A+ closed under expM and
expA = expM | A+. Namely T = EXP, the basic theory of
real exponential fields; T = EXP+ the Rolle and the intermediate
value properties for all 2x-polynomials; and T = Texp, the
complete theory of the field of reals with exponentiation.
(2)$_\{\llcorner\}$Texp$_\{\lrcorner\}$ is recursively axiomatizable iff Texp is
decidable. $_\{\llcorner\}$Texp$_\{\lrcorner\}$ implies LE0(xy) (least element
principle for open formulas in the language <,+,x,-1,xy)
but the reciprocal is an open question. $_\{\llcorner\}$Texp$_\{\lrcorner\}$ satisfies
“provable polytime witnessing”: if $_\{\llcorner\} $Texp$_\{\lrcorner\}$ proves ∀x∃y : |y| < |x|k)R(x,y) (where $|y|:=_\{\llcorner\}$log(y)$_\{\lrcorner\}$, k < ω
and R is an NP relation), then it proves ∀x R(x,ƒ(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\} $Texp$_\{\lrcorner\}$ is a
conservative extension of $_\{\llcorner\} $Texp$_\{\lrcorner\}$ for sentences in
∀Δ0(xy) (universal quantifications of bounded
formulas in the language of rings plus xy). 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.
},

author = {Boughattas, Sedki, Ressayre, Jean-Pierre},

journal = {RAIRO - Theoretical Informatics and Applications},

keywords = {Computation with reals; exponentiation; model theory; o-minimality; computation with reals},

language = {eng},

month = {1},

number = {1},

pages = {105-119},

publisher = {EDP Sciences},

title = {Arithmetization of the field of reals with exponentiation extended abstract},

url = {http://eudml.org/doc/250355},

volume = {42},

year = {2008},

}

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

DA - 2008/1//

PB - EDP Sciences

VL - 42

IS - 1

SP - 105

EP - 119

AB -
(1) Shepherdson proved that a discrete unitary commutative semi-ring
A+ satisfies IE0 (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, expA) of $_{\llcorner} T _{\lrcorner}$ are all integral parts A of models
M of T with A+ closed under expM and
expA = expM | A+. Namely T = EXP, the basic theory of
real exponential fields; T = EXP+ the Rolle and the intermediate
value properties for all 2x-polynomials; and T = Texp, the
complete theory of the field of reals with exponentiation.
(2)$_{\llcorner}$Texp$_{\lrcorner}$ is recursively axiomatizable iff Texp is
decidable. $_{\llcorner}$Texp$_{\lrcorner}$ implies LE0(xy) (least element
principle for open formulas in the language <,+,x,-1,xy)
but the reciprocal is an open question. $_{\llcorner}$Texp$_{\lrcorner}$ satisfies
“provable polytime witnessing”: if $_{\llcorner} $Texp$_{\lrcorner}$ proves ∀x∃y : |y| < |x|k)R(x,y) (where $|y|:=_{\llcorner}$log(y)$_{\lrcorner}$, k < ω
and R is an NP relation), then it proves ∀x R(x,ƒ(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} $Texp$_{\lrcorner}$ is a
conservative extension of $_{\llcorner} $Texp$_{\lrcorner}$ for sentences in
∀Δ0(xy) (universal quantifications of bounded
formulas in the language of rings plus xy). 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.

LA - eng

KW - Computation with reals; exponentiation; model theory; o-minimality; computation with reals

UR - http://eudml.org/doc/250355

ER -

## References

top- S. Boughattas, Trois Théorèmes sur l'induction pour les formules ouvertes munies de l'exponentielle. J. Symbolic Logic65 (2000) 111–154.
- L. Fuchs, Partially Ordered Algebraic Systems. Pergamon Press (1963). Zbl0137.02001
- M.-H. Mourgues and J.P. Ressayré, Every real closed field has an integer part. J. Symbolic Logic58 (1993) 641–647. Zbl0786.12005
- S. Priess-Crampe, Angeordnete Strukturen: Gruppen, Körper, projektive Ebenen. Springer-Verlag, Berlin (1983). Zbl0558.51012
- A. Rambaud, Quasi-analycité, o-minimalité et élimination des quantificateurs. PhD. Thesis. Université Paris 7 (2005).
- 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. Zbl0791.03018
- J.P. Ressayre, Gabrielov's theorem refined. Manuscript (1994).
- J.C. Shepherdson, A non-standard model for a free variable fragment of number theory. Bulletin de l'Academie Polonaise des Sciences12 (1964) 79–86. Zbl0132.24701
- L. van den Dries, Exponential rings, exponential polynomials and exponential functions. Pacific J. Math.113 (1984) 51–66. Zbl0603.13019
- 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. Zbl0892.03013

## NotesEmbed ?

topTo embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.