There are actually two different ways to define an ordered field in constructive mathematics, depending on whether the apartness relation of an ordered local ring is tight or logically equivalent to negation of equality. The former is commonly used in real analysis with the Dedekind real numbers, while the latter is used in synthetic differential geometry.

]]>non-Archimedean Heyting ordered fields do not necessarily have an absolute value function. See for instance the real.numbers used in smooth infinitesimal analysis, as well as the surreal numbers

]]>the nlab article on strict total order explicitly states that the MacNeille real numbers do not form a strict total order, and are thus by definition not an ordered field.

Anonymous

]]>François G. Dorais proved here that any Cauchy complete Archimedean ordered field without a lattice structure has a lattice structure, so the extra axioms for the lattice structure in the HoTT book are unnecessary.

The Cauchy real numbers can be constructively proven to satisfy the fundamental theorem of algebra, so one could define the lattice structure on the Cauchy reals from the absolute value, from the square root function, from the FTA.

I think that just about wraps up all the important ordered fields which have a lattice structure.

]]>Adding the references named on the nForum

]]>going ahead and adding material about ordered fields in constructive mathematics as discussed in the nForum

]]>What is probably better for this article is to keep the original definition that Toby Bartels gave for the definition of an ordered field in classical mathematics, and then create a section on constructive notions of ordered fields, similar to what was done in the field article on the nLab.

It will either be the case that the constructive definition is much more complicated than the classical definition (assuming that every definition found in the literature is equivalent to the definitions in the HoTT Book and the thesis), or there will be at least two inequivalent definition of an ordered field in constructive mathematics. Both cases would need significant amounts of text explaining why the classical definition is insufficient and why the extra structure is needed, and additionally in the second case, how the definitions relate to each other.

]]>I just realised that there is another aspect of the definitions in my given sources that isn’t included in the definition of the article: They also define an ordered field to be a Heyting field, with respect to the canonical tight apartness relation defined by $a \# b \coloneqq a \lt b \vee b \lt a$.

]]>I have sent an email to Toby Bartels regarding his 2010 definition of an ordered field, but Toby Bartels have a weird email system so hopefully I didn’t do anything incorrectly and the email successfully gets through to them.

]]>The MathOverflow user Geoffrey Irving has this to say about ordered fields with and without lattice structure:

one can convert back and forth between definitions with and without lattice structure. Given a lattice field, one can adjoin a positive transcendental with no other information to get a nonlattice field. And given a nonlattice field, there is a constructive lattice closure that extends it as a constructive field.

However it was in a comment, and Geoffrey Irving did not provide any proof of his statement, so I’ve opened up another MathOverflow question asking for a proof of Geoffrey Irving’s statement here.

]]>It looks to me that if a statement is evidently a short informal side remark (not much more than a dozen parenthetical words in rev 1) and given that you have references and expertise already all pointing to it needing improvement, it’s unclear how going to a large public forum with “the nLab claims this statement” serves a purpose? If you are genuinely uncertain then send an email to Toby Bartels – otherwise please just fix it (cf. #6). Thanks!

]]>I’ve started a reference request on MathOverflow for the definition of ordered field here.

]]>Mike,

Are the surreal numbers even a commutative ring in constructive mathematics? The nlab article on the surreal numbers says the following:

The definition of $\geq$ for numbers as formulated by Conway leans heavily upon properties of negation, and in particular the classical principle of excluded middle. However, it can be made more constructive by defining $\lt$ separately from $\le$:

- A number $x$ consists of a set $L_x$ of numbers and a set $R_x$ of numbers, under the condition that every member of $L_x$ is $\lt$ every member of $R_x$.
- $x \leq y$ if $x' \lt y$ is true for any $x' \in L_x$, and $x \lt y'$ is true for any $y' \in R_y$.
- $x \lt y$ if there exists an $x'\in R_x$ such that $x'\le y$, or there exists a $y'\in L_y$ such that $x\le y'$.
- $x = y$ is defined to mean $x \le y$ and $y \le x$.
This approach works up to a point. However, it encounters a problem in proving that multiplication is well-defined, i.e. that it respects equality. We can prove that if $x\ge 0$ then $y\le z \Rightarrow x y \le x z$ and hence $y = z \Rightarrow x y = x z$, and that if $x\le 0$ then $y\le z \Rightarrow x y \ge x z$ and hence $y = z \Rightarrow x y = x z$; but without excluded middle we can’t say that every $x$ is either $\ge 0$ or $\le 0$, so how can we conclude that $y = z \Rightarrow x y = x z$? It is unknown whether there is a solution to this problem.

Section 11.6 of the HoTT book on surreal numbers never defines multiplication on the surreal numbers either.

]]>Re #1:

It seems safe to assume that the short note from ref 1 leaves room for improvement, certainly if it differs from established literature. Also, on the off-chance that there was a deeper claim meant to be implied by rev 1, the author can still come back and expand on it later. So I don’t think you should hold back if you see room to improve the entry and have the energy to do so.

(NB: In practice one cannot assume that a later edit of an entry is meant as an endorsement of all previous material that is kept.)

]]>complete -> Dedekimd complete.

To disambiguate from Cauchy complete, which is frequently used to refer to Cauchy sequences and is a weaker condition than Dedekind completeness

Anonymous

]]>fixed second definition to align with the first, the old second definition implies that the field is a Heyting, while depending on the definition of field in the first definition of ordered field, such as Peter Johnson’s residue fields, it is not necessarily true that the field is Heyting.

Anonymous

]]>Do the MacNeille real numbers have a pseudolattice structure in constructive mathematics?

Even if the MacNeille real numbers have a pseudolattice structure, with the weak order defined by $a \leq b \coloneqq \max(a, b) = b$, it is not necessarily true that $\neg (a \lt b) \iff \max(a, b) = a$ in the MacNeille real numbers.

Also note that the current definition does not specify how a field is defined, nor set any requirements of invertibility for positive elements, or any relationship to whatever weak order a field might have. Are fields defined as Heyting fields, or Peter Johnstone’s residue fields? Defining fields as Heyting fields would exclude the MacNeille real numbers from being an ordered field.

]]>Are the surreal numbers a pseudolattice, constructively? I don’t know, I haven’t thought about it at all.

]]>Auke Booij’s thesis Analysis in univalent type theory as well as the HoTT book explicitly defines an ordered field to have an lattice structure on the underlying commutative ring, which is different from the definition of an ordered field in the nlab article, where such a condition is missing. (by lattice I mean unbounded lattice, or what some people call pseudolattices)

However, there are no references in the current nlab article on ordered fields showing that an ordered field doesn’t have a lattice structure in constructive mathematics. The basic definition lacking a lattice structure was already written in 2010 in the first revision of the article by Toby Bartels, and the other editors of the article, Todd Trimble and a few anonymous editors from earlier this year, all accepted the basic definition provided by Toby Bartels, since it hasn’t been modified since the first revision. So if they are still around I would like them or somebody else to provide references from the mathematical literature justifying that ordered fields do not necessarily have a lattice structure, or prove that every ordered field as currently defined has a compatible lattice structure. Otherwise I’ll insert the lattice structure into the definition.

]]>