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.
-
1$\begingroup$ @WillSawin The issue is that OP's theory only has axioms like that for sets definable without parameters. The sets you're using are defined with parameters -- $a$ in the first case, and the coefficients of $f$ in the second. But in some sense the theory where you allow sets definable with parameters into the scheme is probably the more natural one to use anyway. $\endgroup$– Tim CampionCommented Feb 6, 2021 at 2:02
-
3$\begingroup$ In the MSE question, the OP also mentions that they discussed the theory where you allow parameters several years ago in a prequel MSE question, which Asaf Karagila answered. It's worth mentioning that for the current question, Noah Schweber says on MSE he suspects a counterexample is given by taking $\mathbb R^{alg}(\pi)$, say. I'd also suggest comparing to the natural analog of this question in the field language rather than the ordered field language. $\endgroup$– Tim CampionCommented Feb 6, 2021 at 2:15
-
2$\begingroup$ @MattF. Yeah, the part that's not obvious (and the reason Noah didn't definitively claim it was a counterexample) is whether it does satisfy all the unparameterized LUB axioms. It's confusing to me because if we were working over RCF already, you could say that all the definable sets are just finite unions of intervals (i.e. RCF is o-minimal), and approach what the axioms look like that way. But I don't know how to extend the language of ordered fields to eliminate quantifiers, so you've got to to think about syntactically much more complicated formulas when "enumerating" all the LUB axioms. $\endgroup$– Tim CampionCommented Feb 6, 2021 at 3:11
-
1$\begingroup$ @TimCampion Ah, I see. I missed "without parameters". This question is interesting! $\endgroup$– Will SawinCommented Feb 6, 2021 at 14:59
-
5$\begingroup$ @WillSawin Well, I have one deleted answer where I missed this, you missed it, Ali Enayat's answer missed this, and when the OP originally asked the question in 2015, Asaf Karagila naturally assumed the OP meant "with parameters". Judging by the comments on that question, it appears that the OP themself didn't notice the discrepancy until two years later in 2017! $\endgroup$– Tim CampionCommented Feb 6, 2021 at 15:02
6 Answers
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.
-
$\begingroup$ I don't follow the argument that $\text{sup}(X)$ is in $M$. Fix a first-order formula $\varphi(x)$, let $X\subseteq \mathbb{Q}_M(r)$ be the set defined by $\varphi(x)$ in this field, and assume $X$ is bounded in $\mathbb{Q}_M(r)$. I agree that for rational $p < q$, the property $p<\sup(X)<q$ is determined by a forcing condition, and all conditions agree on all properties of this form. Why does this imply that $\sup(X)\in M$? $\endgroup$ Commented Mar 1, 2021 at 2:12
-
1$\begingroup$ @AlexKruckman Correct. (Also, forcing is useful in model theory.) $\endgroup$ Commented Mar 1, 2021 at 2:56
-
1$\begingroup$ Since $\mathbb Q_M(r)$ is generated by the reals of $M$, rather than the rationals of $M$, shouldn't it be denoted $\mathbb R_M(r)$? (This kept tripping me when trying to understand the argument.) $\endgroup$ Commented Mar 1, 2021 at 10:13
-
1$\begingroup$ Thank you. A nice argument, by the way. $\endgroup$ Commented Mar 1, 2021 at 12:11
-
1$\begingroup$ I suppose you already know this, but let me mention explicitly in connection to the last question that no model elementarily equivalent to $\mathbb R_M(r)$ is computable, and the first-order theory of $\mathbb R_M(r)$ is highly undecidable. Indeed, the results on definability in simple transcendental extensions quoted in comments by @AlexKruckman show that $\mathbb R_M$ and $\mathbb N$ are definable in $\mathbb R_M(r)$, from which it follows easily that the full second-order arithmetic structure of the ground model $(\mathbb N,\mathcal P_M(\mathbb N))$ is interpretable in $\mathbb R_M(r)$. $\endgroup$ Commented Mar 1, 2021 at 22:28
Noah Schweber suggested on math stack exchange that $\mathbb Q^{alg}(r)$ could satisfy this weak least upper bound property for some fixed transcendental number $r$, say $r=\pi$. In this case, it would be a counterexample.
I think this may be true, but I don't think it is possible to prove with current technology.
Consider definable sets of the form $$ \exists y \exists z \textrm{ such that } f(x,y,z)=0, -1 \leq y \leq 1, -1 \leq z \leq 1 , \textrm{ and } \forall w, y+1 \neq w^2$$ for a complicated polynomial $f$.
Then $x,y,z$ must lie on a bounded subset of the surface $S$ defined by the equation $f$. The last condition forces $y \notin \mathbb Q^{alg}$, so $(x,y,z)$ must lie on the intersection of a rational curve with this bounded subset. Unless this rational curve has a very particular form, possible $(x,y,z)$ are dense on any intersection of a rational curve with a bounded subset, since almost any rational function in $\pi$ will not be a perfect square.
Does this set have a supremum?
It might be reasonable to guess that rational curves on $S$ are either dense in the real topology, or contained in some proper closed subset, and in either case there exists a supremum, since we could either ignore the last condition or replace it with an additional equation, and in either case solve it in the usual real closed fields way.
But we can't prove this for an arbitrary surface. If neither is true, the topological closure of the space of rational curves could be some weird transcendental thing, and the supremum would be a bizarre transcendental.
This problem motivates an alternative proposal to find a "counterexample". If this theory is complete, it certainly proves $\forall x, x>0 \implies \exists y, y^2=x$. If so, then it proves this using finitely many axioms, and thus finitely many parameter-free definable sets. We can try to show this is impossible by showing that these finitely many parameter-free definable sets admit least upper bounds (or are unbounded) in $\mathbb Q(r_1,\dots, r_n)$, where $r_1,\dots,r_n$ are independent transcendentals.
The trick here is that definable sets like the one above have "true" least upper bounds in $\mathbb R$ that are insensitive to our choice of $r_1,\dots, r_n$, so we can simply choose $r_i$ to be the least upper bounds of the finitely many paramater-free definable sets, if any of them are transcendental.
The difficulty with this approach is that the "true" least upper bound of other parameter-free definable sets could potentially depend on our choice of $r_1,\dots,r_n$. It could theoretically be that no choice works because the least upper bound keeps jumping around to confound us.
This technique does, at least, answer Tim Campion's question about whether the theory of an ordered field with the axiom scheme that every bounded set definable without parameters in the language of a \emph{field} (not the language of an ordered field) has an upper bound.
Every set definable without parameters in the language of a field is independent of the ordering, by definition, and thus independent of the choice of transcendentals $r_1,\dots, r_n$. In particular, if it contains any nonconstant rational function in $r_1,\dots, r_n$, then it is unbounded. If it does not contain any nonconstant rational function in $r_1,\dots, r_n$, then it is contained in $\mathbb Q^{alg}$ and independent of $r_1,\dots, r_n$. Therefore its least upper bound, if it exists, is independent of $r_1,\dots, r_n$.
So given any finite set of parameter-free definable sets in the language of a field, we can choose $n$ to be at least the the number of sets, and then choose $r_1,\dots, r_n$ to be the least upper bounds of these sets, if any are transcendental, or arbitrary transcendentals, otherwise, showing that these finite set having least upper bounds does not imply that all positive numbers are squares.
-
5$\begingroup$ I think $\mathbb{Q}^{\text{alg}}(r)$ cannot be an example for any transcendental $r$. It's a theorem that $\mathbb{N}$ is definable in $\mathbb{Q}^{\text{alg}}(r)$ (see Theorem 3.29 in Model Theoretic Algebra by Jensen and Lenzing). Using the arithmetic on $\mathbb{N}$, we can carry out computations, so the cut corresponding to any computable real number should be definable. But there are always computable reals which are not in $\mathbb{Q}^{\text{alg}}(r)$. $\endgroup$ Commented Mar 1, 2021 at 3:35
-
2$\begingroup$ @AlexKruckman Did not know that theorem - that definitely ruins my suspicion! $\endgroup$ Commented Mar 1, 2021 at 3:39
-
1$\begingroup$ At the risk of being a broken record....it'd be interesting to see the definition of $\mathbb{N}$ in $\mathbb{Q}^{\text{alg}}(r)$ explicitly. $\endgroup$– user44143Commented Mar 1, 2021 at 14:23
-
2$\begingroup$ @MattF. Let $R$ be real closed and $t$ transcendental over $R$. Step 1: $x\in R$ is definable in $R(t)$ by $\exists y (1+x^4 = y^2)$. Step 2: Define $x\leq_2 y$ if $y-x$ is a sum of two squares in $R(t)$. Step 3: $n\in \mathbb{N}$ is definable in $R(t)$ using $t$ as a parameter by $\varphi(n,t)$: $$n\in R\land \exists x (x\neq 0 \land x^2\leq_2 t^2\land \forall y\in R ((y\neq n \land x^2\leq_2(t-y)^2)\to x^2\leq_2 (t-y-1)^2))).$$ Step 4: Remove the parameter for $t$ by $$n\in \mathbb{N}\iff \forall x(\varphi(0,x)\land \forall y\in R((\varphi(y,x)\to\varphi(y+1,x)) \to \varphi(n,x))).$$ $\endgroup$ Commented Mar 1, 2021 at 16:25
-
2$\begingroup$ Of course, it takes some work to show that this definition works! As I said in my previous comment, you can read a complete proof in the book by Jensen and Lenzing. $\endgroup$ Commented Mar 1, 2021 at 16:27
Edit: As Emil Jeřábek has pointed out in the comments, there is an error in the paper linked below, and the example does not work. I'll leave the answer here to document the error and add to the interesting list of attempted answers gathered here. An erratum has now appeared: Corrigendum to "[..]" RML, referencing this discussion.
Let me add that Dmytro Taranovsky has given a correct example, but I would still be very interested to see a "forcing-free" and especially an "algebraically natural" example of a $\emptyset$-definably complete ordered field which is not definably complete.
This question was answered negatively by Mojtaba Moniri in his recent paper On definable completeness for ordered fields, Reports on Mathematical Logic, Number 54 (2019), pp. 95-100.
An explicit example is given: $\mathbb{R}((t^\Gamma))$, where $\Gamma$ is the ordered additive group of dyadic rationals. Here $\mathbb{R}((t^\Gamma))$ is the Hahn series field over $\mathbb{R}$ with value group $\Gamma$: its elements are formal sums $\sum_{e\in \Gamma}c_et^e$ with $c_e\in \mathbb{R}$ such that the support $\{e\in \Gamma\mid c_e\neq 0\}$ is well-ordered. This field is complete for cuts definable without parameters, but not real closed: $t$ has no cube root.
-
3$\begingroup$ I’m confused. Aren’t Hahn series fields complete (even spherically complete)? This implies that a Hahn series fields cannot be a counterexample. $\endgroup$ Commented Mar 1, 2021 at 6:50
-
3$\begingroup$ Specifically, if $\Gamma=\mathbb Z[\frac12]$, then in $\mathbb R((t^\Gamma))$, the parameter-free set $X=\{x>0:\forall y>0\,\exists z\,(xy<z^3<y)\}$ consists exactly of the positive infinitesimal elements, and as such it has no least upper bound. $\endgroup$ Commented Mar 1, 2021 at 7:23
-
2$\begingroup$ The culprit is Lemma 2.1 (attributed to personal communication by van den Dries), which is directly contradicted by the definability of $X$ above. The problem with the proof is that $\Gamma'$ is not regularly dense, hence the Robinson–Zakon criterion does not apply; indeed, $\Gamma'$ is not elementarily equivalent to $\Gamma$, as $\exists x>0\,\forall y\,(0<y<x\to\exists z\,y=3z)$ holds in $\Gamma'$, but not in $\Gamma$. $\endgroup$ Commented Mar 1, 2021 at 12:08
-
2$\begingroup$ I meant Scott complete (or equivalently, complete as valued fields). See my answer below for a general argument that a counterexample cannot be complete, or even just henselian. $\endgroup$ Commented Mar 1, 2021 at 14:36
-
2$\begingroup$ @NoahSchweber Not that I know of. I sent a message to Moniri about it (with a CC to van den Dries, from whom I already got a short reply explaining that his involvement in the whole matter was quite minimal—he just gave the author some suggestions what to try). $\endgroup$ Commented Mar 1, 2021 at 22:20
This is a non-answer too long for a comment.
If $K$ is an ordered field that satisfies the least upper bound property for sets definable without parameters, then suprema of sets definable with parameters can be arbitrarily closely approximated in $K$.
Consequently, the completion of $K$ is a real-closed field (and $K$ itself is a real-closed field if it happens to be henselian).
To see this, let $X=\{x:K\models\phi(x,\vec a)\}$ be a nonempty bounded set. Applying an affine transformation if necessary, we may assume $0\in X\subseteq(-\infty,1)$. Let $\psi(w)$ denote the formula $$\begin{multline*} e>0\land\forall\vec u\:\bigl[\phi(0,\vec u)\land\forall x\:(\phi(x,\vec u)\to x<1)\\\to\exists z\:\bigl(\phi(z,\vec u)\land\forall x\:(\phi(x,\vec u)\to x<z+e)\bigr)\bigr]. \end{multline*}$$ In words, $\psi(e)$ says that for every set of the form $Y=\{x:K\models\phi(x,\vec u)\}$ for some $\vec u\in K$, if $0\in Y\subseteq(-\infty,1)$, then $\sup Y$ can be approximated within distance $e$, in the sense that there exists $z\in Y$ such that $Y\subseteq(-\infty,z+e)$.
Now, $E=\{e:K\models\psi(e)\}$ is definable without parameters, and clearly $1\in E\subseteq(0,+\infty)$, hence by assumption (or rather, by the equivalent greatest lower bound property), there exists $e_0=\inf E\ge0$.
If $e_0=0$, we are done. However, $e_0>0$ is impossible, because $$e\in E\implies e/2\in E.$$ Indeed, using the notation above, if $z\in Y\subseteq(-\infty,z+e)$, then either $z\in Y\subseteq(-\infty,z+e/2)$, or there exists $z'\ge z+e/2$ such that $z'\in Y\subseteq(-\infty,z'+e/2]$.
In my hasty first reading I did not notice the stipulation about parameter-freeness; I am leaving this answer "only for the record".
The answer to the question is in the positive, provided "real ordered field" is interpreted as "real closed field", and parameters are allowed. The details are worked out in a section 3 of a paper by Salehi and Zarza (a preprint of which can be found here); the paper was published as follows:
S. Salehi & M. Zarza, First-Order Continuous Induction and a Logical Study of Real Closed Fields, Bulletin of the Iranian Mathematical Society volume 46, pages225–243(2020).
-
$\begingroup$ Are you referring to Rmk 4.9, which says that their theory D-Sup implies RCF? I think D-Sup is a different theory than the one the OP is talking about on two counts. First, there is no restriction to $\emptyset$-definable sets in the least uppber bound axioms of D-Sup. Second, what their scheme does is, for each formula $\phi$, it adds an axiom which says, internal to the theory, that if the extent of $\phi$ is bounded then the extent of $\phi$ has a least upper bound. $\endgroup$ Commented Feb 6, 2021 at 4:04
-
$\begingroup$ But the OP's theory is restricted to $\phi$ without parameters, and (if I understand it correctly) simply asserts, for each such $\phi$ whose extent in $\mathbb R$ is bounded, that the extent of $\phi$ has a least upper bound. $\endgroup$ Commented Feb 6, 2021 at 4:04
-
$\begingroup$ It's possible that I don't understand their conventions for notating free variables, and in fact there is a $\emptyset$-definability restriction there. It's also possible that I don't understand the OP's theory, though I 'm pretty certain at least that the OP intends a "parameter-free" restriction. $\endgroup$ Commented Feb 6, 2021 at 4:09
-
4$\begingroup$ Notation aside, the argument in the paper is just the standard proof (originally due to Tarski, I believe) that the existence of suprema for sets definable with parameters implies RCF, which is also given by Asaf Karagila’s answer to the OP’s math.SE question math.stackexchange.com/questions/1531177/…. There is nothing in the argument to justify that it should work in the absence of parameters. $\endgroup$ Commented Feb 6, 2021 at 8:51
-
1$\begingroup$ @TimCampion Apart from the issue of parameters, the formulation of the D-Sup schema in the paper is the correct one. Your reading of the least upper bound property trivially implies RCF: given any sentence $\psi$ that holds in $\mathbb R$, define $\phi(x)$ as $x=0\lor(x>0\land\neg\psi)$. Then $\{x:\phi(x)\}$ is bounded in $\mathbb R$, hence your formulation of the axiom says that $\phi$ has a least upper bound, hence in particular, it has a bound. This implies $\psi$. $\endgroup$ Commented Feb 6, 2021 at 8:57
EDIT 2: This wrong proof at least shows that the upper bound property holds in $K(\pi)$, when $\phi$ is $\Sigma_1$. Indeed, if $\phi$ is $\Sigma_1$ then we have the inclusion of solution sets
$$ \phi(K) \subset \phi(K(\pi)) \subset \phi(\mathbb R). $$
Both $\phi(K)$ and $\phi(\mathbb{R})$ can be expressed in the same way as a finite union of points and intervals, so the supremum in $K$ is once again the supremum in $K(\pi)$.
EDIT: As Emil Jeřábek points out, this proof breaks by assuming the quantifier-free equivalence preserves the solution set in $K(\pi)$ as well.
Let $K$ denote the field of real algebraic numbers (real-closed, elementarily equivalent to $\mathbb{R}$). I may be missing something basic, but I think we can show that $K(\pi)$ is a counterexample to elementary equivalence in the following way:
First, note that $K$ satisfies the theory in question, since $\mathbb R$ does. Let $\phi(x)$ be a formula without parameters. Since $Th(K) = Th(\mathbb R) = RCF$ eliminates quantifiers, we can replace $\phi(x)$ with a quantifier-free formula whose solution set in $\mathbb{R}$ (and hence in all subfields) is the same. By model completeness of RCF the embedding $K \hookrightarrow \mathbb{R}$ is elementary, so we have
$$ \{x \in K: \phi(x) \} = \{x \in \mathbb{R}: \phi(x) \} \cap K. $$
The solution set of $\phi(x)$ in $\mathbb{R}$ is a finite union of points and intervals. Furthermore, all the points in this solution set are algebraic. If not, since rationals can separate the distinct points and intervals, and are definable without parameters, it follows that there is some formula $\psi$ without parameters whose unique solution in $\mathbb{R}$ is a transcendental number $s$. Additionally, $\psi$ is quantifier-free, since $\phi$ is. But this is clearly impossible.
Suppose that $\phi(x)$ defines a nonempty bounded subset of $K(\pi)$. Then $\phi(x)$ defines a bounded subset of $K$. Furthermore, the (nonempty) solution set of $\phi(x)$ in $\mathbb R$ consists of intervals and algebraic points, so its solution set in $K$ is nonempty as well. Since $K$ satisfies the theory, this means that $\phi(x)$ has a least upper bound $y$ in $K$. Furthermore, this $y$ must actually be the least upper bound of the set $\phi(x)$ defines in $\mathbb{R}$: By our argument above, the least upper bound is either an algebraic point, or the upper bound of an interval in which elements of $K$ are dense.
Therefore, there is some $y \in K$ which is the least upper bound of the set defined by $\phi(x)$, both in $K$ and in $\mathbb R$. But it follows that $y$ is also the least upper bound of the set defined by $\phi(x)$ in $K(\pi)$. This shows that $K(\pi)$, which is not real-closed, must satisfy this theory as well.
-
1$\begingroup$ $K$ has quantifier elimination, but $K(\pi)$ has not. You are supposed to show the least upper bound property for sets of the form $\{x\in K(\pi):K(\pi)\models\phi(x)\}$ where $\phi$ is an arbitrary formula, and this cannot be reduced to the case of just quantifier-free $\phi$. For example, the set defined by the formula $\phi(x)=\exists y\,x=y^2$ is dense in $K(\pi)_{\ge0}$ with a dense complement, hence it certainly is not a finite union of intervals. $\endgroup$ Commented Feb 10, 2021 at 20:59
-
$\begingroup$ Right, but I don't believe that my proof uses quantifier elimination / o-minimality for $K(\pi)$ (again, I'm probably missing something). It's true that the set you identify isn't a finite union of intervals in $K(\pi)$, but it is in $\mathbb{R}$ which I think is all I use. $\endgroup$ Commented Feb 10, 2021 at 21:25
-
$\begingroup$ Nevermind, I see the issue. My apologies $\endgroup$ Commented Feb 10, 2021 at 21:27
-
$\begingroup$ @SpencerDembner So, does this settle the issue? You answered the question with a correct argument? $\endgroup$ Commented Feb 10, 2021 at 21:50
-
1$\begingroup$ @user107952 no, unfortunately the argument doesn't work because of the issue Emil brought up. $\endgroup$ Commented Feb 10, 2021 at 21:51