one-sided real number

There are really two notions of one-sided real number: lower reals and upper reals. But there is a nearly perfect symmetry between them (although the lower reals seem to get slightly more use).

These are largely concepts in constructive mathematics. Using excluded middle, a bounded one-sided real number is simply a real number, but constructively they are more general (and less well behaved). Lower reals are particularly important in constructive measure theory as the values taken by positive measures (and more generally are used to define extended positive cones).

However, even in classical mathematics, there are some differences, at least in emphasis and application. First, it is most natural to include $\infty$ as a lower real and include $-\infty$ as an upper real. (However, you can restrict to *bounded* lower/upper reals to avoid that, or alternatively genralise to *extended* lower/upper reals if you want to include both $\pm\infty$ at once.) Also, the natural topology on the lower reals is the *lower semicontinuous topology* (and the natural topology on the upper reals is the *upper semicontinuous topology*).

One-sided numbers are sometimes called (upper or lower) *semicontinuous* numbers. To see why, consider a locale (or topological space) $L$, and consider the (upper or lower) semicontinuous functions (real-valued) on $L$. On the one hand, these are the same as the continuous functions from $L$ to (classically) the set of real numbers equipped with the semicontinuous topology or to (constructively) a locale whose points are the one-sided real numbers. On the other hand, these semicontinuous functions are precisely the internal one-sided real numbers in the topos of sheaves over $L$.

Lower and upper reals don't interact well together; for a system that naturally includes both (and, constructively, much more), use the MacNeille real numbers.

(In the following, ‘number’ without qualification may be taken to mean either a real number or a rational number; the result is the same either way. Indeed, we could take any dense set of real numbers.)

A **lower real number** is the supremum of an inhabited set of numbers. A **bounded lower real** is the supremum of an inhabited set of numbers that has a finite upper bound. An **extended lower real** is the supremum of an arbitrary set of numbers.

An **upper real number** is the infimum of an inhabited set of numbers. A **bounded upper real** is the infimum of an inhabited set of numbers that has a finite lower bound. An **extended lower real** is the infimum of an arbitrary set of numbers.

We cannot generalize further by taking more extrema of the same sort. Explicitly, the supremum of any inhabited set of lower reals is a lower real and the infimum of any inhabited set of upper reals is an upper real. (Similar results obtain if we use either bounded or extended reals, so long as we also either require the set to bounded or allow it to be empty.) However, mixing extrema takes us further to the MacNeille real numbers.

There are some choices as to how exactly to represent one-sided real numbers; we will define them here as certain subsets of the set $\mathbb{Q}$ of rational numbers. If we replaced $\mathbb{Q}$ with any other dense subset of the real line, then the definitions would end up being equivalent.

An **extended lower real number** is any subset $L$ of $\mathbb{Q}$ such that

- if $a \in L$, then $a \lt b$ for some $b \in L$; and
- if $a \lt b$ and $b \in L$, then $a \in L$.

We can actually combine these into a single rule:

- $a \in L$ if and only if $a \lt b$ for some $b \in L$.

A **lower real number** is an extended lower real $L$ such that:

- some $a \in L$.

A **bounded lower real number** is a lower real $L$ such that

- some $b \notin L$.

When treated explicitly as a subset of $\mathbb{Q}$, we call $L$ a **lower set**. When we interpret $L$ as a one-sided real number $x$, we write $a \lt x$ to mean that $a \in L$. Conversely, we can interpret any rational number, or even any real number, $x$ as a bounded lower real, specifically as the set of all rational numbers less than $x$. (A bounded lower real is **located** if it is the lower real obtained in this way from a real number; classically, every bounded lower real number is located.) We interpret $\infty$ as the lower real whose lower set is all of $\mathbb{Q}$; we interpret $-\infty$ as the extended lower real whose lower set is empty.

An **extended upper real number** is any subset $U$ of $\mathbb{Q}$ such that

- if $b \in U$, then $a \lt b$ for some $a \in U$; and
- if $a \lt b$ and $a \in U$, then $b \in U$.

We can actually combine these into a single rule:

- $b \in U$ if and only if $a \lt b$ for some $a \in U$.

An **upper real number** is an extended upper real $U$ such that:

- some $b \in U$.

A **bounded upper real number** is an upper real $U$ such that

- some $a \notin U$.

When treated explicitly as a subset of $\mathbb{Q}$, we call $U$ an **upper set**. When we interpret $U$ as a one-sided real number $x$, we write $x \lt b$ to mean that $b \in U$. Conversely, we can interpret any rational number, or even any real number, $x$ as a bounded upper real, specifically as the set of all rational numbers greater than $x$. (A bounded upper real is **located** if it is the upper real obtained in this way from a real number; classically, every bounded upper real number is located.) We interpret $-\infty$ as the upper real whose upper set is all of $\mathbb{Q}$; we interpret $\infty$ as the extended upper real whose upper set is empty.

We define order relations between extended lower reals $x$ and $y$ as follows:

- $x \lt y$ if and only if there exists a rational number $a$ such that $a \lt y$ but not $a \lt x$;
- $x \leq y$ if and only if $a \lt y$ for every rational number $a$ such that $a \lt x$.

In other words, $\leq$ is $\subseteq$ on lower sets, and $\lt$ is $\subsetneq$ (in an appropriate sense).

We define order relations between extended upper reals $x$ and $y$ as follows:

- $x \lt y$ if and only if there exists a rational number $b$ such that $x \lt b$ but not $y \lt b$;
- $x \leq y$ if and only if $x \lt b$ for every rational number $b$ such that $y \lt b$.

In other words, $\leq$ is $\supseteq$ on upper sets, and $\lt$ is $\supsetneq$.

We now have multiple meanings for $x \lt y$ or $x \leq y$ if one or both of these is already a rational number or a real number, but it is a theorem that the meanings are all consistent. We also have $-\infty \leq x \leq \infty$ for every extended number $x$, and $-\infty \lt x \lt \infty$ for every bounded number $x$. Finally, $x \leq y$ if $x \lt y$ or $x = y$; the converse holds classically.

Each version of $\leq$ is a partial order and each version of $\lt$ is a quasiorder. By excluded middle, $\leq$ is a total order and $\lt$ is the corresponding linear order, but neither of these results holds constructively. In particular, the comparison law for $\lt$ is invalid, which is why one-sided reals are not as well behaved as ordinary (located) real numbers.

Given any collection of extended lower reals, their **supremum** is an extended lower real which is found by taking the union of lower sets. The supremum of an inhabited set of lower reals is a lower real, and the supremum of an inhabited set of bounded lower reals is bounded iff the set has a bounded lower real as an upper bound. In any case, this supremum really is the supremum under $\leq$. This agrees with the notion of supremum of real numbers in the real number system, when that exists. Every extended lower real is also the supremum in this sense of its corresponding lower set, interpreted as a set of lower reals that happen to all be rational numbers.

Given any collection of extended upper reals, their **infimum** is an extended upper real which is found by taking the union of upper sets. The infimum of an inhabited set of upper reals is an upper real, and the infimum of an inhabited set of bounded upper reals is bounded iff the set has a bounded upper real as a lower bound. In any case, this infimum really is the infimum under $\leq$. This agrees with the notion of infimum of real numbers in the real number system, when that exists. Every extended upper real is also the infimum in this sense of its corresponding upper set, interpreted as a set of upper reals that happen to all be rational numbers.

Constructively, we cannot necessarily take the infimum of a set of lower reals, nor the supremum of a set of upper reals. We can, however, interpret such a supremum or infimum as a MacNeille real number.

In general, you can extend order-preserving functions of rational numbers to lower reals and to upper reals; you simply take the image of the lower or upper set and close it downward or upwards, as appropriate. If you have an order-reversing function of rational numbers, then you can apply it to a lower real to get an upper real and conversely; this is about the only interaction that I know of between the two kinds of one-sided real.

Since addition is order-preserving, it works nicely, at least to make a monoid; but subtraction doesn't work in general. Multiplication has trouble with negative numbers but produces good results if you restrict to $[0,\infty]$. Notice that we get $0 \cdot \infty = 0$ with lower reals but $0 \cdot \infty = \infty$ with extended upper reals; thus, ${[{0,\infty}[}$ is a rig for either lower or upper reals, while $[0,\infty]$ is a rig only for lower reals. (This doesn't so much mean that upper reals behave worse than lower reals, as that extended reals on either side behave worse.) We can also use logarithms to translate between addition and multiplication. (In particular, $-\infty + \infty = -\infty$ with extended lower reals but $-\infty + \infty = \infty$ with extended upper reals.)

Of course, arithmetic with one-sided real numbers is much easier than this in classical mathematics, where the bounded or extended versions may be identified; but even there, the natural operations involving $\pm\infty$ may differ. Accordingly, the conventions for arithmetic with infinities can signal which sort of number is appropriate for a constructive development.

If you really want to do arbitrary arithmetic operations constructively on upper or lower reals, then again you need their common generalisation, the MacNeille reals.

Let's put this on a separate page: semicontinuous topology. For one thing, it's more advanced than the elementary stuff above; for another thing, it's more interesting in classical mathematics; and finally, it's more complicated in constructive mathematics. The main point is that each type of one-sided real number has its own natural topology, and these differ (both classically and constructively) from the usual topology on the real line.

There is a bijective correspondence of internal extended lower real numbers in a sheaf topos $\mathrm{Sh}(X)$ of a topological space $X$ and lower semicontinuous functions $X \to \mathbb{R} \cup \{ +\infty \}$, or equivalently a continuous function $X \to \mathbb{R} \cup \{ +\infty \}$, when the latter is equipped with the lower semicontinuous topology. (We will work classically in the external logic.)

Let $\Delta(\mathbb{Q})$ denote the constant sheaf of rational numbers on $X$. A *lower real number* $U$ in $\mathrm{Sh}(X)$ is then defined as a subsheaf of $\Delta(\mathbb{Q})$ satisfying the axioms above (interpreted in the internal language). Such a lower real number induces a lower semicontinuous function $x \mapsto \sup U_x$, where $U_x$ denotes the stalk of $U$ at $x$ (taken as a subset of $\mathbb{Q}$).

Conversely, a lower semicontinuous function $f : X \to \mathbb{R} \cup \{ +\infty \}$ defines an internal lower real number $U$ with sections

$U(A) \coloneqq \{ \varphi : A \to \mathbb{Q} | \forall x \in A: \varphi(x) \lt f(x) \} \subseteq \Delta(\mathbb{Q})(A)$

over open sets $A \subseteq X$.

See Mulvey (1974, page 28) for details.

For the externally constructive version of this, it is best to take $X$ to be a locale; we need to use the (external) locale $L$ of lower real numbers in place of $\mathbb{R} \cup \{\infty\}$, and the notion of semicontinuous map is replaced with a continuous map (in the sense of locales) to $L$.

- C. Mulvey (1974):
*Intuitionistic Algebra and Representations of Rings*. In Hofmann, Liukkonen:*Recent Advances in the Representation Theory of Rings and C*-Algebras by Continuous Sections*, AMS 1974.

Revised on September 24, 2013 11:51:48
by Toby Bartels
(98.23.150.36)