Integer parts of real closed exponential fields. (English) Zbl 0791.03018

Ressayre, J.-P.

Clote, Peter (ed.) et al., Arithmetic, proof theory, and computational complexity. Oxford: Clarendon Press. Oxf. Logic Guides. 23, 278-288 (1993).

Let \(K\) be an ordered field, \(A\) a subring; \((K,2^ x)\) is an exponential field iff: \(2^ 1=2\), \(2^{x+y}= 2^ x\cdot 2^ y\), \(2^ x\) is an order morphism growing faster than \(x^ n\) \((n\in\mathbb{N})\) and having an inverse \(\log(y)\), defined for \(y>0\). And \(A\) is an Integer Part of \(K\) iff: every element \(x\) of \(K\) satisfies \([x]\leq x<[x]+ 1\) for a unique element \([x]\) of \(A\) – called the integer part of \(x\) in \(A\). If in addition \(A^ +\) is closed under \(2^ x\), then \(A\) is an Integer Part of \((K,2^ x)\).
Of course, \(\mathbb{Z}\) is the only Integer Part of \((K,2^ x)\) if \(K\) is Archimedean. If not, the existence of an Integer Part is a more delicate question; its solution below has unexpected consequences for the standard exponential field \((\mathbb{R},2^ x)\):
Theorem 1 – Every real closed exponential field has an Integer Part. Theorem 2 – The above axioms for exponential fields axiomatize the complete theory of \((\mathbb{R},2^ x)\), over the complete theory of \((\mathbb{R},2^ x|[0,1])\). Theorem 3 – If a function \(f\) is definable in \((\mathbb{R},2^ x)\), then there is a finite partition of its domain such that on each component, \(f\) equals some function obtained by composition from only: \(2^ x\), \(\log(y)\), and functions definable in \((\mathbb{R},2^ x|[0,1])\).
When \(K\) is non-Archimedean, one obtains \(A\), an Integer Part of \((K,2^ x)\) proving Theorem 1, by representing every element of \((K,2^ x)\) as a transfinite series \(\sum a_ i2^{\gamma_ i}\) – where \(i\) ranges over some ordinal, \(a_ i\in\mathbb{R}\), and \((\gamma_ i)\) is a decreasing sequence from \(K\); and by taking for \(A\) the set of elements of \(K\) which thus got represented by a series all of whose monomials \(a_ i 2^{\gamma_ i}\) are either infinite or in \(\mathbb{Z}\). This construction of \(A\) is the crux of the proof of Theorems 2 and 3, because it allows to construe the full function \(2^ x\) over \(K\) from its two parts \(2^ x|[0,1]\) and \(2^ x| A^ +\). And despite serious attempts to find more constructive proofs of these theorems, it remains so far essentially the only way to prove them.
The paper only outlines these proofs; a complete proof of a generalization of these results is included in: L. van den Dries, A. Macintyre, D. Marker, “The elementary theory of the restricted analytic field of the reals with exponentiation [Ann. Math., II. Ser. (to appear)].
For the entire collection see [Zbl 0777.00008].

Reviewer: J.-P.Ressayre (Paris)

MSC:

03C60	Model-theoretic algebra
03H15	Nonstandard models of arithmetic
14P99	Real algebraic and real-analytic geometry
03C62	Models of arithmetic and set theory

Keywords:

real exponential field; Integer Part