nLab admissible Archimedean ordered field

Idea

In constructive mathematics, not every proposition is a boolean, which means that there is a hierarchy of sublattices $\Sigma$ of the frame of truth values $\Omega$ in which the pseudo-order relation of an Archimedean ordered field might take values in.

Definition

Given a sublattice of the frame of truth values $\Sigma \subseteq \Omega$, an Archimedean ordered field $F$ is $\Sigma$-admissible if and only if there is a function $(-) \lt_\Sigma (-):F \times F \to \Sigma$ such that $(x \lt_\Sigma y) = \top$ if and only if $x \lt y$.

Examples

• Every discrete Archimedean ordered field is admissible for the set of booleans $\mathbb{2}$.

• The Cauchy real numbers is admissible for the set of semi-decidable propositions $\Sigma_0^1$, and is in fact the terminal Archimedean ordered field which is admissible for $\Sigma_0^1$.

• Given a $\sigma$-frame of propositions $\Sigma$, the ordered field $\mathbb{R}_\Sigma$ of two-sided Dedekind real numbers constructed out of the Dedekind cuts valued in $\Sigma$ is $\Sigma$-admissible, and is in fact terminal Archimedean ordered field which is admissible for $\Sigma$.

• Assuming the limited principle of omniscience, the Cauchy real numbers, HoTT book real numbers, and the lower, upper, and two-sided $\mathbb{2}$-Dedekind real numbers are all $\mathbb{2}$-admissible Archimedean ordered fields.

 Related concepts

• sigma-frame of propositions

• Archimedean ordered field

 References

Archimedean ordered fields admissible for a $\sigma$-frame $\Sigma$ are defined in section 11.2.3 of:

• Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)