## Idea ## Dedekind completeness but without the located requirement, resulting in an Archimedean ordered field that behaves like the arithmetic of [[closed interval]]s on the [[rational numbers]]. ## Defintion ## An [[Archimedean ordered field]] $F$ is **interval-complete** if * For all terms $a:F$, the [[lower bounded open interval]] $(a,\infty)$ is inhabited. $$\alpha:\prod_{a:F} \left[(a, \infty)\right]$$ * For all terms $a:F$, the [[upper bounded open interval]] $(-\infty,a)$ is inhabited. $$\beta:\prod_{a:F} \left[(-\infty, a)\right]$$ * For all terms $a:F$ and $b:F$, $a \lt b$ if and only if $(b,\infty)$ is a subinterval of $(a,\infty)$ $$\gamma:\prod_{a:F} \prod_{b:F} (a \lt b) \cong ((b,\infty) \subseteq (a,\infty)$$ (for all propositions $A$ and $B$, $p:(A \cong B) \cong ((A \to B) \times (B \to A))$) * For all terms $a:F$ and $b:F$, $b \lt a$ if and only if $(-\infty,b)$ is a subinterval of $(-\infty,a)$ $$\delta:\prod_{a:F} \prod_{b:F} (b \lt a) \cong ((-\infty,b) \subseteq (-\infty,a)$$ * For all terms $a:F$ and $b:F$, the intersection of $(a,\infty)$ and $(-\infty,b)$ is a subinterval of the [[open interval]] $(a,b)$ $$\eta:\prod_{a:F} \prod_{b:F} ((a, \infty) \cap (-\infty, b)) \subseteq (a, b)$$ ## See also ## * [[Archimedean ordered field]] * [[Dedekind real closed intervals]] * [[locator]] * [[closed interval]]