View source for Model theory of the real exponential function

A branch of [[Model theory|model theory]] studying the [[Elementary theory|elementary theory]] <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m110/m110160/m1101601.png" /> of the ordered [[Field|field]] <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m110/m110160/m1101602.png" /> of real numbers with the real exponential function <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m110/m110160/m1101603.png" /> (cf. [[Exponential function, real|Exponential function, real]]). It is motivated by Tarski's question [[#References|[a7]]], p. 45, whether <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m110/m110160/m1101604.png" /> is decidable.

A. Wilkie showed in [[#References|[a8]]] that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m110/m110160/m1101605.png" /> is model complete. Combining this with Khovanskii's finiteness theorem [[#References|[a5]]], it follows that this theory is [[O-minimal|<img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m110/m110160/m1101606.png" />-minimal]]. In fact, Wilkie first studies expansions (cf. [[Structure(2)|Structure]]) of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m110/m110160/m1101607.png" /> by a Pfaffian chain of functions (see also [[#References|[a2]]]): Fix <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m110/m110160/m1101608.png" /> and an open set <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m110/m110160/m1101609.png" /> containing the closed unit box <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m110/m110160/m11016010.png" />. A Pfaffian chain of functions on <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m110/m110160/m11016011.png" /> is a sequence <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m110/m110160/m11016012.png" /> of analytic functions (cf. [[Analytic function|Analytic function]]) for which there exist polynomials <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m110/m110160/m11016013.png" /> (for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m110/m110160/m11016014.png" />; <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m110/m110160/m11016015.png" />) such that

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m110/m110160/m11016016.png" /></td> </tr></table>

for all <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m110/m110160/m11016017.png" />. Wilkie shows that the expansion of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m110/m110160/m11016018.png" /> by a Pfaffian chain of functions restricted to the closed unit box has a model-complete theory. In particular, the expansion <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m110/m110160/m11016019.png" /> of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m110/m110160/m11016020.png" /> by the restricted exponential function has a model-complete theory. Wilkie then deduces the model completeness of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m110/m110160/m11016021.png" /> from this last result. An alternative proof of the model completeness, and an axiomatization of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m110/m110160/m11016022.png" /> over <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m110/m110160/m11016023.png" />, was found by J.P. Ressayre in 1991 (see [[#References|[a3]]] for a generalization of Ressayre's result).

In [[#References|[a6]]], A. Macintyre and Wilkie show that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m110/m110160/m11016024.png" /> is decidable provided that the real version of Schanuel's conjecture (cf. [[Algebraic independence|Algebraic independence]]) is true.

The theory <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m110/m110160/m11016025.png" /> does not admit [[Elimination of quantifiers|elimination of quantifiers]]. In fact, an expansion of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m110/m110160/m11016026.png" /> by a family of total real-analytic functions (see [[#References|[a1]]]) admits elimination of quantifiers if and only if each function is semi-algebraic, i.e., has a semi-algebraic graph (cf. [[Semi-algebraic set|Semi-algebraic set]]). However, let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m110/m110160/m11016027.png" /> denote the family of restricted real-analytic functions, i.e., functions <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m110/m110160/m11016028.png" />, for all <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m110/m110160/m11016029.png" />, which are given on <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m110/m110160/m11016030.png" /> by a power series converging on a neighbourhood of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m110/m110160/m11016031.png" /> and are set equal to <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m110/m110160/m11016032.png" /> outside of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m110/m110160/m11016033.png" />. It is shown in [[#References|[a3]]] that the expansion <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m110/m110160/m11016034.png" /> admits elimination of quantifiers. The authors also give a complete axiomatization of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m110/m110160/m11016035.png" />, and establish that it is <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m110/m110160/m11016036.png" />-minimal. In [[#References|[a4]]] they construct a model of this theory which is not Archimedean and use it to solve a problem raised by G.H. Hardy: they show that the compositional inverse of the function <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m110/m110160/m11016037.png" /> is not asymptotic at <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m110/m110160/m11016038.png" /> to a composition of semi-algebraic functions, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m110/m110160/m11016039.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m110/m110160/m11016040.png" />.


====References====
<table><TR><TD valign="top">[a1]</TD> <TD valign="top">  L. van den Dries,   "Remarks on Tarski's problem concerning  $({\bf R},+,\cdot,\exp)$"  G. Lolli (ed.)  G. Longo (ed.)  A. Marcja (ed.) , ''Logic Colloquium '82'' , North-Holland  (1984)  pp. 97–121</TD></TR>
<TR><TD valign="top">[a2]</TD> <TD valign="top">  L. van den Dries,   "Tarski's problem and Pfaffian functions"  J.B. Paris (ed.)  A.J. Wilkie (ed.)  G.M. Wilmers (ed.) , ''Logic Colloquium '84'' , North-Holland  (1986)  pp. 59–90</TD></TR>
<TR><TD valign="top">[a3]</TD> <TD valign="top">  L. van den Dries,   A.J. Macintyre,   D. Marker,   "The elementary theory of restricted analytic fields with exponentiation"  ''Ann. of Math.'' , '''140'''  (1994)  pp. 183–205</TD></TR>
<TR><TD valign="top">[a4]</TD> <TD valign="top">  L. van den Dries,   A.J. Macintyre,   D. Marker,   "Logarithmic-exponential power series"  ''J. London Math. Soc.'' '''56''' (1997) 417-434.  Zbl 0924.12007</TD></TR>
<TR><TD valign="top">[a5]</TD> <TD valign="top">  A. Khovanskii,   "On a class of systems of transcendental equations"  ''Soviet Math. Dokl.'' , '''22'''  (1980)  pp. 762–765  (In Russian)</TD></TR>
<TR><TD valign="top">[a6]</TD> <TD valign="top">  A.J. Macintyre,   A.J. Wilkie,   "On the decidability of the real exponential field"  P.G. Odifreddi (ed.) , ''Kreisel 70th Birthday Volume'' , CLSI  (1995)</TD></TR>
<TR><TD valign="top">[a7]</TD> <TD valign="top">  A. Tarski,   J.C.C. McKinsey,   "A decision method for elementary algebra and geometry" , Univ. California Press  (1951)</TD></TR>
<TR><TD valign="top">[a8]</TD> <TD valign="top">  A.J. Wilkie,   "Model completeness results for expansions of the ordered field of real numbers by restricted Pfaffian functions and the exponential function"  ''J. Amer. Math. Soc.'' , '''9''' :  4  (1996)</TD></TR></table>