# Proper definition of ordered field in constructive mathematics

The nLab article on ordered fields defines ordered fields to be a field $$K$$ with a strict linear order $$<$$ such that $$0 < 1$$ and for all elements $$a \in K$$ and $$b \in K$$, if $$a > 0$$ and $$b > 0$$ then $$a + b > 0$$ and $$a \cdot b > 0$$. The nLab article goes on to claim that this definition is also valid in constructive mathematics.

In classical mathematics, the relation $$\leq$$ defined as $$a \leq b := \neg (b < a)$$ could be proved to be a total order, and thus a lattice with binary meets $$\min$$ and joins $$\max$$. However, in constructive mathematics, $$\leq$$ cannot be proved to be a total order without excluded middle, although it still can be proved that $$\leq$$ is a partial order. As a result, it isn't provable that the field $$K$$ has lattice structure.

The nLab article does not provide any sources that ordered fields in constructive mathematics do not have a lattice structure $$(K, \leq, \min, \max)$$. On the other hand, I have found two sources in the constructive mathematics literature where the definition of ordered field explicitly has lattice structure:

• Univalent Foundations Project (2013), Homotopy Type Theory -- Univalent Foundations of Mathematics, section 11.2.1, pdf
• Auke B. Booij (2020), Analysis in univalent type theory (2020), section 4.1, pdf

Are there any references in the constructive mathematics literature which define ordered fields without the lattice structure?

Edit: The nLab article on ordered fields has been edited to say that in constructive mathematics there are multiple definitions of an ordered field. However, the original definition provided in the first paragraph remains unsourced.

• Presumably $\mathbb{R}$ should be an ordered field, and $\le$ isn’t necessarily a total order constructively on $\mathbb{R}$. Jul 5 at 18:19
• The issue isn't whether $\leq$ is a total order on the field $K$, but whether every pair of element of $K$ has a join and a meet, which is a weaker condition than $\leq$ being a total order. In the two sources above, the join is written as $\max$ and the meet is written as $\min$, even though $\leq$ is not a total order. Jul 5 at 18:20
• and in constructive mathematics, the join $\max$ and the meet $\min$ are well defined binary operations in the Cauchy real numbers and the Dedekind real numbers, but this follows not from the order structure on the Cauchy or Dedekind real numbers, but from the construction of the Cauchy and Dedekind real numbers in terms of Cauchy sequences of rational numbers and Dedekind cuts respectively. Jul 5 at 18:26
• @GeoffreyIrving just to alert you that the OP has a followup question to you, here: mathoverflow.net/q/426091/381 All this is prodded by nForum discussion here: nforum.ncatlab.org/discussion/14737/ordered-field/… Jul 5 at 19:46
• Answered (though the proofs are immediate). Jul 5 at 19:55

The word "constructive" has many variations. Some might even say that it's a moving target. This is not a one-size-fits-all situation, so I would contend that maybe the proper definition of ordered field changes from one context to context. This is not immediately clear since there are ubiquitous ordered fields like $$\mathbb Q$$, $$\mathbb R$$, and maybe more. The varieties of constructivism could conceivably be forced to agree on the basis of this common ground. This is not the case: here are two contexts which superficially appear to be closely connected but diverge on whether an ordered field should have a lattice structure or not.
The first context is constructive real analysis. Infinite sequences and their convergence are at the very heart of this topic. In this context, it is essential that $$\mathbb R$$ be Cauchy complete (at least in the weak sense that a Cauchy sequence with a modulus of convergence has a limit). In another answer, I argued that this ensures that $$\mathbb R$$ has a lattice structure. So, in this context, the lattice structure is quite natural and a practitioner might be tempted to disregard ordered fields without lattice structure as mere curiosities.
The second context is smooth infinitesimal analysis. This isn't what is normally meant by "constructivism" but the idea does have some constructive roots, albeit with perhaps stronger roots in nonstandard analysis. Also models of smooth infinitesimal analysis take the form of smooth toposes. [SIA is not really my cup of tea, perhaps someone with more intimate knowledge could provide a better defense or rebuttal(!) of SIA as a variety of constructivism.] Now, in any such model, $$\mathbb R$$ cannot have a lattice structure since that directly leads to functions that are not smooth, e.g. $$|x| = \max(x,-x)$$. Nevertheless, $$\mathbb R$$ has a reasonable ordered structure and a practitioner would like this to be an ordered field.
• (Some models have invertible infinitesimals but then $\mathbb R$ is also not archimedean. I think that is weird for other reasons. Models where infinitesimals are noninvertible seem to be more relevant.) Jul 7 at 21:43