6
$\begingroup$

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.

Improve this question
$\endgroup$
7
  • $\begingroup$ Presumably $\mathbb{R}$ should be an ordered field, and $\le$ isn’t necessarily a total order constructively on $\mathbb{R}$. $\endgroup$
    – Geoffrey Irving
    Jul 5, 2022 at 18:19
  • 5
    $\begingroup$ 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. $\endgroup$
    – Madeleine Birchfield
    Jul 5, 2022 at 18:20
  • 6
    $\begingroup$ 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. $\endgroup$
    – Madeleine Birchfield
    Jul 5, 2022 at 18:26
  • 1
    $\begingroup$ @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/… $\endgroup$
    – Urs Schreiber
    Jul 5, 2022 at 19:46
  • 1
    $\begingroup$ Answered (though the proofs are immediate). $\endgroup$
    – Geoffrey Irving
    Jul 5, 2022 at 19:55

1 Answer 1

Reset to default
5
$\begingroup$

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.

This is definitely not the strongest argument I've ever made but this does provide good evidence that there is no "proper definition of ordered field in constructive mathematics", or even a proper definition of ordered field in constructive analysis if "analysis" is understood in a broader sense that includes both real analysis and differential geometry.

Improve this answer
$\endgroup$
3
  • $\begingroup$ The models of real numbers used in smooth infinitesimal analysis contains nonzero nilpotent infinitesimals and so they don't form a field. $\endgroup$
    – Madeleine Birchfield
    Jul 7, 2022 at 21:35
  • $\begingroup$ @MadeleineBirchfield They are nonzero but they are not apart from zero. $\endgroup$
    – François G. Dorais
    Jul 7, 2022 at 21:35
  • $\begingroup$ (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.) $\endgroup$
    – François G. Dorais
    Jul 7, 2022 at 21:43

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.