A theory $T$ has the *existence property* (EP) if the following holds:


Let $\phi(x)$ be a formula with one free variable (and no parameters) such that $T \vdash (\exists x) \phi(x)$. Then there is another formula $\psi(x)$ (again no parameters) such that $T \vdash (\exists ! x)\psi(x)$ (ie there is a unique $x$ such that $\psi(x)$) and $T \vdash(\forall x)\psi(x) \rightarrow \phi(x)$.


For example, $T := \operatorname{Th}(\langle \mathbb{C}, 0, 1, +, \times \rangle)$ *does not* have EP, because if one takes $\phi(x)$ to be $x^2 + 1 = 0$, then neither of the two solutions $\pm i$ is fixed by the automorphism $z \mapsto \bar{z}$.


The question I would like to ask is: Does the theory of ordered fields have the existence property?


I can see that $\operatorname{Th}(\langle \mathbb{R}, 0, 1, +, \times, < \rangle)$ *does* have EP. Since the theory is o-minimal, $\{x | \phi(x)\}$ is either finite, in which case it has a greatest element, or it contains an interval, in which case there is a rational, $q$ such that $\phi(q)$. Also, one can show that the theory of ordered fields with intuitionistic logic has EP using Kripke models. (Incidentally if that last remark is already known, I would be grateful if someone can provide a reference for it). However, I can't see how to adjust either proof to work with (classical) ordered fields in general.



Existence property for ordered fields
The answer is negative.


For any model $M$, let $M\_d$ denote the submodel of its parameter-free definable elements. We have the following characterization for classical theories.


**Lemma:** $T$ has EP iff $M\_d\preceq M$ for every $M\models T$.


**Proof:** $\leftarrow$ is left as an exercise. $\to$: By Tarski’s test, it suffices to show that whenever $M\models\exists x\,\phi(x,a\_1,\dots,a\_n)$ for some $a\_1,\dots,a\_n\in M\_d$, there is $b\in M\_d$ such that $M\models\phi(b,a\_1,\dots,a\_n)$. Since we can plug in the definition of each $a\_i$, it suffices to show this for $n=0$. We have $T\vdash\exists x\,(\exists y\,\phi(y)\to\phi(x))$, hence by EP, there exists $\psi(x)$ such that $T\vdash\exists!x\,\psi(x)$, and $T\vdash\exists y\,\phi(y)\to\forall x\,(\psi(x)\to\phi(x))$. Thus, if $b$ is the element defined by $\psi(x)$ in $M$, we have $M\models\phi(b)$. QED


So, the question is whether every ordered field is an elementary extension of its subfield of definable elements. Here is an easy counterexample.


**Example:** Let $F$ be the rational function field $\mathbb Q(x)$, ordered so that $x>q$ for every $q\in\mathbb Q$.


1. $F\_d=\mathbb Q$.
2. $F$ is not elementarily equivalent to $\mathbb Q$.


**Proof:**


1. For any $q\in\mathbb Q$, there is a unique automorphism $\sigma\_q$ of $F$ such that $\sigma\_q(x)=x+q$, specifically $\sigma\_q(f(x)/g(x))=f(x+q)/g(x+q)$. Definable elements are fixed by every automorphism, and it is easy to check that a rational function $f(x)/g(x)$ is fixed by $\sigma\_q$ for $q\ne0$ only when it is a constant.
2. In $\mathbb Q$, every positive element is the sum of four squares. This sentence does not hold in $F$. In particular, $x$ is not a sum of four (or more) squares, as we can make $\mathbb Q(x)$ into an ordered field in a different way so that $x$ becomes negative.


EDIT: Since this may be lost in the argument, let me state explicitly that an example of a formula $\phi(x)$ which violates EP in the theory of ordered fields is
\begin{multline}\forall y\,(y>0\to\exists z\_1,z\_2,z\_3,z\_4\,z\_1^2+z\_2^2+z\_3^2+z\_4^2=y)\\\lor (x>0\land\forall z\_1,z\_2,z\_3,z\_4\,z\_1^2+z\_2^2+z\_3^2+z\_4^2\ne x).\end{multline}


