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.

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.