On the elementary theory of the real exponential field

TL;DR

Under Schanuel's conjecture, the paper characterizes the complete theory of the real exponential field, showing it is axiomatized by definably complete exponential fields and establishing its decidability, with an unconditional result on a restricted exponential function.

Contribution

It provides a new axiomatization of the real exponential field's theory assuming Schanuel's conjecture and proves its decidability, including an unconditional result for a restricted exponential function.

Findings

Complete theory of the real exponential field is axiomatized by definably complete exponential fields.

Under Schanuel's conjecture, the theory is decidable.

Unconditional proof of model completeness for the exponential function on (-1,1).

Abstract

Assuming Schanuel's conjecture, we prove that the complete theory $T_{\exp}$ of the real exponential field is axiomatized by the axioms of definably complete exponential fields satisfying $\exp' = \exp$. This implies the result of Macintyre and Wilkie that, under the same conjecture, $T_{\exp}$ is decidable. Our approach is based on the model completeness of a similar set of axioms for the exponential function restricted to $(-1,1)$, which we prove unconditionally.