Issue |
RAIRO-Theor. Inf. Appl.
Volume 42, Number 1, January-March 2008
A nonstandard spirit among computer scientists:a tribute to Serge Grigorieff at the occasion of his 60th birthday
|
|
---|---|---|
Page(s) | 105 - 119 | |
DOI | https://doi.org/10.1051/ita:2007048 | |
Published online | 18 January 2008 |
Arithmetization of the field of reals with exponentiation extended abstract
CNRS and Paris 7 University, France; bougatas@logique.jussieu.fr
(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.