Archimedean ordered fields without maxima and minima in constructive mathematics

Question

In constructive mathematics, let us define an ordered (Heyting) field $F$ to be a commutative ring with a binary relation $<$ which is

1. irreflexive, where for all $x$, $\neg (x < x)$
2. asymmetric, where for all $x$ and $y$, $\neg ((x < y) \wedge (y < x))$
3. transitive, where for all $x$, $y$, and $z$, $x < y$ and $y < z$ implies that $x < z$
4. cotransitive, where for all $x$, $y$, and $z$, $x < y$ implies that $x < z$ or $z < y$
5. connected, where for all $x$ and $y$, $\neg ((x < y) \vee (y < x))$ implies that $x = y$

such that

1. $0 < 1$
2. for all $x$, $y$, and $z$ in $F$, if $z < x + y$, then $z < x$ or $z < y$
3. for all $x$ and $y$ in $F$, if $0 < x$ and $0 < y$, then $0 < x y$
4. for all $x$ in $F$, $x$ is invertible if and only if $0 < x$ or $x < 0$.

There is a partial order defined as $x \leq y$ if and only if $\neg (y < x)$, and a tight apartness relation defined as $x \; \# \; y$ if and only if $(x < y) \vee (y < x)$. This implies that ordered fields here have stable equality because one has $\neg \neg \neg (x \; \# \; y)$ implies that $\neg (x \; \# \; y)$ and thus that $\neg \neg (x = y)$ implies that $x = y$. Thus, this definition excludes what David Jaz Myers calls a "Kock field" in Orbifolds as microlinear types in synthetic differential cohesive homotopy type theory, since those local rings don't have stable equality.

The rational numbers are a subfield of every ordered field. An ordered field $F$ is Archimedean if it satisfies the Archimedean property, which we define to be that the rationals are dense in $F$: for all $x$ and $y$ in $F$ such that $x < y$, there exists a rational number $q$ such that $x < q < y$.

Defined as such, every Archimedean ordered field is a subfield of the Dedekind real numbers.

There are many examples of Archimedean ordered fields which have a minimum function (i.e. binary meets with respect to the partial order $\leq$) and a maximum function (i.e. binary joins with respect to $\leq$) on the ordered field. Examples of such Archimedean ordered fields include the rational numbers, the real algebraic numbers, the Cauchy real numbers, the Dedekind real numbers, and any Cauchy complete Archimedean ordered field (the absolute value function is the limit of the sequence of functions $f_n(x) = x \tanh(n x)$ and the maximum and minimum can be constructed from the absolute value, see here).

Is there an Archimedean ordered field which has neither a minimum functon nor a maximum function? Or is it provable that every Archimedean ordered field has a minimum function and maximum function?

Answer 1

In the topos of sheaves over $\mathbb{R}$ we can construct a sub-ordered field of the Dedekind reals that does not have meets and joins. We recall that we can explicitly describe the Dedekind reals in $\mathrm{Sh}(\mathbb{R})$ as the sheaf $R$ where $R(U)$ is the set of continuous functions $U \to \mathbb{R}$. We define $R'(U) \subseteq R(U)$ to be the set of differentiable functions. We need to check that $R'$ is a sheaf. However, we can show this directly since differentiability is a "local" property: if $(V_i)_{i \in I}$ is an open cover of $U$ then $f : U \to \mathbb{R}$ is differentiable iff its restriction to every $V_i$ is.

We make $R'$ an ordered field by restricting the ordering and field operations of $R$. In particular, note that differentiable functions are closed under addition and multiplication, include the constantly 0 and constantly 1 functions, and that if $f : U \to \mathbb{R}$ is such that $f(x) > 0$ for all $x \in U$, then $1 / f$ is differentiable.

Since $R'$ is a sub ordered field of $R$ it inherits several properties. In particular, it is Archimedean and connected.

However, $R'$ does not have meets and joins. E.g. the zero function and the identity function do not have a join. For any differentiable function $f$ such that $f(x) \geq 0$ and $f(x) \geq x$ there is another differentiable function $g$ with the same property but strictly smaller than $f$ on some inhabited open set.