Existence property for ordered fields

Question

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.

Answer 1

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}