% Part: sets-functions-relations
% Chapter: arithmetization
% Section: cuts
%
\documentclass[../../../include/open-logic-section]{subfiles}

\begin{document}

\olfileid{sfr}{arith}{cuts}
\olsection{From $\Rat$ to $\Real$}

In essence, the Completeness Property shows that any point $\alpha$ of
the real line divides that line into two halves perfectly: those for
which $\alpha$ is the least upper bound, and those for which $\alpha$
is the greatest lower bound. To \emph{construct} the real numbers from
the rational numbers, Dedekind suggested that we simply think of the
reals as the \emph{cuts} that partition the rationals. That is, we
identify $\sqrt{2}$ with the \emph{cut} which separates the rationals
$< \sqrt{2}$ from the rationals $> \sqrt{2}$. 

Let's tidy this up. If we cut the rational numbers into two halves, we
can uniquely identify the partition we made just by considering its
\emph{bottom} half. So, getting precise, we offer the following
definition:

\begin{defn}[Cut] 
A \emph{cut} $\alpha$ is any non-empty proper
initial segment of the rationals with no greatest element. That is,
$\alpha$ is a cut iff:
\begin{enumerate}
	\item \emph{non-empty, proper}: $\emptyset \neq \alpha \subsetneq \Rat$
	\item \emph{initial}: for all $p,q \in \Rat$: if $p < q \in \alpha$ then $p \in \alpha$
	\item \emph{no maximum}: for all $p \in \alpha$ there is a $q \in \alpha$ such that $p < q$ 
\end{enumerate} 
Then $\Real$ is the set of cuts. 
\end{defn}

So now we can say that $\sqrt{2} = \Setabs{p \in \Rat}{p^2 < 2\text{
or }p < 0}$. Of course, we need to check that this \emph{is} a cut,
but we relegate that to \olref[check]{sec}.

As before, having defined some entities, we next need to define basic
functions and relations upon them. We begin with an easy one:
\begin{align*}
	\alpha \leq \beta \text{ iff }\alpha \subseteq \beta
\end{align*}
This definition of an order allows to \emph{state} the central result,
that the set of cuts has the Completeness Property. Spelled out fully,
the statement has this shape. If $S$ is a non-empty set of cuts with
an upper bound, then $S$ has a least upper bound. In more detail: there is a cut, $\lambda$, which is an upper bound for $S$, i.e.\ $(\forall \alpha \in S)\alpha \subseteq
\lambda$, and $\lambda$ is the least such cut, i.e.\ $(\forall \beta \in \Real)((\forall \alpha \in S)\alpha \subseteq \beta \lif \lambda \subseteq \beta)$. Now here is
the proof of the result:

\begin{thm}\ollabel{realcompleteness}
The set of cuts has the Completeness Property. 
\end{thm}

\begin{proof}
Let $S$ be any non-empty set of cuts with an upper bound. Let $\lambda
= \bigcup S$. 
%\Setabs{p \in \Rat}{(\exists \alpha \in S)p \in \alpha}$$
We first claim that $\lambda$ is a cut:
\begin{enumerate}
\item Since $S$ has an upper bound, at least one cut is in $S$, so
$\emptyset \neq \lambda$. Since $S$ is a set of cuts, $\lambda
\subseteq \Rat$. Since $S$ has an upper bound, some $p \in \Rat$ is
absent from every cut $\alpha \in S$. So $p\notin \lambda$, and hence
$\lambda \subsetneq \Rat$.
\item Suppose $p < q \in \lambda$. So there is some $\alpha \in S$
such that $q \in \alpha$. Since $\alpha$ is a cut, $p \in \alpha$. So
$p \in \lambda$.
\item Suppose $p \in \lambda$. So there is some $\alpha \in S$ such
that $p \in \alpha$. Since $\alpha$ is a cut, there is some $q \in
\alpha$ such that $p < q$. So $q \in \lambda$. 
\end{enumerate}
This proves the claim. Moreover, clearly $(\forall \alpha \in S)\alpha
\subseteq \bigcup S = \lambda$, i.e.\ $\lambda$ is an upper bound on $S$. So now suppose $\beta \in \mathbb{R}$ is also an upper bound, i.e.\ $(\forall \alpha \in S)\alpha \subseteq \beta$. For any $p \in \Rat$, if $p \in \lambda$, then there is $\alpha \in S$ such that $p \in \alpha$, so that $p \in \beta$. Generalizing, $\lambda \subseteq \beta$. So $\lambda$ is the \emph{least} upper bound on $S$.
\end{proof}

So we have a bunch of entities which satisfy the Completeness
Property. And one way to put this is: there are no ``gaps'' in our
cuts. (So: taking further ``cuts'' of reals, rather than rationals,
would yield no interesting new objects.)

Next, we must define some operations on the reals. We start by
embedding the rationals into the reals by stipulating that $p_\Real =
\Setabs{q \in \Rat}{q < p}$ for each $p \in \Rat$. We then define:
\begin{align*}
	\alpha + \beta &= \Setabs{p + q}{p \in \alpha \land q \in \beta}\\
%	\alpha - \beta &\defis \Setabs{p - q}{p \in \alpha \land q \in \Rat \setminus \beta}\\
	\alpha \times \beta &= 
	\Setabs{p \times q}{0 \leq p \in \alpha \land 0 \leq q \in \beta} \cup 0^\mathbb{R} & \text{if }\alpha, \beta \geq 0_\Real
%	\alpha \div \beta &\defis 
%	\Setabs{\nicefrac{p}{q}}{p \in \alpha \land q \in \Rat \setminus \beta}  & \text{if }\alpha \geq 0_\Real, \beta > 0_\Real
\end{align*}
To handle the other multiplication cases, first let: %that $0_\Real \times \alpha = 0_\Real = \alpha \times 0_\Real$, and add:
\begin{align*}
	-\alpha &= \Setabs{p - q}{p < 0 \land q \notin \alpha}
\end{align*}
and then stipulate:
\begin{align*}
	\alpha \times \beta &\defis 
	\begin{cases}
		\mathord{-}\alpha \times \mathord{-}\beta &\text{if }\alpha < 0_\Real\text{ and }\beta < 0_\Real\\
		\mathord{-}(\mathord{-}\alpha \times \beta) &\text{if }\alpha < 0_\Real \text{ and }\beta > 0_\Real\\
		\mathord{-}(\alpha \times \mathord{-}\beta) &\text{if }\alpha > 0_\Real \text{ and }\beta < 0_\Real
	\end{cases}
\end{align*}
We then need to check that each of these definitions always yields a
cut. And finally, we need to go through an easy (but long-winded)
demonstration that the cuts, so defined, behave exactly as they
should. But we relegate all of this to \olref[check]{sec}.
\end{document}