
I write for the language of ordered exponential rings, for the the real ordered exponential field, and for its elementary theory. Recall that is model complete in by Wilkie's theorem, and that is ominimal.
I start with a few preliminary results that I actually didn't know were true in general.
Lemma
Proposition
Corollary
Proof. The underlying ordered set is saturated by definition of surreal numbers and by a simple fact (found in [1, Chapter 1]): if and are sets of surreal numbers with , then the simplest number with
has birthday .
We also know, by a result of Ehrlich and van den Dries [2], that and that can be expanded into a model of . Thus is ominimal.
Corollary
I was asking myself the following questions:
Question
Question
Lou found answers to those questions, which I next explain.
In order to answer the first question, in the negative, we require three objects:
We write for Hardy's field of logarithmicoexponential functions, i.e. germs at that can be obtained as compositions of , , and semialgebraic functions . In other words, this is the closure of the field of rational functions under real closure, and , which Hardy showed to be a Hardy field.
Let denote the Hardy field of germs at of definable functions , allowing parameters. Note that given a positive infinite germ , its functional inverse is also definable with parameters in , so .
Let be nonstandard, i.e. a proper elementary extension of . Fix an with . This exists since is the largest archimedean ordered field.
Proposition
Proof. Cheking all details is a bit tedious but I think this is a wellknown result. I just give the definition. Fix a representative of a germ in . There is a defining formula for with parameters and a real number such that for all , the number is unique with . Let be a second defining formula with parameters satisfying the same relation, with respect to the same germ, for a possibly distinct . In particular, we have
(1) 
Recall that is ominimal, so is an elementary embedding. We have , so by (1), the unique element of with is also the unique element of satisfying . We define to be that element .
Similar arguments show that commutes with definable functions , whence in particular that it is an embedding in , hence an elementary embedding by model completeness.
Proposition
Proof. Assume for contradiction that there is such an embedding and write . The field is contained in , and since must commute with semialgebraic functions as well as with and , we have . For the same reasons, we have . The function is injective, so must coincide with , whence in . But this is known to be false: for instance it is a theorem of van den Dries, Macintyre and Marker that the germ of the functional inverse of does not lie in .
This raises a question:
Question
The answer to the second question is positive. In order to embed into an elementary extension of , it is enough, since and by model completeness, to construe it as a substructure of a model of .
Proposition
Proof. We need to prove that is a model of the universal theory of . Consider a universal formula where is a boolean combination of atomic formulas, hence, up to equivalence modulo the theory of rings, of exponentialpolynomial equations, inequations, inequalities... We can assume that is in disjunctive conjunctive form
where each , each symbol is among , and , and are finite sets.
Assume that is valid in and let be representatives of germs in . Since is finite, there are a cofinal subset and an for which we have
whenever . Since is a Hardy field, the sign of each function
for is stationnary. So we actually have for all sufficiently large . This means that , whence in particular that . Therefore is valid in . This shows that embeds into a model of .
Corollary
Proof. We first embed into a Hardy field which is closed under . This is just done by closing under as explained in Lou's lecture. Then embed into a model of using Proposition 4, and conclude with Corollary 2.