4
$\begingroup$

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?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
-1
$\begingroup$

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$.

Improve this answer
$\endgroup$
4
  • $\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$
    – Madeleine Birchfield
    Commented 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$
    – Geoffrey Irving
    Commented 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$
    – Andrej Bauer
    Commented 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$
    – François G. Dorais
    Commented Jul 5, 2022 at 22:08

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .