Real closed exponential fields

TL;DR

This paper provides a detailed, constructive account of Ressayre's proof that every real closed exponential field has an exponential integer part, highlighting the complexity and limitations of the construction.

Contribution

It offers a detailed, effective construction of exponential integer parts in real closed exponential fields, clarifying Ressayre's original outline and demonstrating its limitations.

Findings

The construction is effective but may require many steps.

There exists an exponential field where the construction cannot be completed in $L_{\omega_1^{CK}}$.

The procedure depends on fixed objects like residue field sections and well orderings.

Abstract

In an extended abstract Ressayre considered real closed exponential fields and integer parts that respect the exponential function. He outlined a proof that every real closed exponential field has an exponential integer part. In the present paper, we give a detailed account of Ressayre's construction, which becomes canonical once we fix the real closed exponential field, a residue field section, and a well ordering of the field. The procedure is constructible over these objects; each step looks effective, but may require many steps. We produce an example of an exponential field $R$ with a residue field $k$ and a well ordering $<$ such that $D^c(R)$ is low and $k$ and $<$ are $\Delta^0_3$, and Ressayre's construction cannot be completed in $L_{\omega_1^{CK}}$.