Schanuel’s Conjecture and the Decidability of the Real Exponential Field

Abstract

In [5] I showed that the theory of the real exponential field, i.e. the theory T _exp of the structure R _exp := 〈R; +, ·, -, 0, 1, exp, <〉 is model complete. Subsequently, in the paper[4], Macintyre and I settled, conditionally, an old question of Tarski concerning the decidability of Texp. We showed that if a certain famous conjecture from transcendental number theory, namely Schanuel’s conjecture, is true then T _exp is, indeed, a decidable theory and in this lecture I am happy to comply with the organizers’ suggestion that I explain precisely the rôle played by this conjecture in the verification of the algorithm.