\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*{Cauchy real number}

\hypertarget{cauchy_real_numbers}{}\section*{{Cauchy real numbers}}\label{cauchy_real_numbers}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{definitions}{Definitions}\dotfill \pageref*{definitions} \linebreak
\noindent\hyperlink{classical_version}{Classical version}\dotfill \pageref*{classical_version} \linebreak
\noindent\hyperlink{moduli_of_convergence}{Moduli of convergence}\dotfill \pageref*{moduli_of_convergence} \linebreak
\noindent\hyperlink{generalisations}{Generalisations}\dotfill \pageref*{generalisations} \linebreak
\noindent\hyperlink{relations_between_these_definitions}{Relations between these definitions}\dotfill \pageref*{relations_between_these_definitions} \linebreak
\noindent\hyperlink{generalisations_2}{Generalisations}\dotfill \pageref*{generalisations_2} \linebreak
\noindent\hyperlink{motivation}{Motivation}\dotfill \pageref*{motivation} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


\hypertarget{idea}{}\subsection*{{Idea}}\label{idea}

A Cauchy real number is a [[real number]] that is given as the limit of a [[Cauchy sequence]] of [[rational numbers]]. One may use this idea as a \emph{definition} of the general concept of real number. This is due to [[Georg Cantor]] in 1872, the same year that [[Richard Dedekind]] developed [[Dedekind cuts]] as a definition of the same concept.

\hypertarget{definitions}{}\subsection*{{Definitions}}\label{definitions}

If we simply want a construction of the [[real line]] $\mathbb{R}$ for the purposes of [[classical mathematics]], then we can use Cantor's original version. If we wish to use weak [[foundations]] or [[internalisation|internalise]] the Cauchy real line, then there are subtler alternatives.

\hypertarget{classical_version}{}\subsubsection*{{Classical version}}\label{classical_version}

Putting Cantor's definition in modern terminology, $\mathbb{R}$ is the [[quotient set]] of the set of Cauchy sequences of rational numbers, with two sequences considered equivalent if their difference converges to zero. Although the notion of Cauchy sequence (and convergence, for that matter) is best known in the context of [[metric spaces]] (which cannot be defined in general without having, at least implicitly, constructed $\mathbb{R}$ already), it is easy to state the definitions in elementary terms. If there is any tricky point, it is that the requirements made for all $\epsilon \gt 0$ need be made only for rational $\epsilon$. (We could also treat $\mathbb{Q}$ as a [[uniform space]] or even a [[Cauchy space]], although again to write down the definitions of those structures still requires one to handle the $\epsilon$s.)

To be explicit: A \textbf{Cauchy real number} $x$ is an [[infinite sequence]] $(x_0,x_1,x_2,\ldots)$ of [[rational numbers]] such that, for every positive rational number $\epsilon$, there exists a [[natural number]] $\alpha$ such that

\begin{displaymath}
{|x_i - x_j|} \leq \epsilon
\end{displaymath}
holds whenever $i,j \geq \alpha$. Two Cauchy real numbers $x,y$ are considered \textbf{equal} if, for every positive rational number $\epsilon$, there exists a natural number $\alpha$ such that

\begin{displaymath}
{|x_i - y_i|} \leq \epsilon
\end{displaymath}
holds whenever $i \geq \alpha$. It is easy to prove that this is an [[equivalence relation]] on the set of Cauchy sequences, so the set $\mathbb{R}$ of real numbers is a quotient set.

This definition comes in two steps: one to identify the Cauchy sequences from among the infinite sequences, another to identify equivalent sequences. Actually, we can do this in one step by placing a [[partial equivalence relation]] on the set of \emph{all} infinite sequences of rational numbers. Two sequences $x,y$ are considered equivalent if, for every positive rational number $\epsilon$, there exists a natural number $\alpha$ such that

\begin{displaymath}
{|x_i - y_j|} \leq \epsilon
\end{displaymath}
holds whenever $i,j \geq \alpha$. It is immediate that a sequence $x$ is Cauchy if and only if it equivalent to itself, and it is easy to prove that two Cauchy sequences $x,y$ are equivalent if and only if they are equal as real numbers using the definition above. Thus, we can construct $\mathbb{R}$ immediately as a [[subquotient]] of the [[function set]] $\mathbb{Q}^{\mathbb{N}}$.

\hypertarget{moduli_of_convergence}{}\subsubsection*{{Moduli of convergence}}\label{moduli_of_convergence}

In weak foundations, we sometimes want to be a little more strict about how a sequence is Cauchy and how the difference of two such sequences converges to zero. We do this by requiring explicit moduli of convergence. These moduli can always be constructed using (for example) either [[countable choice]] or the principle of [[excluded middle]], but the requirement makes a difference in (for example) a [[localic topos]] over any non-[[discrete space]].

(Since the term `Cauchy real number' is used ambiguously in the constructive literature, we can identify Cantor's classical definition above as a \textbf{Cantor real number} or a \textbf{classical Cauchy real number}.)

In general, a \textbf{[[modulus of convergence]]} may be any function $\alpha$ from the positive rational numbers to the natural numbers such that, for every natural number $n$, there is a positive rational number $\epsilon$ such that $\alpha(\epsilon) \geq n$.

A \textbf{modulated Cauchy real number} $x$ is an infinite sequence $(x_0,x_1,x_2,\ldots)$ of rational numbers such that there exists a modulus $\alpha$ such that

\begin{displaymath}
{|x_i - x_j|} \leq \epsilon
\end{displaymath}
holds whenever $i,j \geq \alpha(\epsilon)$. Two modulated Cauchy real numbers $x,y$ are considered \textbf{equal} if there exists a modulus $\alpha$ such that

\begin{displaymath}
{|x_i - y_i|} \leq \epsilon
\end{displaymath}
holds whenever $i \geq \alpha(\epsilon)$. Again we can combine these conditions into a single partial equivalence relation: that there exists a modulus $\alpha$ such that

\begin{displaymath}
{|x_i - y_j|} \leq \epsilon
\end{displaymath}
holds whenever $i,j \geq \alpha(\epsilon)$.

Some variations are often met. A modulus $\alpha$ may be extended to all rational numbers, although the conditions above can only be required for positive $\epsilon$. Alternatively, it is enough to define $\alpha$ (and require the conditions) for $\epsilon$ of specific form; common choices are $1/n$ and $1/2^n$ for $n$ a natural number. (The important criterion is to use a set of positive rational numbers of which zero is a limit point.)

It is also possible to fix a specific modulus $\alpha$ ahead of time. Then we need to treat each index separately, in this way: An \textbf{$\alpha$-regular Cauchy real number} $x$ is an infinite sequence $(x_0,x_1,x_2,\ldots)$ of rational numbers such that

\begin{displaymath}
{|x_i - x_j|} \leq \delta + \epsilon
\end{displaymath}
holds whenever $i \geq \alpha(\delta)$ and $j \geq \alpha(\epsilon)$. Two $\alpha$-regular Cauchy real numbers are considered \textbf{equal} if

\begin{displaymath}
{|x_i - y_i|} \leq 2\epsilon
\end{displaymath}
holds whenever $i \geq \alpha(\epsilon)$. Once more, we can combine these conditions into a single partial equivalence relation: that

\begin{displaymath}
{|x_i - y_j|} \leq \delta + \epsilon
\end{displaymath}
holds whenever $i \geq \alpha(\delta)$ and $j \geq \alpha(\epsilon)$.

\hypertarget{generalisations}{}\subsubsection*{{Generalisations}}\label{generalisations}

While requiring a modulus of convergence, even fixing the modulus of convergence, may be more restrictive, it is also possible to use a potentially more lax definition.

One way is to use [[multivalued functions]] from the natural numbers. A \textbf{multivalued Cauchy real number} $x$ is an [[entire relation]] between natural numbers and rational numbers such that, for every positive rational number $\epsilon$, there exists a natural number $\alpha$ such that, whenever $i, j \geq \alpha$,

\begin{displaymath}
{|a - b|} \leq \epsilon
\end{displaymath}
holds for some $a,b$ such that $x_{i,a}$ and $x_{j,b}$ hold. Two multivalued Cauchy real numbers are considered \textbf{equal} if, for every positive rational number $\epsilon$, there exists a natural number $\alpha$ such that, whenever $i \geq \alpha$,

\begin{displaymath}
{|a - b|} \leq \epsilon
\end{displaymath}
holds for some $a,b$ such that $x_{i,a}$ and $y_{i,b}$ hold. The partial equivalence relation subsuming both conditions is that, for every positive rational number $\epsilon$, there exists a natural number $\alpha$ such that, whenever $i,j \geq \alpha$,

\begin{displaymath}
{|a - b|} \leq \epsilon
\end{displaymath}
holds for some $a,b$ such that $x_{i,a}$ and $y_{j,b}$.

Another way is to use [[nets]] (also called `generalised sequences'). A \textbf{generalised Cauchy real number} $x$ is a net $(x_\nu)_{\nu\colon D}$ (where $D$ is any [[directed set]] of indices) of rational numbers such that, for every positive rational number $\epsilon$, there exists an index $\alpha$ in $D$ such that

\begin{displaymath}
{|x_i - x_j|} \leq \epsilon
\end{displaymath}
holds whenever $i,j \geq \alpha$ in $D$. Two generalised Cauchy real numbers $x,y$ are considered \textbf{equal} if, for every positive rational number $\epsilon$, there exists an index $\alpha$ for $x$ and an index $\beta$ for $y$ such that

\begin{displaymath}
{|x_i - y_j|} \leq \epsilon
\end{displaymath}
holds whenever $i \geq \alpha$ and $j \geq \beta$. Actually, this is already a partial equivalence relation on all nets which subsumes both conditions.

Requiring a modulus of convergence would make no difference for either of these, since we would expect such a modulus to also to be either multivalued or given by a net, and these are easy to construct explicitly (even in constructive mathematics).

(Since the term `Cauchy real number' logically applies just as well to these generalisations, we may speak of \textbf{sequential real numbers} for the classical or modulated version.)

\hypertarget{relations_between_these_definitions}{}\subsubsection*{{Relations between these definitions}}\label{relations_between_these_definitions}

Classically, all of these definitions are equivalent. In fact, to prove their equivalence, we need only the principle of \textbf{[[weak countable choice]]} ($WCC$): A [[surjective function]] $f\colon S \to \mathbb{N}$ [[split epic|splits]], if, whenever $i \ne j$, either $f^*(i)$ or $f^*(j)$ is a [[singleton]]. (This is a rather special case of [[countable choice]] that can also be proved using only [[excluded middle]].)

If we don't accept $WCC$, then we still have these results:

\begin{utheorem}
(constructive).

Given any modulus of convergence $\alpha$, every $\alpha$-regular Cauchy real number is a modulated Cauchy real number. Furthermore, any two $\alpha$-regular real numbers are equal as $\alpha$-regular real numbers if and only if they are equal as modulated Cauchy real numbers. Conversely, every modulated Cauchy real number is equal (as a modulated Cauchy real number) to some $\alpha$-regular Cauchy real number.

Every modulated Cauchy real number is a classical Cauchy real number, and any two equal modulated Cauchy real numbers are equal as classical Cauchy real numbers.

Every classical Cauchy real number is a multivalued Cauchy real number, and any two equal classical Cauchy real numbers are equal as multivalued Cauchy real numbers.

Every multivalued Cauchy real number becomes a generalised Cauchy real number whose index set $D$ comes equipped with a surjection to the natural numbers. Furthermore, any two multivalued Cauchy real numbers are equal as multivalued Cauchy real numbers if and only if they are equal as generalised Cauchy real numbers. Conversely, any generalised Cauchy real number is equal (as a generalised Cauchy real number) to some multivalued Cauchy real number.

Every generalised Cauchy real number becomes a [[Dedekind real number]] in the usual way, defining lower and upper sets in terms of the order relation on generalised Cauchy real numbers. Furthermore, any two generalised Cauchy real numbers are equal as generalised Cauchy real numbers if and only if they are equal as Dedekind cuts. Conversely, any Dedekind cut is equal (as a Dedekind cut) to some generalised Cauchy real number.

\end{utheorem}
Hence even in [[constructive mathematics]], there are only three notions that we need consider: modulated Cauchy real numbers, classical Cauchy real numbers, and Dedekind real numbers; and there is a [[function]] from each of these to the next.

Just to be explicit, here are the missing converses:

\begin{utheorem}
(assuming $WCC$).

Every classical Cauchy real number is modulated, and any two equal Cauchy real numbers are equal as modulated Cauchy real numbers.

Every multivalued Cauchy real number is equal (as a multivalued Cauchy real number) to some classical Cauchy real number, and two classical Cauchy real numbers are equal if they are equal as multivalued Cauchy real numbers.

\end{utheorem}
Most practitioners of both [[constructive mathematics]] and [[topos theory]] want to use the Dedekind real numbers. Without $WCC$, the classical Cauchy real numbers are not very well behaved. The modulated Cauchy real numbers, however, do have their good points; for example, the [[fundamental theorem of algebra]] is simplest for them. They also make sense in [[predicative mathematics]] with [[function sets]], whereas the Dedekind reals require [[powersets]] for their definition.

On the other hand, even the (modulated) Cauchy real numbers are not necessarily Cauchy complete, i.e. a Cauchy sequence (even a modulated one) of Cauchy real numbers need not converge to another Cauchy real number (though it always does converge to a Dedekind real number, since the Dedekind real numbers \emph{are} always Cauchy complete). The problem is that without countable choice, we cannot lift a (modulated) Cauchy sequence of (modulated Cauchy) real numbers to a Cauchy sequence of Cauchy sequences in order to ``diagonalize'' it; a countermodel is constructed by \hyperlink{Lubarsky}{Lubarsky}.

For non-modulated Cauchy sequences and reals, there are additional problems even if we assume representatives are already chosen. A modulated Cauchy sequence of modulated Cauchy sequences does converge to a modulated Cauchy sequence. Moreover, a \emph{modulated} Cauchy sequence of \emph{classical} Cauchy sequences, and a \emph{classical} Cauchy sequence of \emph{modulated} Cauchy sequences, both necessarily converge to a \emph{classical} Cauchy sequence. But the results need not be modulated, and a classical Cauchy sequence of classical Cauchy sequences need not converge to a classical Cauchy sequence. In fact, \hyperlink{Lubarsky}{Lubarsky} shows that:

\begin{itemize}%
\item The generic classical Cauchy sequence, in the [[classifying topos]] of classical Cauchy sequences, is not modulated. Thus, we cannot prove that every classical Cauchy sequence is modulated. Hence, we cannot prove that a classical Cauchy sequence of modulated Cauchy sequences has a modulated limit (since a classical Cauchy sequence of rationals can be regarded as a classical Cauchy sequence of (constant) modulated Cauchy sequences).


\item The generic classical Cauchy sequence of classical Cauchy sequences, in the classifying topos of such, does not converge to a classical Cauchy sequence.


\item The generic modulated Cauchy sequence of classical Cauchy sequences, in the classifying topos of such, does not converge to a modulated Cauchy sequence.



\end{itemize}
(Actually, Lubarsky writes using [[Heyting-valued sets]] on topological spaces rather than classifying toposes of propositional [[geometric theories]], but it seems almost certain to me that his results can be rephrased as the above.)

\hypertarget{generalisations_2}{}\subsection*{{Generalisations}}\label{generalisations_2}

Although the notion of [[metric space]] doesn't make sense until we know what real numbers are, once we have these, we can recognise that the rational numbers form a metric space $\mathbb{Q}$ and the real numbers were constructed from them in a way that makes reference only to the metric-space structure of $\mathbb{Q}$. Thus, this procedure may be generalised to any metric space to produce its [[complete metric space|completion]].

We can also interpret $\mathbb{Q}$ as a [[uniform space]] or even as a [[Cauchy space]] and define analogous notions of completion for these. However, these require us (in general) to use generalised Cauchy sequences, that is Cauchy [[nets]], even in classical mathematics. (Of course, without [[weak countable choice]], we should use nets even for metric spaces.)

\hypertarget{motivation}{}\subsection*{{Motivation}}\label{motivation}

Suppose that we wish to approximate a real number $x$ by common fractions with arbitrarily large denominators. That is, given any natural number $i$, we wish to find [[integers]] $a_i$ such that $x_i \coloneqq a_i/i$ is within $1/i$ of $x$. Then the sequence of values $(0,x_1,x_2,x_3,\ldots)$ is an $\alpha$-regular Cauchy real with $\alpha(1/i) \coloneqq i$ as modulus of convergence. (You can extend $\alpha$ to every positive rational number by $\alpha(\epsilon) \coloneqq \lfloor{1/\epsilon}\rfloor$, but that is not important.) Conversely, given an $\alpha$-regular Cauchy real $(x_0,x_1,x_2,\ldots)$ for this modulus $\alpha$, we can round each $x_i$ (for $i \gt 0$) to the nearest rational number with denominator $i$ (which can be done using only rational arithmetic) to produce an equal $\alpha$-regular Cauchy real.

We might instead want to approximate $x$ by arbitrarily long decimal fractions. That is, given any natural number $i$, we wish to find integers $a_i$ such that $x_i \coloneqq a_i/10^i$ is within $1/10^i$ of $x$. Now the sequence of values $(x_0,x_1,x_2,\ldots)$ is an $\alpha$-regular Cauchy real with $\alpha(1/10^i) \coloneqq i$ as modulus of convergence. Conversely, we can round off the values of any $\alpha$-regular Cauchy real as before. Of course, there is nothing special about the base $10$ here; for theoretical purposes, base $2$ is popular.

Thus, to \emph{define} a real number to be an $\alpha$-regular Cauchy real (for any of these choices of $\alpha$) is to make into a definition our intuition that we can round real numbers in this way.

Note we may be rounding up or down, regardless of which is nearer. For example, in approximating $e = \exp\,1$ by decimal fractions, we might get ($2,2.7,2.71,\ldots)$ or $(3,2.7,2.72,\ldots)$, but we might also get $(2,2.8,2.71,\ldots)$. To choose to always round down, towards zero, or towards the nearer approximant (with a rule for $0.5$) requires an application of [[excluded middle]] (or at least the [[lesser limited principle of omniscience]]).

Even for Dedekind reals without $WCC$, we can always approximate a real number in this way up to any given $i$. Choice is needed only to make infinitely many approximations at once. Trying to avoid this can motivate multivalued Cauchy real numbers.

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

\begin{itemize}%
\item [[Georg Cantor]]; 1872; \emph{\href{http://www.maths.tcd.ie/pub/HistMath/People/Cantor/Ausdehnung/}{Ueber die Ausdehnung eines Satzes aus der Theorie der trigonometrischen Reihen}}; Section 1.


\item [[Fred Richman]], Douglas Bridges, Peter Schuster; 1998; \emph{A weak countable choice principle}; available from \href{http://math.fau.edu/richman/html/docs.htm}{http\char58\char47\char47math\char46fau\char46edu\char47richman\char47html\char47docs\char46htm}.


\item [[Fred Richman]]; 1998; \emph{The fundamental theorem of algebra: a constructive development without choice}; available from \href{http://math.fau.edu/richman/html/docs.htm}{http\char58\char47\char47math\char46fau\char46edu\char47richman\char47html\char47docs\char46htm}.


\item [[Robert Lubarsky]], \emph{On the Cauchy Completeness of the Constructive Cauchy Reals}, \href{https://doi.org/10.1016/j.entcs.2006.09.012}{doi}



\end{itemize}
Formalization of Cauchy real numbers in [[homotopy type theory]] is discussed in

\begin{itemize}%
\item [[Egbert Rijke]], [[Bas Spitters]], \emph{Cauchy reals in the univalent foundations} (talk notes, May 2013) (\href{http://www.cs.ru.nl/~spitters/presentation_reals.pdf}{pdf})

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

[[!redirects Cantor real number]] [[!redirects Cantor real numbers]] [[!redirects Cantor real]] [[!redirects Cantor reals]]

[[!redirects modulated Cauchy real number]] [[!redirects modulated Cauchy real numbers]] [[!redirects modulated Cauchy real]] [[!redirects modulated Cauchy reals]]

[[!redirects regular Cauchy real number]] [[!redirects regular Cauchy real numbers]] [[!redirects regular Cauchy real]] [[!redirects regular Cauchy reals]]

[[!redirects sequential real number]] [[!redirects sequential real numbers]] [[!redirects sequential real]] [[!redirects sequential reals]]



\end{document}