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.