RAIRO-Theor. Inf. Appl.
Volume 42, Number 1, January-March 2008A nonstandard spirit among computer scientists:a tribute to Serge Grigorieff at the occasion of his 60th birthday
|Page(s)||105 - 119|
|Published online||18 January 2008|
Arithmetization of the field of reals with exponentiation extended abstract
CNRS and Paris 7 University, France; email@example.com
(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 in the language of rings plus exponentiation such that the models (A, expA) of 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 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.
Mathematics Subject Classification: 03H15
Key words: Computation with reals / exponentiation / model theory / o-minimality
© EDP Sciences, 2007
Current usage metrics show cumulative count of Article Views (full-text article views including HTML views, PDF and ePub downloads, according to the available data) and Abstracts Views on Vision4Press platform.
Data correspond to usage on the plateform after 2015. The current usage metrics is available 48-96 hours after online publication and is updated daily on week days.
Initial download of the metrics may take a while.