Real closed exponential fields - D'Aquino, Paola; Knight, Julia F.; Kuhlmann, Salma; Lange, Karen (My University, 2012)
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 ≺ 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 ≺ on R such that Dc(R) is low and k and ≺ are Δ 0 3, and Ressayre's construction cannot be completed in LωCK1.
Keywords: 510