Real closed exponential fields
Volume 219 / 2012
Abstract
Ressayre considered real closed exponential fields and “exponential” integer parts, i.e., integer parts that respect the exponential function. In 1993, 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 and then analyze the complexity. Ressayre's construction is canonical once we fix the real closed exponential field $R$, a residue field section $k$, and a well ordering $\prec $ on $R$. The construction is clearly constructible over these objects. Each step looks effective, but there may be many steps. We produce an example of an exponential field $R$ with a residue field section $k$ and a well ordering $\prec $ on $R$ such that $D^c(R)$ is low and $k$ and $\prec $ are $\Delta ^0_3$, and Ressayre's construction cannot be completed in $L_{\omega _1^{\rm CK}}$.
