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

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].

### 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