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.

  • 1
    $\begingroup$ It seems that the EP (is you call it) is slightly weaker than the theory having "Definable Skolem Functions." If so, it is known that all o-minimal structures (which admit a group structure, at least) have this property (for an interval, either take the midpoint or etc.), which can help generalize your argument for RCF to cases where the $\phi$ can have parameters. Just in case you're still interested in this property. $\endgroup$ Aug 16, 2013 at 16:25

1 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$.


  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}


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.