\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{MacNeille real number}

\hypertarget{macneille_real_numbers}{}\section*{{MacNeille real numbers}}\label{macneille_real_numbers}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{definition}{Definition}\dotfill \pageref*{definition} \linebreak
\noindent\hyperlink{with_closed_sets}{With closed sets}\dotfill \pageref*{with_closed_sets} \linebreak
\noindent\hyperlink{with_open_sets}{With open sets}\dotfill \pageref*{with_open_sets} \linebreak
\noindent\hyperlink{comparing_definitions}{Comparing definitions}\dotfill \pageref*{comparing_definitions} \linebreak
\noindent\hyperlink{properties}{Properties}\dotfill \pageref*{properties} \linebreak
\noindent\hyperlink{relation_to_other_kinds_of_real_numbers}{Relation to other kinds of real numbers}\dotfill \pageref*{relation_to_other_kinds_of_real_numbers} \linebreak
\noindent\hyperlink{completeness}{Completeness}\dotfill \pageref*{completeness} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


\hypertarget{idea}{}\subsection*{{Idea}}\label{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).

\hypertarget{definition}{}\subsection*{{Definition}}\label{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 [[Dedekind cut|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.

\hypertarget{with_closed_sets}{}\subsubsection*{{With closed sets}}\label{with_closed_sets}

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

\begin{itemize}%
\item $U$ is the set of [[upper bounds]] of $L$: that is, $s \in U$ iff for all $r \in L$, $s \geq r$; and
\item $L$ is the set of [[lower bounds]] of $U$: that is, $r \in L$ iff for all $s \in U$, $r \leq s$.

\end{itemize}
Given two such cuts, define $(L_1, U_1) \leq (L_2, U_2)$ to mean:

\begin{itemize}%
\item $L_1 \subseteq L_2$; and
\item $U_1 \supseteq U_2$.

\end{itemize}
(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 \textbf{extended MacNeille real numbers}. The \textbf{MacNeille real numbers} are the sub-poset consisting of the pairs $(L,U)$ such that $L$ and $U$ are both [[inhabited set|inhabited]].

\hypertarget{with_open_sets}{}\subsubsection*{{With open sets}}\label{with_open_sets}

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

\begin{itemize}%
\item $L$ is an extended [[lower real number]] and $U$ is an extended [[upper real number]]. That is, $L$ is an open down-set and $U$ is an open up-set.
\item $U$ is the interior of the complement of $L$: that is, $s \in U$ iff there is an $r\lt s$ with $r\notin L$.
\item $L$ is the interior of the complement of $U$: that is, $r \in L$ iff there is an $s\gt r$ with $s\notin U$.

\end{itemize}
Given two such cuts, define $(L_1, U_1) \leq (L_2, U_2)$ to mean:

\begin{itemize}%
\item $L_1 \subseteq L_2$; and
\item $U_1 \supseteq U_2$.

\end{itemize}
(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 \textbf{extended MacNeille real numbers}. The \textbf{MacNeille real numbers} are the sub-poset consisting of the pairs $(L,U)$ such that $L$ and $U$ are both [[inhabited set|inhabited]].

\hypertarget{comparing_definitions}{}\subsubsection*{{Comparing definitions}}\label{comparing_definitions}

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

In one direction, if $(L,U)$ is a closed extended MacNeille real number, define $L^o$ and $U^o$ to be the interiors of $L$ and $U$ respectively. Then $L^o$ is an extended lower real and $U^o$ is an extended upper real. If $s\in U^o$, then by definition there is a $t\lt s$ with $t\in U$. Then if $r$ is such that $t\lt r \lt s$, we have $r\notin L$ (and hence $r\notin L^o$), since if $r\in L$ we would have $r\le t$. Conversely, if we have $r\lt s$ with $r\notin L^o$, then there does not exist a $t\gt r$ with $t\in L$, which is to say (since the rationals satisfy trichotomy) that for every $t\in L$ we have $t\le r$, i.e. $r\in U$, and hence $s\in U^o$. The dual proof shows the corresponding axiom for $L^o$, so $(L^o,U^o)$ is an open extended MacNeille real number, which is bounded if $(L,U)$ is.

In the other direction, if $(L,U)$ is an open extended MacNeille real number, define $L^c$ to be the set of lower bounds of $U$, and $U^c$ to be the set of upper bounds of $L$. (The notation is admittedly a little misleading, since $L^c$ is a function of $U$ rather than $L$.) Then if $r\in L^c$ and $s\in U^c$ and $r\gt s$, then for a $t$ such that $s\lt t\lt r$ we would have $t\notin U$ and $t\notin L$, hence by the MacNeille condition $r\in L$ and $s\in U$, a contradiction. Thus, if $r\in L^c$ and $s\in U^c$ then $r\le s$, so $L^c$ consists of lower bounds for $U^c$ and vice versa. Conversely, if $r$ is a lower bound of $U^c$, then it is also a lower bound of $U$, and so $r\in L^c$. Thus $(L^c,U^c)$ is a closed extended MacNeille real number, which is bounded if $(L,U)$ is.

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

On the other side, suppose $(L,U)$ is an open extended MacNeille real. Then $(L^c)^o$ is the interior of the set of lower bounds of $U$. Since $L$ consists of lower bounds for $U$, and $L$ is open, we have $L \subseteq (L^c)^o$. On the other hand, if $r\in (L^c)^o$ then there is an $s\in L^c$ with $r\lt s$. Then for any $t$ with $r\lt t\lt s$ we have $t\notin U$ (since $s$ is a lower bound for $U$), hence by the MacNeille condition $r\in L$. Thus $L= (L^o)^c$, and dually $U = (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.

\hypertarget{properties}{}\subsection*{{Properties}}\label{properties}

\hypertarget{relation_to_other_kinds_of_real_numbers}{}\subsubsection*{{Relation to other kinds of real numbers}}\label{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\lt s$ then $r\in L$ or $s\in U$, which certainly implies that $(r\notin L)\Rightarrow (s\in U)$ and $(s\notin U)\Rightarrow (r\in L)$. This gives an order-embedding.

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

If we define an \textbf{interval} to be a pair $(L,U)$ where $L$ is an extended lower real, $U$ is an extended upper real, and $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 $L$ to $(L,int(\neg L))$ and $U$ to $(int(\neg U),U)$ --- two kinds of ``singleton'' intervals. These are both order-embeddings, and in fact the lower reals are a [[coreflective subcategory|coreflective]] sub-poset and the upper reals are a [[reflective subcategory|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.

\hypertarget{completeness}{}\subsubsection*{{Completeness}}\label{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.)

\hypertarget{references}{}\subsection*{{References}}\label{references}

\begin{itemize}%
\item Section D4.7 of [[Sketches of an Elephant]]


\item In [[Anne Troelstra|Troelstra]] and [[Dirk van Dalen|van Dalen]], \emph{[[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'').



\end{itemize}
[[!redirects MacNeille real number]] [[!redirects MacNeille real numbers]] [[!redirects MacNeille real]] [[!redirects MacNeille reals]] [[!redirects MacNeille number]] [[!redirects MacNeille numbers]]



\end{document}