Real Ordered Field – Is This the Complete Theory?

Question

We know that the real ordered field can be characterized up to isomorphism as a complete ordered field. However this is a second order characterization. That raises the following question. Consider the following theory. We take as axioms the axioms for ordered fields, and then add an axiom schema that states that every nonempty set that is definable without parameters that is bounded above has a least upper bound. Is that theory the complete first order theory of the real ordered field? And if it is not, can someone exhibit a model of that theory that is not elementarily equivalent to the real ordered field? I asked this question on math stack exchange, but I did not receive an answer.

Answer 1

It is not. Using set forcing, we can add 'undefinable' reals in a controlled manner, while keeping complexity of parameter-free definable sets low.

Specifically, let $M$ be a countable $ω$-model of ZFC\P, real $r$ be Cohen generic over $M$, and $ℝ_M(r)$ be the minimal field of reals containing $r$ and all reals in $M$ (in the initial revision, I called it $ℚ_M(r)$; it is a proper subset of $ℝ^{M[r]}$). Then, in $ℝ_M(r)$, every parameter-free definable bounded subset has the least upper bound, but $\sqrt{|r|}$ does not exist.

Because $r$ is transcendental over $M$, $\sqrt{|r|}∉ℝ_M(r)$.

Next, let $X$ be a bounded set of reals parameter-free definable in $ℝ_M(r)$. $ℝ_M(r)$ may not be closed under square roots, but it witnesses that the Cohen forcing is homogeneous, and therefore $\sup(X)∈M$, as required.

In more detail, by genericity, $\sup(X)$ can be determined with arbitrary given precision by a forcing condition (with the forcing relation definable in $M$). For Cohen forcing (modulo choice of representation), the conditions are rational $p<t$ (asserting $p<r<t$). Now, if $r$ is Cohen generic, then so is $qr$ for all nonzero $q∈ℚ$, and $ℝ_M(qr) = ℝ_M(r)$ (and same with $q+r$), and therefore all conditions lead to the same $\sup(X)$.

An interesting remaining question is whether there are computable examples.