This post originated from my reference request for the definition of an ordered field in constructive mathematics: Proper definition of ordered field in constructive mathematics

We are working in constructive mathematics. For the sake of this post, let us define a ordered field 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$. $K$ has a partial order $\leq$ defined by $a \leq b := \neg(b < a)$. An ordered field is a lattice field if additionally it contains a binary meet function $\min$ and join function $\max$ such that $(K, \leq, \min, \max)$ is a (unbounded) lattice. A nonlattice field is an ordered field where the partial order $\leq$ does not form a lattice.

In one of the comments of my reference request, Geoffrey Irving states

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.

Are there proofs of these two statements?


1 Answer 1


Given a constructive ordered field $K$, the field $K(t)$ of rational functions can be given the minimal order structure inherited from $K$ and $t > 0$. That is, two rational functions $f(t), g(t)$ have $f(t) < g(t)$ if that is derivable from order information on $K$ and $t > 0$. The resulting field is not a lattice even if $K$ is, as we cannot determine whether $1 < t$, and thus $\max(1,t)$ is not a known rational function of $t$.

In the reverse direction, let $K$ be a constructive ordered field that is not necessarily a lattice. Generate an ordered field $L$ as all expressions generated starting with $K$ from field operations and $\max$, with all $x < y$ statements generated by reducing to simpler expressions (we have to generate expressions and $x < y$ statements together to avoid divide by zero). E.g., we know $x < \max(y,z)$ if we know $x < y \lor x < z$, etc. Then $L$ is a constructive ordered field that is a lattice, and $K \subset L$.

  • $\begingroup$ Minor question, which I probably should have made it clear in the questions above, and in my original reference request, but are the constructive ordered fields here Heyting fields, with respect to the canonical tight apartness relation defined by $a \# b := a \lt b \vee b \lt a$? Other definition of fields do exist which are not Heyting, such as the residue fields from Peter Johnstone's Rings, Fields, and Spectra. $\endgroup$ Jul 5, 2022 at 20:10
  • $\begingroup$ The first construction certainly works for Heyting fields, as by assumption $t$ is transcendental. Thus, any nonconstant rational function is invertible, and if $K$ is Heyting then any nonzero is invertible. The second construction should also work for Heyting fields, but it's not quite as obvious. $\endgroup$ Jul 5, 2022 at 20:20
  • 2
    $\begingroup$ Could you be a bit more precise about the reverse direction, or provide a reference? What does it mean to "generate an ordered field"? How is the order playing a role in the generation? $\endgroup$ Jul 5, 2022 at 21:32
  • 2
    $\begingroup$ I agree with Andrej, but I also don't understand the first part. In $K(t)$ we know that $1 < 2$ and therefore we should also have $1 < t \lor t < 2$, no? $\endgroup$ Jul 5, 2022 at 22:08

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.