Algebraic elements in ordered integral domain The following is a question of abstract algebra which is expressed using a model theoretical language. (I'm sorry, I'm not sufficiently fluent in algebra.)  

Let $N$ be an ordered integral domain, $M\subseteq N$ a subdomain, $b\in N$ algebraic over $M$, and $p(x) = {\rm qf\mbox{-}tp}(b/M)$.
Is $p(x)$ principal? That is, equivalent (over the theory of ordered integral domain and the diagram of $M$) to one of its finite subsets.

If you forget the order, $p(x)$ is equivalent to the formula $t(x)=0$ where $t(x)$ is the minimal polynomial over $M$ that has a zero in $b$. I guess that now the required formula has the form $t(x)=0\wedge a<x<c$ for some $a,c\in M$. But I cannot prove it.
 A: Yes. I think the easiest way to show this is to use the model theory of real closed fields. For the purposes of this answer, let's view the theory of real-closed fields ($\text{RCF}$) as a theory in the language of ordered integral domains. The key facts are that (1) $\text{RCF}$ has quantifier elimination in this language (actually, model-completeness is enough), and (2) every ordered integral domain extends to a model of $\text{RCF}$ (e.g. its real closure).
So let $R$ be a real closure of $N$. Since $p(x)$ contains some non-zero polynomial equation, it has only finitely many realizations in $R$, i.e. it is a model-theoretically algebraic type. An algebraic type is always isolated relative to a complete theory, so there is some formula $\varphi(x)\in p(x)$ such that $\varphi(x)$ implies all of $p(x)$ relative to $\text{RCF}_M = \text{RCF}\cup \text{ElDiag}(M)$ (this is the complete theory of $R$ in the language with constants naming every element of $M$).
Now we want to strengthen this to show that $\varphi(x)$ implies all of $p(x)$ relative to the incomplete theory $\text{OD}\cup \text{Diag}(M)$ of ordered integral domains together with the diagram of $M$. 
So suppose we have $M'\models \text{OD}\cup \text{Diag}(M)$ and $b'\in M'$, such that $M'\models \varphi(b')$. Let $R'$ be a real closure of $M'$. Then $R'\models \text{RCF}\cup \text{Diag}(M)$, and since $\text{RCF}$ has quantifier elimination, the ordinary diagram $\text{Diag}(M)$ implies the elementary diagram $\text{ElDiag}(M)$ relative to $\text{RCF}$, so $R'\models \text{RCF}_M$. Since $\varphi(x)$ is quantifier-free, also $R'\models \varphi(b')$, so $R'\models p(b')$. And since all the formulas in $p(x)$ are quantifier-free, also $M'\models p(b')$, as desired. 
