Integer Parts of Real Closed Exponential Fields
J -P Ressayrc · 1993
Abstract This paper is an extended abstract: the detailed proofs an being prepared for future publication. We define real exponential fields as ordered fields with a function 2x satisfying a set E of four basic axioms. We show that every real closed exponential field in this sense possesses an “integer part”, that is a discrete subring Z such that z+ is closed under 2x, and every element x of the field has an “integer part” ⌊ x ⌋ ∈ Z, such that ⌊ x ⌋ ≤ x <: ⌊ x ⌋ + 1. By using such integer parts, we show that Th(ℝ, 2x) is equivalent to E + Th(ℝ, 21/(H-x3); and we deduce the model completeness of Th(ℝ,2x) from the model completeness ofTh(ℝR,21/(l+x2 )by an argument which differs from Wilkie’s original proof.