Arithmetization of the field of reals with exponentiation extended abstract
Sedki Boughattas, Jean-Pierre Ressayre · RAIRO - Theoretical Informatics and Applications · 2008
(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.