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

Abstract

top

 (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 ⌞ T ⌟ in the language of rings plus exponentiation such that the models (A, expA) of ⌞ T ⌟ 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) ⌞ Texp ⌟ is recursively axiomatizable iff Texp is decidable.  ⌞ Texp ⌟ implies LE0(xy) (least element principle for open formulas in the language <,+,x,-1,xy) but the reciprocal is an open question. ⌞ Texp ⌟ satisfies “provable polytime witnessing”: if ⌞ Texp ⌟ proves ∀x∃y : |y| < |x|k)R(x,y) (where | y | : = ⌞ log(y) ⌟ , 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 ⌞ Texp ⌟ is a conservative extension of ⌞ Texp ⌟ 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.


How to cite

top

Boughattas, 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
  1. S. Boughattas, Trois Théorèmes sur l'induction pour les formules ouvertes munies de l'exponentielle. J. Symbolic Logic65 (2000) 111–154.  
  2. L. Fuchs, Partially Ordered Algebraic Systems. Pergamon Press (1963).  
  3. M.-H. Mourgues and J.P. Ressayré, Every real closed field has an integer part. J. Symbolic Logic58 (1993) 641–647.  
  4. S. Priess-Crampe, Angeordnete Strukturen: Gruppen, Körper, projektive Ebenen. Springer-Verlag, Berlin (1983).  
  5. A. Rambaud, Quasi-analycité, o-minimalité et élimination des quantificateurs. PhD. Thesis. Université Paris 7 (2005).  
  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.  
  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 Sciences12 (1964) 79–86.  
  9. L. van den Dries, Exponential rings, exponential polynomials and exponential functions. Pacific J. Math.113 (1984) 51–66.  
  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.  

NotesEmbed ?

top

You must be logged in to post comments.

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

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.