nLab
MacNeille real number

MacNeille real numbers

Idea

The MacNeille real numbers are a version of real numbers defined by forming the MacNeille completion of the rational numbers, and then perhaps excluding the top and bottom element (±\pm\infty). In classical mathematics, this produces the ordinary real numbers (and if we include ±\pm\infty it produces the extended real numbers). However, in constructive mathematics, it yields something different (and less well behaved); it is not a constructive theorem that every bounded MacNeille number is located (hence a real number in the usual sense of constructive mathematics).

Definition

Let \mathbb{Q} be the poset of rational numbers with its usual Archimedean order?.

There are two obvious ways to define the MacNeille real numbers from \mathbb{Q}, one based on closed cuts (which matches the general theory of MacNeille completions) and one based on open cuts (which is compatible with other types of real numbers). Fortunately, they are equivalent.

Outside of these definitions themselves, we will adopt the open definition, since it relates better to other kinds of real numbers.

With closed sets

A pair (L,U)(L,U) of subsets of \mathbb{Q} is called a closed Dedekind–MacNeille cut in \mathbb{Q} if:

  • UU is the set of upper bounds of LL: that is, sUs \in U iff for all rLr \in L, srs \geq r; and
  • LL is the set of lower bounds of UU: that is, rLr \in L iff for all sUs \in U, rsr \leq s.

Given two such cuts, define (L 1,U 1)(L 2,U 2)(L_1, U_1) \leq (L_2, U_2) to mean:

  • L 1L 2L_1 \subseteq L_2; and
  • U 1U 2U_1 \supseteq U_2.

(Actually, either of these assertions alone implies the other.)

Then the set of such cuts becomes a poset, in fact a complete lattice, called the set of extended MacNeille real numbers. The MacNeille real numbers are the sub-poset consisting of the pairs (L,U)(L,U) such that LL and UU are both inhabited.

With open sets

A pair (L,U)(L,U) of subsets of \mathbb{Q} is called an open Dedekind–MacNeille cut in \mathbb{Q} if:

  • LL is an extended lower real number and UU is an extended upper real number. That is, LL is an open down-set and UU is an open up-set.
  • UU is the interior of the complement of LL: that is, sUs \in U iff there is an r<sr\lt s with rLr\notin L.
  • LL is the interior of the complement of UU: that is, rLr \in L iff there is an s>rs\gt r with sUs\notin U.

Given two such cuts, define (L 1,U 1)(L 2,U 2)(L_1, U_1) \leq (L_2, U_2) to mean:

  • L 1L 2L_1 \subseteq L_2; and
  • U 1U 2U_1 \supseteq U_2.

(Actually, either of these assertions alone implies the other.)

Then the set of such cuts becomes a poset, in fact a complete lattice, called the set of extended MacNeille real numbers. The MacNeille real numbers are the sub-poset consisting of the pairs (L,U)(L,U) such that LL and UU are both inhabited.

Comparing definitions

The open and closed definitions above are equivalent, even in constructive mathematics.

In one direction, if (L,U)(L,U) is a closed extended MacNeille real number, define L oL^o and U oU^o to be the interiors of LL and UU respectively. Then L oL^o is an extended lower real and U oU^o is an extended upper real. If sU os\in U^o, then by definition there is a t<st\lt s with tUt\in U. Then if rr is such that t<r<st\lt r \lt s, we have rLr\notin L (and hence rL or\notin L^o), since if rLr\in L we would have rtr\le t. Conversely, if we have r<sr\lt s with rL or\notin L^o, then there does not exist a t>rt\gt r with tLt\in L, which is to say (since the rationals satisfy trichotomy) that for every tLt\in L we have trt\le r, i.e. rUr\in U, and hence sU os\in U^o. The dual proof shows the corresponding axiom for L oL^o, so (L o,U o)(L^o,U^o) is an open extended MacNeille real number, which is bounded if (L,U)(L,U) is.

In the other direction, if (L,U)(L,U) is an open extended MacNeille real number, define L cL^c to be the set of lower bounds of UU, and U cU^c to be the set of upper bounds of LL. (The notation is admittedly a little misleading, since L cL^c is a function of UU rather than LL.) Then if rL cr\in L^c and sU cs\in U^c and r>sr\gt s, then for a tt such that s<t<rs\lt t\lt r we would have tUt\notin U and tLt\notin L, hence by the MacNeille condition rLr\in L and sUs\in U, a contradiction. Thus, if rL cr\in L^c and sU cs\in U^c then rsr\le s, so L cL^c consists of lower bounds for U cU^c and vice versa. Conversely, if rr is a lower bound of U cU^c, then it is also a lower bound of UU, and so rL cr\in L^c. Thus (L c,U c)(L^c,U^c) is a closed extended MacNeille real number, which is bounded if (L,U)(L,U) is.

To show that these operations are inverses, suppose first (L,U)(L,U) is a closed extended MacNeille real. Then (L o) c(L^o)^c is the set of lower bounds of the interior of UU. Any lower bound of UU is of course a lower bound for its interior, so L(L o) cL\subseteq (L^o)^c. On the other hand, if rr is a lower bound for U oU^o, to show rLr\in L it suffices to show rsr\le s for all sUs\in U. But if r>sr\gt s, then rU or\in U^o, a contradiction since U oU^o is open. Thus L=(L o) cL= (L^o)^c, and dually U=(U o) cU = (U^o)^c.

On the other side, suppose (L,U)(L,U) is an open extended MacNeille real. Then (L c) o(L^c)^o is the interior of the set of lower bounds of UU. Since LL consists of lower bounds for UU, and LL is open, we have L(L c) oL \subseteq (L^c)^o. On the other hand, if r(L c) or\in (L^c)^o then there is an sL cs\in L^c with r<sr\lt s. Then for any tt with r<t<sr\lt t\lt s we have tUt\notin U (since ss is a lower bound for UU), hence by the MacNeille condition rLr\in L. Thus L=(L o) cL= (L^o)^c, and dually U=(U o) cU = (U^o)^c.

On the rest of this page, we will adopt the open definition, since it relates better to other kinds of real numbers.

Properties

Relation to other kinds of real numbers

Any (extended) located real number is an (extended) MacNeille real number. The locatedness condition says that if r<sr\lt s then rLr\in L or sUs\in U, which certainly implies that (rL)(sU)(r\notin L)\Rightarrow (s\in U) and (sU)(rL)(s\notin U)\Rightarrow (r\in L). This gives an order-embedding.

Similarly, if (L,U)(L,U) is an (extended) MacNeille real number, then by definition LL is an (extended) lower real number and UU is an (extended) upper real number. Since LL and UU in a MacNeille real are recoverable from each other, this gives two order-embeddings.

If we define an interval to be a pair (L,U)(L,U) where LL is an extended lower real, UU is an extended upper real, and LU=L\cap U = \emptyset, then we can embed both lower reals and upper reals into the poset of intervals by taking the interior of the complement as the other half. That is, we map LL to (L,int(¬L))(L,int(\neg L)) and UU to (int(¬U),U)(int(\neg U),U) — two kinds of “singleton” intervals. These are both order-embeddings, and in fact the lower reals are a coreflective sub-poset and the upper reals are a reflective sub-poset. Thus we have an adjunction between extended lower reals and extended upper reals, and the extended MacNeille reals are the jointly fixed sub-poset. They are also the set-theoretic intersection of the lower and upper reals inside the intervals.

Completeness

Since the extended MacNeille reals are a reflective sub-poset of the extended lower reals and a coreflective sub-poset of the extended upper reals, they are closed in the former under infima and in the latter under suprema. In particular, they are a complete lattice. Note, though, that neither infima nor suprema are constructed as set-theoretic unions (unlike infima of upper reals and suprema of lower reals), which makes them less useful for purposes of constructive analysis. (On the other hand, the extended located real numbers are not, constructively, a complete lattice at all.)

References

  • Section D4.7 of Sketches of an Elephant

  • In Troelstra and van Dalen?, Constructivism in Mathematics?, section 5.5, the extended MacNeille real numbers are called the “extended real numbers” (and the MacNeille real numbers themselves are called the “bounded extended real numbers”).

Last revised on February 21, 2017 at 05:53:23. See the history of this page for a list of all contributions to it.