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


\begin{document}
	
\olfileid{sfr}{arith}{check}
\olsection{Ordered Rings and Fields}

Throughout this chapter, we claimed that certain definitions behave
``as they ought''. In this technical appendix, we will spell out what
we mean, and (sketch how to) show that the definitions do behave
``correctly''. 

In \olref[int]{sec}, we defined addition and multiplication on $\Int$.
We want to show that, as defined, they endow $\Int$ with the structure
we ``would want'' it to have. In particular, the structure in question
is that of a commutative ring.

\begin{defn}
	A \emph{commutative ring} is a set $S$, equipped with specific elements $0$ and $1$ and operations $+$ and $\times$, satisfying these eight formulas:
	\begin{align*}
		\emph{Associativity}&&a + (b+ c) & = (a + b) + c \\
		&& (a \times b) \times c & = a \times (b\times c)\\
		\emph{Commutativity}&&a + b &= b+ a  \\
		&&  a \times b&= b\times a\\ 
		\emph{Identities}&&a + 0 &= a \\
		&& a \times 1 &= a\\
		\emph{Additive Inverse}&&(\exists b\in S)0&=a + b\\
		\emph{Distributivity}&&a \times (b+ c ) &= (a \times b) + (a \times c)
	\end{align*}
	Implicitly, these are all bound with universal quantifiers restricted to $S$. And note that the elements $0$ and~$1$ here need not be the natural numbers with the same name.
\end{defn}

So, to check that the integers form a commutative ring, we just need
to check that we meet these eight conditions. None of the conditions
is {difficult} to establish, but this is a bit laborious. For example,
here is how to prove \emph{Associativity}, in the case of addition:

\begin{proof} 
Fix $i, j, k \in \Int$. So there are $a_1, b_1, a_2, b_2, a_3, b_3 \in
\Nat$ such that $i = \equivrep{a_1, b_1}{}$ and $j =
\equivrep{a_2,b_2}{}$ and $k = \equivrep{a_3, b_3}{}$. (For
legibility, we write ``$\equivrep{x, y}{}$'' rather than
``$\equivrep{x, y}{\Intequiv}$''; we'll do this throughout this
section.) Now:
\begin{align*}
	i + (j + k) &= \equivrep{a_1, b_1}{}+(\equivrep{a_2, b_2}{} + \equivrep{a_3, b_3}{}) \\
	&= \equivrep{a_1,  b_1}{} + \equivrep{a_2+a_3, b_2+b_3}{}\\
	&= \equivrep{a_1 + (a_2 + a_3), b_1 + (b_2 + b_3)}{}\\
	&= \equivrep{(a_1 + a_2) + a_3, (b_1 + b_2) + b_3}{}\\
	&= \equivrep{a_1 + a_2, b_1 + b_2}{} + \equivrep{a_3, b_3}{}\\
	&= (\equivrep{a_1, b_1}{} + \equivrep{a_2, b_2}{}) + \equivrep{a_3, b_3}{}\\
	&= (i+j) + k
\end{align*}
helping ourselves freely to the behavior of addition on $\Nat$.
\end{proof}

Equally, here is how to prove \emph{Additive Inverse}:

\begin{proof}
Fix $i \in \Int$, so that $i = \equivrep{a,b}{}$ for some $a,b \in
\Nat$. Let $j = \equivrep{b,a}{} \in \Int$. Helping ourselves to the
behaviour of the naturals, $(a+b) + 0 = 0 + (a+b)$, so that
$\tuple{a+b, b+a} \sim_\Int \tuple{0,0}$ by definition, and hence
$\equivrep{a+b, b+a}{} = \equivrep{0, 0}{} = 0_\Int$. So now $i + j =
\equivrep{a,b}{}+\equivrep{b,a}{}=\equivrep{a+b, b+a}{}= \equivrep{0,
0}{} = 0_\Int$.
\end{proof}

And here is a proof of \emph{Distributivity}:

\begin{proof}
As above, fix $i = \equivrep{a_1, b_1}{}$ and $j =
\equivrep{a_2,b_2}{}$ and $k = \equivrep{a_3, b_3}{}$. Now:
\begin{align*}
	i \times (j + k) 
	&= \equivrep{a_1, b_1}{} \times (\equivrep{a_2,b_2}{} + \equivrep{a_3, b_3}{})\\
	&= \equivrep{a_1, b_1}{} \times \equivrep{a_2 + a_3,b_2+b_3}{}\\
	&= \equivrep{a_1  (a_2 + a_3) + b_1  (b_2+b_3), a_1  (b_2 + b_3) + b_1 (a_2 + a_3)}{}\\
	&= \equivrep{a_1 a_2 + a_1a_3 + b_1 b_2+b_1b_3, a_1 b_2 + a_1b_3 + a_2b_1 + a_3b_1}{}\\		
%		&= \equivrep{a_1 a_2 + b_1b_2 + a_1a_3 + b_1 b_2+b_1b_3, a_1 b_2 + a_1b_3 + a_2b_1 + a_3b_1}{}\\		
	&= \equivrep{a_1a_2 + b_1b_2, a_1b_2 + a_2b_1}{} + \equivrep{a_1a_3 + b_1b_3, a_1b_3 + a_3b_1}{}\\
	&= (\equivrep{a_1, b_1}{} \times \equivrep{a_2,b_2}{}) + (\equivrep{a_1, b_1}{} \times  \equivrep{a_3, b_3}{})\\
	&= (i \times j) + (i \times k)
\end{align*}
\end{proof}

We leave it as an exercise to prove the remaining five conditions.
Having done that, we have shown that $\Int$ constitutes a commutative
ring, i.e., that addition and multiplication (as defined) behave as
they should.

\begin{prob}
Prove that $\Int$ is a commutative ring.
\end{prob}

But our task is not over. As well as defining addition and
multiplication over $\Int$, we defined an ordering relation, $\leq$,
and we must check that this behaves as it should. In more detail, we
must show that $\Int$ constitutes an \emph{ordered} ring.\footnote{Recall
	from \olref[sfr][rel][ord]{def:linearorder} that a total order
	is a relation which is reflexive, transitive, anti-symmetric, and connected. 
	In the context of order relations, connectedness is sometimes called
	\emph{trichotomy}, since for any $a$ and $b$ we have $a \leq b \lor a
	= b \lor a \geq b$.} 

\begin{defn}
An \emph{ordered ring} is a commutative ring which is also equipped
with a total order relation, $\leq$, such that:
\begin{align*}
	a \leq b &\lif a + c \leq b + c\\
	(a \leq b \land 0 \leq c) &\lif a \times c \leq b \times c
\end{align*}
\end{defn}

\begin{prob}
Prove that $\Int$ is an ordered ring. 
\end{prob}

As before, it is laborious but routine to show that~$\Int$, as
constructed, is an ordered ring. We will leave that to you.

This takes care of the integers. But now we need to show very similar
things of the rationals. In particular, we now need to show that the
rationals form an ordered \emph{field}, under our given definitions of
$+$, $\times$, and $\leq$:
\begin{defn}\ollabel{orderedfield}
An \emph{ordered field} is an ordered ring which also satisfies:
\begin{align*}
	\emph{Multiplicative Inverse}& & (\forall a \in S \setminus \{0\})(\exists b \in S) a\times b& = 1
\end{align*}
\end{defn}

Once you have shown that $\Int$ constitutes an ordered ring, it is
easy but laborious to show that $\Rat$ constitutes an ordered field.

\begin{prob}
Prove that $\Rat$ is an ordered field.
\end{prob}

Having dealt with the integers and the rationals, it only remains to
deal with the reals. In particular, we need to show that $\Real$
constitutes a \emph{complete} ordered field, i.e., an ordered field
with the Completeness Property. Now, \olref[cuts]{realcompleteness}
established that $\Real$ has the Completeness Property. However, it
remains to run through the (tedious) of checking that $\Real$ is an
ordered field. 

Before tearing off into \emph{that} laborious exercise, we need to
check some more ``immediate'' things. For example, we need a guarantee
that $\alpha + \beta$, as defined, is indeed a \emph{cut}, for any
cuts $\alpha$ and $\beta$. Here is a proof of that fact:

\begin{proof}	
Since $\alpha$ and $\beta$ are both cuts, $\alpha + \beta = \Setabs{p
+ q}{p \in \alpha \land q \in \beta}$ is a non-empty proper subset of
$\Rat$. Now suppose $x < p + q$ for some $p \in \alpha$ and $q \in \beta$.
Then $x - p < q$, so $x - p \in \beta$, and $x = p + (x - p) \in
\alpha + \beta$. So $\alpha + \beta$ is an initial segment of $\Rat$.
Finally, for any $p + q \in \alpha + \beta$, since $\alpha$ and
$\beta$ are both cuts, there are $p_1 \in \alpha$ and $q_1 \in \beta$
such that $p < p_1$ and $q < q_1$; so $p + q < p_1 + q_1 \in \alpha +
\beta$; so $\alpha + \beta$ has no maximum. 
\end{proof}

Similar efforts will allow you to check that $\alpha - \beta$ and
$\alpha \times \beta$ and $\alpha \div \beta$ are cuts (in the last
case, ignoring the case where $\beta$ is the zero-cut). Again, though,
we will simply leave this to you. 

\begin{prob}
Prove that $\Real$ is an ordered field.
\end{prob}

But here is a small loose end to tidy up. In
\olref[cuts]{sec}, we suggest that we can take $\sqrt{2} =
\Setabs{p \in \Rat}{p < 0 \text{ or }p^2 < 2}$. But we do need to show
that this set is a \emph{cut}. Here is a proof of that fact:

\begin{proof}
Clearly this is a nonempty proper initial segment of the rationals; so
it suffices to show that it has no maximum. In particular, it suffices
to show that, where $p$ is a positive rational with $p^2 < 2$ and $q =
\frac{2p+2}{p+2}$, both $p < q$ and $q^2 < 2$. To see that $p < q$,
just note:
\begin{align*}
	p^2 &< 2\\
	p^2 + 2p &< 2 + 2p\\
	p(p + 2) &< 2 + 2p\\
	p &< \tfrac{2+2p}{p+2} = q
\end{align*}
To see that $q^2 < 2$, just note:
\begin{align*}
	p^2 &< 2\\
	2p^2 + 4p + 2 &< p^2 + 4p+ 4\\
	4p^2 + 8p + 4 &< 2(p^2 + 4p + 4)\\
	(2p+2)^2 & <2(p+2)^2\\
	\tfrac{(2p+2)^2}{(p+2)^2} &< 2\\
	q^2 &< 2
\end{align*}
\end{proof}
\end{document}