Mathematics and Computation

A blog about mathematics for computers

On complete ordered fields

Joel Hamkins advertised the following theorem on Twitter:

Theorem: All complete ordered fields are isomorphic.

The standard proof posted by Joel has two parts:

  1. A complete ordered field is archimedean.
  2. Using the fact that the rationals are dense in an archimedean field, we construct an isomorphism between any two complete ordered fields.

The second step is constructive, but the first one is proved using excluded middle, as follows. Suppose $F$ is a complete ordered field. If $b \in F$ is an upper bound for the natural numbers, construed as a subset of $F$, then so $b - 1$, but then no element of $F$ can be the least upper bound of $\mathbb{N}$. By excluded middle, above every $x \in F$ there is $n \in \mathbb{N}$.

So I asked myself and the constructive news mailing list what the constructive status of the theorem is. But something was amiss, as Fred Richman immediately asked me to provide an example of a complete ordered field. Why would he do that, don't we have the MacNeille reals? After agreeing on definitions, Toby Bartels gave the answer, which I am taking the liberty to adapt a bit and present here. I am probably just reinventing the wheel, so if someone knows an original reference, please provide it in the comments.

The theorem holds constructively, but for a bizarre reason: if there exists a complete ordered field, then the law of excluded middle holds, and the standard proof is valid!

As there are many constructive versions of order and completeness, let me spell out the definitions that are well adapted to the oddities of constructive mathematics. In classical logic these are all equivalent to the usual ones. Having to disentangle definitions when passing to constructive mathematics is a bit like learning how to be careful when passing from commutative to non-commutative algebra.

A partial order $\leq$ on a set $P$ is a reflexive, transitive and antisymmetric relation on $P$.

We are interested in linearly ordered fields, but constructively we need to take care, as the usual linearity, $x \leq y \lor y \leq x$, is quite difficult to satisfy, and may fail for reals.

A strict order on a set $P$ is a relation $<$ which is:

The associated partial order is defined by $x \leq y \Leftrightarrow \lnot (y < x)$. The reflexivity, antisymmetry and transitivity of $\leq$ follow respectively from irreflexivity, tightness, and weak linearity of $<$.

Next, an element $x \in P$ is an upper bound for $S \subseteq P$ when $y \leq x$ for all $y \in P$. An element $x \in P$ is the supremum of $S \subseteq P$ if it is an upper bound for $S$, and for every $y < x$ there exists $z \in S$ such that $y < z$. A poset $P$ is (Dedekind-MacNeille) complete when every inhabited bounded subset has a supremum (for the classically trained, $S \subseteq P$ is inhabited when there exists $x \in S$, and this is not the same as $S \neq \emptyset$).

A basic exercise is to give a non-trivial complete order, i.e., a strict order $<$ whose associated partial order $\leq$ is complete.

Theorem: If there exists a non-trivial complete order then excluded middle holds.

Proof. Suppose $<$ is a strict order on a set $P$ whose associated order $\leq$ is complete, and there exist $a, b \in P$ such that $a < b$. Let $\phi$ be any proposition. Consider the set $S = \lbrace x \in P \mid x = a \lor (\phi \land x = b)\rbrace$. Observe that $\phi$ is equivalent to $b \in S$. Because $a \in S \subseteq \lbrace a, b\rbrace$, the set $S$ is inhabited and bounded, so let $s$ be its supremum. We know that $a < s$ or $s < b$, from which we can decide $\phi$:

  1. If $a < s$ then $b \in S$: indeed, there exists $c \in S$ such that $a < c$, but then $c = b$. In this case $\phi$ holds.
  2. If $s < b$ then $\lnot(b \in S)$: if we had $b \in S$ then $S = \lbrace a, b \rbrace$ and $b = s < b$, which is impossible. In this case $\lnot\phi$. $\Box$

This immediately gives us the desired theorem.

Theorem (constructive): All complete ordered fields are isomorphic.

Proof. The definition of a complete ordered field requires $0 < 1$, therefore excluded middle holds. Now proceed with the usual classical proof. $\Box$

This is very odd, as I always thought that the MacNeille reals form a MacNeille complete ordered field. Recall that a MacNeille real is a pair $(L, U)$ of subsets of $\mathbb{Q}$ such that:

  1. $U$ is the set of upper bounds of $L$: $u \in U$ if, and only if, $\ell \leq u$ for all $\ell \in L$,
  2. $L$ is the set of lower bounds of $U$: $\ell \in L$ if, and only if, $\ell \leq u$ for all $u \in U$,
  3. $L$ and $U$ are inhabited.

Furthermore, the MacNeille reals are complete, as they are just the MacNeille completion of the rationals. We may define a strict order on them by stipulating that, for $x = (L_x, U_x)$ and $y = (L_y, U_y)$, $$x < y \iff \exists q \in U_x . \exists r \in L_y \,.\, q < r.$$ According to Peter Johnstone (Sketches of an Elephant, D4.7), the MacNeille reals form a commutative unital ring in which $x$ is invertible if, and only if, $x < 0 \lor x > 0$. So apparently, the weak linearity of the strict order is problematic.

What if we relax completeness? Two standard notions of completeness are:

  1. An ordered field $F$ is Cauchy-complete if every Cauchy sequence has a limit in $F$.
  2. An ordered field $F$ is Dedekind-complete if every Dedekind cut determines an element of $F$.

It is easy enough to find non-isomorphic Cauchy-complete fields. Order the field $\mathbb{Q}(x)$ of rational functions with rational coefficients by stipulating that it extends the order of $\mathbb{Q}$ and that $q < x$ for all $q \in \mathbb{Q}$. The Cauchy-completion of $\mathbb{Q}(x)$ is a Cauchy complete field which is not isomorphic to $\mathbb{Q}$. Caveat: I am speaking off the top of my head, do not trust this paragraph! (Or any other for that matter.)

Regarding Dedekind completeness, it is important constructively that we take two-sided Dedekind cuts, i.e., pairs $(L, U)$ of subsets of $F$ such that

Dedekind completeness states that for every Dedekind cut $(L, U)$ in $F$ there exists a unique $x \in F$ such that $L = \lbrace y \in F \mid y < x\rbrace$ and $U = \lbrace y \in F \mid x < y\rbrace$. Constructively this is a weaker form of completeness than the Dedekind-MacNeille one, but classically they coincide. Thus we cannot hope to exhibit constructively two non-isomorphic Dedekind-complete ordered fields (because constructive results are also classically valid). But perhaps there is a model of constructive mathematics where such strange fields exist. Does anyone know of one?


Mike Shulman

(In case 1 of your first theorem, $\neg\neg\phi$ should be $\phi$.)

Weak linearity (a.k.a. cotransitivity or comparison) is essentially a version of the "locatedness" that distinguishes the Dedekind reals from the MacNeille reals, so it's not surprising that if you require your "complete ordered fields" to satisfy it then you exclude the MacNeille reals. Instead of weakening completeness, you could weaken this condition, e.g. by assuming that $\le$ and $<$ are both transitive and $<$ is a "bimodule" over $\le$; see e.g. and section 8 of

(At the moment I'm failing to see where Toby's alternative argument for WLEM involving the algebraic structure fails for the MacNeille reals. Can you help me out?)


When constructivists say that a proof is constructive, what logical system(s) do they mean that it can be formalized in?

(Fixed the typo, thanks.)

To come to the bottom of this, I need to take some time to read the Elephant, section D4.7, and just carefully work out the properties of MacNeille reals.

Toby's WLEM argument works as soon as we assume that we have a strict complete order $<$ with $a < b$, no algebraic structure is necessary. It is easy to adapt the argument I gave to the usual definition of suprema. So the MacNeille reals must fail to give a strict order. In fact, how do you get weak linearity (cotransitivity) for MacNeille reals? That seems hard.

@Andrei: From what I know of constructivists, there are two possibilities. Some use Bishop-style informal constructive mathematics, which more or less corresponds to intuitionistic logic with dependent choice (but a somewhat peculiar treatment of equality on serts). Others use just some variant of intuitionistic logic or set theory without choice. There are very few who use a version of Brouwerian intuitionism.

In this particular case, what I said can be interpreted in intuitionistic set theory (IZF) or the internal language of a topos (higher-order logic with natural numbers).

Mike Shulman

Yes, certainly cotransitivity fails for the MacNeille reals; that's what distinguishes them from the Dedekind reals. But I didn't see where Toby's original argument (as opposed to your improved version) used cotransitivity.

Regarding the question in your final paragraph, what about something like taking the usual constructive definition of the Dedekind reals and weakening the inhabitedness of $L$ and $U$ to nonemptiness? I think that should give a Dedekind-complete order that is not provably Archimedean in your strong sense (and probably fails to be so in some model), but I haven't checked that the algebraic operations work on it.

Mike Shulman

(Hmm, I thought I posted this a few days ago, but it doesn't seem to have appeared even as a PR.)

Yes, of course the MacNeille reals don't satisfy cotransitivity; that's exactly what distinguishes them from the Dedekind reals. But I didn't see where Toby's argument uses cotransitivity. Maybe I didn't look hard enough?

Regarding the question in the last paragraph of your post, the first idea that comes to my mind would be relaxing the usual constructive definition of the Dedekind reals by weakening the requirement that $L$ and $R$ be inhabited to ask only that they be nonempty. It seems to me there's a chance that would yield a Dedekind-complete not-provably-Archimedean strict order, and maybe the algebraic operations would extend to it too.

As far as I can tell, Toby's argument requires cotransitivity of $<$, above I explicitly noted this in the proof which gets you excluded middle from a complete order: the supremum $s$ of the set $S$ is either above $a$ or below $b$.

The idea to have $\lnot\lnot$-bounded Dedekind cuts is good! Let's see, in $Sh(X)$ for a reasonable $X$ the Dedekind cuts are the sheaf of real-valued continuous maps. The unbounded cuts correspond to maps into $[-\infty,\infty]$. The $\lnot\lnot$-bounded ones would be the maps into $[-\infty, \infty]$ which take on values $-\infty$ and $\infty$ on a set with empty interior? Indeed, those will fail to be locally bounded (which is what the archimedean axiom amounts to).

But wait, such a sheaf does not form a ring in the topos. Hmmm.


Hi Andrej. Am I right to say that according to the content of your post, if LEM ≔ {(A ∨ ¬A)|A ∈ WFF(LOST)}, then IZF ∪ LEM ⊢ {“∃ a complete ordered field”} and IZF ∪ {“∃ a complete ordered field”} ⊢ LEM?

Remark: LOST ≔ Language of Set Theory.

@Berrick: Yes, I think so, except that it would be better to phrase LEM as a single sentence, rather than a schema. For instance, you could take it to be $\forall x . (\emptyset \in x \lor \emptyset \not\in x)$.

Hi Andrej. You and I wrote a paper about the Dedekind reals. See in particular Remark 12.13.

This suggests replacing general subsets with RE ones in the definition of Dedekind completeness and a Conway-like construction. (Maybe these could then be the "general" subsets in a realisability topos.)

@PaulTaylor: Paul, of course I remember the paper! And I am sure you could tell I was relying on things that are in that paper. I think of this blog post as essentially stating that MacNeillec-completeness is unreasonably strong from a constructive point of view, and that we should replace it with Dedekind completeness.

Regarding your idea: since the Dedekind reals are a Dedekind-complete archimedean field, if there's another Dedekind-complete field, it has to be non-archimedean, so I think your suggestion is going in the right direction. In the effective topos the Dedekind cuts will indeed be RE-like (thanks to countable choice).

Post a comment:
Write your comment using Markdown. Use $⋯$ for inline and $$⋯$$ for display LaTeX formulas, and <pre>⋯</pre> for display code. Your E-mail address is only used to compute your Gravatar and is not stored anywhere. Comments are moderated through pull requests.