Arithmetization of the field of reals with exponentiationextended 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 T-left perpendicular(right perpendicular) in the language of rings plus exponentiation such that the models (A, exp(A)) of T-left perpendicular(right perpendicular) are all integral parts A of models M of T with A(+) closed under exp(M) and exp(A) = exp(M) vertical bar 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) T-left perpendicular(exp) (right perpendicular) is recursively axiomatizable iff T-exp is decidable. T-left perpendicular(exp) (right perpendicular) implies LE0(x(y)) (least element principle for open formulas in the language <,+, x,- 1, x(y)) but the reciprocal is an open question. T-left perpendicular(exp) (right perpendicular) satisfies "provable polytime witnessing": if T-left perpendicular(exp) (right perpendicular) proves for all x there exists y : vertical bar y vertical bar < vertical bar x vertical bar(k)) R(x, y) (where vertical bar y vertical bar := (left perpendicular)log(y)(right perpendicular), k < w and R is an NP relation), then it proves for all 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 T-left perpendicular(exp) (right perpendicular) is a conservative extension of T-left perpendicular(exp) (right perpendicular) for sentences in for all Delta(0)(x(y)) (universal quanti. cations 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.
exponentiation computation with reals model theory o-minimality