Infinite Sets — Source and provenance

Source and provenance

This successor consumes only the independently accepted chapter slice. The exact projected TeX is shown line by line, and the source-coordinate crosswalk below materializes every coordinate used by formulas, formal objects, references, structures, and corrections. It does not claim that the crosswalk is a complete copy of each upstream source file.

Open the exact accepted projected TeX. Open the accepted chapter-slice receipt.

Accepted projected chapter

20520 bytes; SHA-256 0e5d6e459ee8889e0c2f084f1311109e9d9df7d6019ff4bd6afa4e15e2f403b6.

\olchapter{sfr}{infinite}{Infinite Sets}
\begin{editorial}
This chapter on infinite sets is taken from Tim Button's \emph{Open
Set Theory}.
\end{editorial}
\olfileid{sfr}{infinite}{hilbert}
\olsection{Hilbert's Hotel}
The set of the natural numbers is obviously infinite. So, if we do not
want to \emph{help ourselves} to the natural numbers, our first step
must be characterize an infinite set in terms that do not require
mentioning the natural numbers themselves. Here is a nice approach,
presented by Hilbert in a lecture from 1924. He asks us to imagine
\begin{quote}
[\ldots] a hotel with a finite number of rooms. All of these rooms
should be occupied by exactly one guest. If the guests now swap their
rooms somehow, [but] so that each room still contains no more than one
person, then no rooms will become free, and the hotel-owner cannot in
this way create a new place for a newly arriving guest [\ldots
\textparagraph \ldots]
Now we stipulate that the hotel shall have infinitely many numbered
rooms $1$, $2$, $3$, $4$, $5$, \dots, each of which is occupied by
exactly one guest. As soon as a new guest comes along, the owner only
needs to move each of the old guests into the room associated with the
number one higher, and room~$1$ will be free for the newly-arriving
guest.
\begin{center}
\begin{tikzpicture}[scale = .75]
\foreach \x in {1, 2, 3, 4, 5, 6, 7, 8, 9}
{
\node (\x a) at (\x, 1) {\small{\x}};
\node (\x b) at (\x, 2) {\small{\x}};
}
\node (dotsa) at (10, 1) {\small{\ldots}};
\node (dotsb) at (10, 2) {\small{\ldots}};
\draw[->] (1b)--(2a);
\draw[->] (2b)--(3a);
\draw[->] (3b)--(4a);
\draw[->] (4b)--(5a);
\draw[->] (5b)--(6a);
\draw[->] (6b)--(7a);
\draw[->] (7b)--(8a);
\draw[->] (8b)--(9a);
\draw[->] (9b)--(dotsa);
\draw (1,1) circle (.4);
\end{tikzpicture}
\end{center}
(published in \citealt[730]{EwaldSieg2013}; our translation)
\end{quote}
The crucial point is that Hilbert's Hotel has infinitely many rooms;
and we can take his explanation to define what it means to say this.
Indeed, this was Dedekind's approach (presented here, of course, with
massive anachronism; Dedekind's definition is from
\citeyear{Dedekind1888}):
\begin{defn}\ollabel{defn:DedekindInfinite}
A set $A$ is \emph{Dedekind infinite} iff there is !!a{injection}
from~$A$ to a proper subset of~$A$. That is, there is some $o \in A$
and !!a{injection} $f \colon A \to A$ such that $o \notin \ran{f}$.
\end{defn}
\olfileid{sfr}{infinite}{dedekind}
\olsection{Dedekind Algebras}
We not only want natural numbers to be infinite; we want them to have
certain (algebraic) properties: they need to behave well under
addition, multiplication, and so forth.
Dedekind's idea was to take the idea of the \emph{successor function}
as basic, and then characterise the numbers as those with the
following properties:
\begin{enumerate}
\item There is a number, $0$, which is not the successor of any number
\\i.e., $0 \notin \ran{s}$
\\i.e., $\forall x\ s(x) \neq 0$
\item Distinct numbers have distinct successors
\\i.e., $s$ is !!a{injection}
\\i.e., $\forall x \forall y (s(x) = s(y) \lif x = y)$
\item\ollabel{repeatedapplication} Every number is obtained from
$0$ by repeated applications of the successor function.
\end{enumerate}
The first two conditions are easy to deal with using first-order logic
(see above). But we cannot deal with \olref{repeatedapplication} just
using first-order logic. Dedekind's breakthrough was to reformulate
condition \olref{repeatedapplication}, set-theoretically, as follows:
\begin{enumerate}
\item[3$'$.] The natural numbers are the smallest set that is
\emph{closed under the successor function}: that is, if we apply
$s$ to any !!{element} of the set, we obtain another !!{element}
of the set.
\end{enumerate}
But we shall need to spell this out slowly.
\begin{defn}\ollabel{Closure}
For any function $f$, the set $X$ is $f$-\emph{closed} {iff}
$(\forall x \in X)f(x) \in X$. Now define, for any $o$:
$$\closureofunder{f}{o} = \bigcap\Setabs{X}{o \in X\text{ and }X
\text{ is $f$-closed}}$$
\end{defn}
So $\closureofunder{f}{o}$ is the intersection of all the $f$-closed
sets with $o$ as !!a{element}. Intuitively, then,
$\closureofunder{f}{o}$ is the \emph{smallest} $f$-closed set with $o$
as !!a{element}. This next result makes that intuitive thought
precise;
\begin{lem}\ollabel{closureproperties}
For any function $f$ and any $o \in A$:
\begin{enumerate}
\item\ollabel{closurehaselem} $o \in \closureofunder{f}{o}$; and
\item\ollabel{closureclosed} $\closureofunder{f}{o}$ is $f$-closed; and
\item\ollabel{closuresmallest} if $X$ is $f$-closed and $o \in
X$, then $\closureofunder{f}{o} \subseteq X$
\end{enumerate}
\end{lem}
\begin{proof}
Note that there is at least one $f$-closed set with $o$ as !!a{element}, namely $\ran{f}\cup
\{o\}$. So $\closureofunder{f}{o}$, the intersection of \emph{all}
such sets, exists. We must now check
\olref{closurehaselem}--\olref{closuresmallest}.
Concerning \olref{closurehaselem}: $o \in \closureofunder{f}{o}$ as it is an
intersection of sets which all have $o$ as !!a{element}.
Concerning \olref{closureclosed}: suppose $x \in \closureofunder{f}{o}$. So if $o \in X$ and $X$ is $f$-closed, then $x \in X$, and now $f(x) \in X$ as $X$ is
$f$-closed. So $f(x) \in \closureofunder{f}{o}$.
Concerning \olref{closuresmallest}: quite generally, if $X
\in C$ then $\bigcap C \subseteq X$.
\end{proof}
Using this, we can say:
\begin{defn}
A \emph{Dedekind algebra} is a set $A$ together with a function $f
\colon A \to A$ and some $o \in A$ such that:
\begin{enumerate}
\item \ollabel{ded:proper} $o \notin \ran{f}$
\item \ollabel{ded:injection} $f$ is !!a{injection}
\item \ollabel{ded:closure} $A = \closureofunder{f}{o}$
\end{enumerate}
\end{defn}
Since $A = \closureofunder{f}{o}$, our earlier result tells us that
$A$ is the smallest $f$-closed set with $o$ as !!a{element}. Clearly a
Dedekind algebra is Dedekind infinite; just look at clauses
\olref{ded:proper} and \olref{ded:injection} of the definition. But
the more exciting fact is that any Dedekind infinite set can be turned
into a Dedekind algebra.
\begin{thm}\ollabel{thm:DedekindInfiniteAlgebra}
If there is a Dedekind infinite set, then there is a Dedekind algebra.
\end{thm}
\begin{proof}
Let $D$ be Dedekind infinite. So there is an injection $g \colon D \to
D$ and an element $o \in D \setminus \ran{g}$. Now let $A =
\closureofunder{g}{o}$; by \olref{closureproperties}, $A$ exists and $o \in A$. Let $f =
\funrestrictionto{g}{A}$. We will show that $A, f, o$ comprise a Dedekind
algebra.
Concerning \olref{ded:proper}: $o \notin \ran{g}$ and $\ran{f}
\subseteq \ran{g}$ so $o\notin \ran{f}$.
Concerning \olref{ded:injection}: $g$ is an injection on $D$; so $f
\subseteq g$ must be an injection.
Concerning \olref{ded:closure}: by \olref{closureproperties}, $A$ is $g$-closed; a fortiori, $A$ is $f$-closed. So $\closureofunder{f}{o} \subseteq A$ by \olref{closureproperties}. Since also $\closureofunder{f}{o}$ is $f$-closed and $f = \funrestrictionto{g}{A}$, it follows that $\closureofunder{f}{o}$ is $g$-closed. So $A \subseteq \closureofunder{f}{o}$ by \olref{closureproperties}.
\end{proof}
\olfileid{sfr}{infinite}{induction}
\olsection[Arithmetical Induction]{Dedekind Algebras and Arithmetical Induction}
Crucially, now, a Dedekind algebra---indeed, \emph{any} Dedekind
algebra---will serve as a surrogate for the natural numbers. This is
thanks to the following trivial consequence:
\begin{thm}[Arithmetical induction]\ollabel{thm:dedinfiniteinduction}
Let $N, s, o$ comprise a Dedekind algebra. Then for any set $X$:
\begin{center}
if $o \in X$ and $(\forall {n} \in N \cap X){s}({n}) \in X$, {then} $N \subseteq X$.
\end{center}
\end{thm}
\begin{proof}
By the definition of a Dedekind algebra, $N = \closureofunder{s}{o}$.
Now if both ${o} \in X$ and $(\forall {n} \in N)(n \in X \lif
{s}({n}) \in X)$, then $N = \closureofunder{s}{o} \subseteq X$.
\end{proof}
Since induction is characteristic of the natural numbers, the point is
this. Given any Dedekind infinite set, we can form a Dedekind algebra,
and use that algebra as our surrogate for the natural numbers.
Admittedly, \olref{thm:dedinfiniteinduction} formulates induction in
\emph{set-theoretic} terms. But we can easily put the principle in
terms which might be more familiar:
\begin{cor}\ollabel{natinductionschema}
Let $N, s, o$ comprise a Dedekind algebra. Then for any formula
$\phi(x)$, which may have parameters:
\begin{center}
if $\phi(o)$ and $(\forall {n} \in N)(\phi(n)\lif
\phi({s}({n})))$, {then} $(\forall n \in N)\phi(n)$
\end{center}
\end{cor}
\begin{proof}
Let $X = \Setabs{n \in N}{\phi(n)}$, and now use
\olref{thm:dedinfiniteinduction}
\end{proof}
In this result, we spoke of a formula ``having parameters''. What this
means, roughly, is that for any objects $c_1, \ldots, c_k$, we can
work with $\phi(x, c_1, \ldots, c_k)$. More precisely, we can state
the result without mentioning ``parameters'' as follows. For any
formula $\phi(x, v_1, \ldots, v_k)$, whose free variables are all
displayed, we have:
\begin{align*}
\forall v_1 \ldots \forall v_k((&\phi(o, v_1,\ldots, v_k) \land {}\\
& (\forall x \in N)(\phi(x,v_1, \ldots, v_k) \lif \phi(s(x), v_1,\ldots, v_k))) \lif {}\\
&\hspace{3em} (\forall x \in N)\phi(x, v_1,\ldots, v_k))
\end{align*}
Evidently, speaking of ``having parameters'' can make things much
easier to read. (In \olref[sth][][]{part}, we will use this device
rather frequently.)
Returning to Dedekind algebras: given any Dedekind algebra, we can
also define the usual arithmetical functions of addition,
multiplication and exponentiation. This is non-trivial, however, and
it involves the technique of \emph{recursive definition}. That is a
technique which we shall introduce and justify much later, and in a
much more general context. (Enthusiasts might want to revisit this
after \olref[sth][ord-arithmetic][]{chap}, or perhaps read an alternative
treatment, such as \citealt[pp.~95--8]{Potter2004}.) But, where $N, s, o$
comprise a Dedekind algebra, we will ultimately be able to stipulate the
following:
\begin{align*}
{a} + {o} &= {a} & & & {a} \times {o} &= {o} & & & {a}^{o} &= s(o)\\
{a} + {s}({b}) &= {s}({a}+{b}) &&& {a} \times {s}({b}) &= ({a}\times {b}) + {a} & & & {a}^{{s}({b})} &= {a}^{b} \times {a}
\end{align*}
and show that these behave as one would hope.
\olfileid{sfr}{infinite}{dedekindsproof}
\olsection[Dedekind's ``Proof'']{Dedekind's ``Proof'' of the
Existence of an Infinite Set}
In this chapter, we have offered a set-theoretic treatment of the
natural numbers, in terms of Dedekind algebras. In
\olref[arith][ref]{sec}, we reflected on the philosophical
significance of the arithmetisation of analysis (among other things).
Now we should reflect on the significance of what we have achieved
here.
Throughout \olref[sfr][arith][]{chap}, we took the natural numbers as
given, and used them to construct the integers, rationals, and reals,
explicitly. In this chapter, we have not given an explicit
construction of the natural numbers. We have just shown that,
\emph{given any Dedekind infinite set}, we can define a set which will
behave just like we want~$\Nat$ to behave.
Obviously, then, we cannot claim to have answered a metaphysical
question, such as \emph{which objects are the natural numbers}. But
that's a good thing. After all, in \olref[sfr][arith][ref]{sec}, we
emphasized that we would be wrong to think of the definition of
$\Real$ as the set of Dedekind cuts as a \emph{discovery}, rather than
a convenient stipulation. The crucial observation is that the Dedekind
cuts exemplify the key mathematical properties of the real
numbers. So too here: the crucial observation is that \emph{any}
Dedekind algebra exemplifies the key mathematical properties of the
natural numbers. (Indeed, Dedekind pushed this point home by proving
that all Dedekind algebras are \emph{isomorphic} (\citeyear[Theorems
132--3]{Dedekind1888}). It is no surprise, then, that many
contemporary ``structuralists'' cite Dedekind as a forerunner.)
Moreover, we have shown how to embed the theory of the natural
numbers into a na\"ive simple set theory, which itself still remains
rather informal, but which doesn't (apparently) assume the natural
numbers as given. So, we may be on the way to realising Dedekind's
own ambitious project, which he explained thus:
\begin{quote}
In science nothing capable of proof ought to be believed without
proof. Though this demand seems reasonable, I cannot regard it as
having been met even in the most recent methods of laying the
foundations of the simplest science; viz., that part of logic
which deals with the theory of numbers. In speaking of arithmetic
(algebra, analysis) as merely a part of logic I mean to imply that
I consider the number-concept entirely independent of the notions
or intuitions of space and time---that I rather consider it an
immediate product of the pure laws of thought.
\citep[preface]{Dedekind1888}
\end{quote}
Dedekind's bold idea is this. We have just shown how to build the
natural numbers using (na\"ive) set theory alone. In
\olref[sfr][arith][]{chap}, we saw how to construct the reals given
the natural numbers and some set theory. So, perhaps, ``arithmetic
(algebra, analysis)'' turn out to be ``merely a part of logic'' (in
Dedekind's extended sense of the word ``logic'').
That's the idea. But hold on for a moment. Our construction of a
Dedekind algebra (our surrogate for the natural numbers) is
conditional on the existence of a Dedekind infinite set. (Just look
back to \olref[sfr][infinite][dedekind]{thm:DedekindInfiniteAlgebra}.)
Unless the existence of a Dedekind infinite set can be established via
``logic'' or ``the pure laws of thought'', the project stalls.
So, \emph{can} the existence of a Dedekind infinite set be established
by ``the pure laws of thought''? Here was Dedekind's effort:
\begin{quote}
My own realm of thoughts, i.e., the totality $S$ of all things which
can be objects of my thought, is infinite. For if $s$ signifies an
element of~$S$, then the thought $s'$ that~$s$ can be an object of
my thought, is itself an element of~$S$. If we regard this as an
image $\phi(s)$ of the element~$s$, then \dots~$S$ is [Dedekind]
infinite, which was to be proved.
\citep[\S66]{Dedekind1888}
\end{quote}
This is quite an astonishing thing to find in the middle of a book
which largely consists of highly rigorous mathematical proofs. Two
remarks are worth making.
First: this ``proof'' scarcely has what we would now recognize as a
``mathematical'' character. It speaks of psychological objects
(thoughts), and merely \emph{possible} ones at that.
Second: at least as we have presented Dedekind algebras, this
``proof'' has a straightforward technical shortcoming. If Dedekind's
argument is successful, it establishes only that there are infinitely
many things (specifically, infinitely many thoughts). But Dedekind
also needs to give us a reason to regard~$S$ as a single \emph{set},
with infinitely many !!{element}s, rather than thinking of~$S$ as
\emph{some things} (in the plural).
The fact that Dedekind did not see a gap here might suggest that his
use of the word ``totality'' does not precisely track \emph{our} use
of the word ``set''.\footnote{Indeed, we have other reasons to think
it did not; see \citet[p.~23]{Potter2004}.} But this would not be
too surprising. The project we have pursued in the last two
chapters---a ``construction'' of the naturals, and from them a
``construction'' of the integers, reals and rationals---has all been
carried out na\"ively. We have helped ourselves to this set, or that
set, as and when we have needed them, without laying down many general
principles concerning exactly which sets exist, and when. But we know
that we need \emph{some} general principles, for otherwise we will
fall into Russell's Paradox.
The time has come for us to outgrow our na\"ivety.
\olfileid{sfr}{infinite}{card-sb}
\olsection{Appendix: Proving Schr\"oder-Bernstein}
Before we depart from na\"ive set theory, we have one last na\"ive
(but sophisticated!) proof to consider. This is a proof of
Schr\"oder-Bernstein (\olref[sfr][siz][sb]{thm:schroder-bernstein}): if
$\cardle{A}{B}$ and $\cardle{B}{A}$ then $\cardeq{A}{B}$; i.e., given
!!{injection}s $f \colon A \to B$ and $g \colon B \to A$ there is
!!a{bijection} $h \colon A \to B$.
In this chapter, we followed Dedekind's notion of \emph{closures}. In
fact, Dedekind provided a lovely proof of Schr\"oder-Bernstein using this notion, and we
will present it here. The proof closely follows
\citet[pp.~157--8]{Potter2004}, if you want a slightly different but
essentially similar treatment. A little googling will also convince
you that this is a theorem---rather like the irrationality of
$\sqrt{2}$---for which \emph{many} interesting and different proofs
exist.
Using similar notation as \olref[sfr][infinite][dedekind]{Closure},
let
\[
\Closureofunder{f}{B} = \bigcap \Setabs{X}{B \subseteq X
\text{ and $X$ is $f$-closed}}
\]
for each set $B$ and function~$f$. Defined thus,
$\Closureofunder{f}{B}$ is the smallest $f$-closed set containing~$B$,
in that:
\begin{lem}\ollabel{Closureprops}
For any function $f$, and any $B$:
\begin{enumerate}
\item\ollabel{Closurehaselem} $B \subseteq \Closureofunder{f}{B}$; and
\item\ollabel{Closureclosed} $\Closureofunder{f}{B}$ is $f$-closed; and
\item\ollabel{Closuresmallest} if $X$ is $f$-closed and $B
\subseteq X$, then $\Closureofunder{f}{B} \subseteq X$.
\end{enumerate}
\end{lem}
\begin{proof}
Exactly as in \olref[sfr][infinite][dedekind]{closureproperties}.
\end{proof}
We need one last fact to get to Schr\"oder-Bernstein:
\begin{prop}\ollabel{sbhelper}
If $A \subseteq B \subseteq C$ and $A \approx C$, then $\cardeq{\cardeq{A}{B}}{C}$.
\end{prop}
\begin{proof}
Given !!a{bijection} $f \colon C \to A$, let $F =
\Closureofunder{f}{C \setminus B}$ and define a function $g$ with
domain $C$ as follows:
\[
g(x) =
\begin{cases}
f(x) &\text{if $x \in F$}\\
x & \text{otherwise}
\end{cases}
\]
We'll show that $g$ is !!a{bijection} from $C \to B$, from which it
will follow that $\comp{f^{-1}}{g} \colon A \to B$ is !!a{bijection},
completing the proof.
First we claim that if $x \in F$ but $y\notin F$ then $g(x) \neq
g(y)$. For reductio suppose otherwise, so that $y = g(y) = g(x) =
f(x)$. Since $x \in F$ and $F$ is $f$-closed by \olref{Closureprops},
we have $y = f(x) \in F$, a contradiction.
Now suppose $g(x) = g(y)$. So, by the above, $x \in F$ iff $y \in F$.
If $x, y \in F$, then $f(x) = g (x) = g(y) = f(y)$ so that $x = y$
since $f$ is !!a{bijection}. If $x, y \notin F$, then $x = g(x) =
g(y) = y$. So $g$ is !!a{injection}.
It remains to show that $\ran{g} = B$. So fix $x \in B \subseteq C$.
If $x \notin F$, then $g(x) = x$. If $x \in F$, then $x = f(y)$ for
some $y \in F$, since otherwise $F \setminus \{x\}$ would be $f$-closed and extend $C\setminus B$, which is impossible by \olref{Closureprops}; now $g(y) = f(y) = x$.
\end{proof}
Finally, here is the proof of the main result. Recall that given a
function $h$ and set $D$, we define $\funimage{h}{D} = \Setabs{h(x)}{x
\in D}$.
\begin{proof}[Proof of Schr\"oder-Bernstein] Let $f \colon A \to B$
and $g \colon B \to A$ be !!{injection}s. Since $\funimage{f}{A}
\subseteq B$ we have that $\funimage{g}{\funimage{f}{A}} \subseteq
g[B] \subseteq A$. Also, $\comp{f}{g} \colon A \to
\funimage{g}{\funimage{f}{A}}$ is an !!{injection} since both $g$ and
$f$ are; and indeed $\comp{f}{g}$ is !!a{bijection}, just by the way
we defined its codomain. So
$\cardeq{\funimage{g}{\funimage{f}{A}}}{A}$, and hence by
\olref{sbhelper} there is !!a{bijection} $h \colon A \to
\funimage{g}{B}$. Moreover, $g^{-1}$ is !!a{bijection}
$\funimage{g}{B} \to B$. So $\comp{h}{g^{-1}} \colon A \to B$ is
!!a{bijection}.
\end{proof}
\OLEndPartHook

content/sets-functions-relations/infinite/infinite.tex

1 exact source-coordinate anchors materialized from the accepted slice ledgers.

Line 8 · structure · records structure-00048
```
\olchapter{Infinite Sets}
```

content/sets-functions-relations/infinite/hilberts-hotel.tex

34 exact source-coordinate anchors materialized from the accepted slice ledgers.

Line 10 · structure · records structure-00049
```
\olsection{Hilbert's Hotel}
```

Line 14 · source-correction · records TR007-SOURCE-PROSE-001

must be characterize an infinite set in terms that do not require

Line 25 · formula-context · records projected-formula-0002755 projected-formula-0002756 projected-formula-0002757 projected-formula-0002758 projected-formula-0002759
```
Now we stipulate that the hotel shall have infinitely many numbered
```
Line 26 · formula · records projected-formula-0002755 projected-formula-0002756 projected-formula-0002757 projected-formula-0002758 projected-formula-0002759
```
rooms $1$, $2$, $3$, $4$, $5$, \dots, each of which is occupied by
```
Line 27 · formula-context · records projected-formula-0002755 projected-formula-0002756 projected-formula-0002757 projected-formula-0002758 projected-formula-0002759
```
exactly one guest. As soon as a new guest comes along, the owner only
```

Line 28 · formula-context · records projected-formula-0002760

needs to move each of the old guests into the room associated with the

Line 29 · formula · records projected-formula-0002760

number one higher, and room~$1$ will be free for the newly-arriving

Line 30 · formula-context · records projected-formula-0002760
```
guest. 
```
Line 32 · formal-object · records projected-env-000397
```
		\begin{tikzpicture}[scale = .75]
```
Line 33 · formal-object · records projected-env-000397
```
		\foreach \x in {1, 2, 3, 4, 5, 6, 7, 8, 9}
```
Line 34 · formal-object · records projected-env-000397
```
		{
```
Line 35 · formal-object · records projected-env-000397
```
			\node (\x a) at (\x, 1) {\small{\x}};
```
Line 36 · formal-object · records projected-env-000397
```
			\node (\x b) at (\x, 2) {\small{\x}};
```
Line 37 · formal-object · records projected-env-000397
```
		}
```
Line 38 · formal-object · records projected-env-000397
```
		\node (dotsa) at (10, 1) {\small{\ldots}};
```
Line 39 · formal-object · records projected-env-000397
```
		\node (dotsb) at (10, 2) {\small{\ldots}};
```
Line 40 · formal-object · records projected-env-000397
```
		\draw[->] (1b)--(2a);
```
Line 41 · formal-object · records projected-env-000397
```
		\draw[->] (2b)--(3a);
```
Line 42 · formal-object · records projected-env-000397
```
		\draw[->] (3b)--(4a);
```
Line 43 · formal-object · records projected-env-000397
```
		\draw[->] (4b)--(5a);
```
Line 44 · formal-object · records projected-env-000397
```
		\draw[->] (5b)--(6a);
```
Line 45 · formal-object · records projected-env-000397
```
		\draw[->] (6b)--(7a);
```
Line 46 · formal-object · records projected-env-000397
```
		\draw[->] (7b)--(8a);
```
Line 47 · formal-object · records projected-env-000397
```
		\draw[->] (8b)--(9a);
```
Line 48 · formal-object · records projected-env-000397
```
		\draw[->] (9b)--(dotsa);
```
Line 49 · formal-object · records projected-env-000397
```
		\draw (1,1) circle (.4);
```
Line 50 · formal-object · records projected-env-000397
```
		\end{tikzpicture}
```
Line 52 · reference · records reference-000109
```
[citealt reference to EwaldSieg2013]
```
Line 58 · reference · records reference-000110
```
[citeyear reference to Dedekind1888]
```
Line 60 · formal-object, formula-context · records projected-env-000400 projected-formula-0002761
```
\begin{defn}\ollabel{defn:DedekindInfinite}
```
Line 61 · formal-object, formula, formula-context · records projected-env-000400 projected-formula-0002761 projected-formula-0002762 projected-formula-0002763 projected-formula-0002764
```
A set $A$ is \emph{Dedekind infinite} iff there is !!a{injection}
```
Line 62 · formal-object, formula, formula-context · records projected-env-000400 projected-formula-0002761 projected-formula-0002762 projected-formula-0002763 projected-formula-0002764 projected-formula-0002765 projected-formula-0002766
```
from~$A$ to a proper subset of~$A$. That is, there is some $o \in A$
```
Line 63 · formal-object, formula, formula-context · records projected-env-000400 projected-formula-0002762 projected-formula-0002763 projected-formula-0002764 projected-formula-0002765 projected-formula-0002766
```
and !!a{injection} $f \colon A \to A$ such that $o \notin \ran{f}$.
```
Line 64 · formal-object, formula-context · records projected-env-000400 projected-formula-0002765 projected-formula-0002766
```
\end{defn}
```

content/sets-functions-relations/infinite/dedekind-algebra.tex

77 exact source-coordinate anchors materialized from the accepted slice ledgers.

Line 10 · structure · records structure-00050
```
\olsection{Dedekind Algebras}
```
Line 19 · formula-context · records projected-formula-0002767
```
\begin{enumerate}
```
Line 20 · formula, formula-context · records projected-formula-0002767 projected-formula-0002768
```
	\item There is a number, $0$, which is not the successor of any number
```
Line 21 · formula, formula-context · records projected-formula-0002767 projected-formula-0002768 projected-formula-0002769
```
	\\i.e., $0 \notin \ran{s}$
```
Line 22 · formula, formula-context · records projected-formula-0002768 projected-formula-0002769
```
	\\i.e., $\forall x\ s(x) \neq 0$
```
Line 23 · formula-context · records projected-formula-0002769 projected-formula-0002770
```
	\item Distinct numbers have distinct successors 
```
Line 24 · formula, formula-context · records projected-formula-0002770 projected-formula-0002771
```
	\\i.e., $s$ is !!a{injection}
```
Line 25 · formula, formula-context · records projected-formula-0002770 projected-formula-0002771
```
	\\i.e., $\forall x \forall y (s(x) = s(y) \lif x = y)$
```
Line 26 · formula-context · records projected-formula-0002771 projected-formula-0002772
```
	\item\ollabel{repeatedapplication} Every number is obtained from
```

Line 27 · formula · records projected-formula-0002772

	$0$ by repeated applications of the successor function.

Line 28 · formula-context · records projected-formula-0002772
```
\end{enumerate}
```

Line 30 · reference · records reference-000111

[olref reference to sfr:infinite:dedekind:repeatedapplication]

Line 32 · reference · records reference-000112

[olref reference to sfr:infinite:dedekind:repeatedapplication]

Line 33 · formula-context · records projected-formula-0002773
```
\begin{enumerate}
```

Line 34 · formula · records projected-formula-0002773

	\item[3$'$.] The natural numbers are the smallest set that is

Line 35 · formula-context · records projected-formula-0002773 projected-formula-0002774
```
	\emph{closed under the successor function}: that is, if we apply
```

Line 36 · formula · records projected-formula-0002774

	$s$ to any !!{element} of the set, we obtain another !!{element}

Line 37 · formula-context · records projected-formula-0002774
```
	of the set.
```
Line 41 · formal-object, formula-context · records projected-env-000403 projected-formula-0002775 projected-formula-0002776 projected-formula-0002777
```
\begin{defn}\ollabel{Closure}
```
Line 42 · formal-object, formula, formula-context · records projected-env-000403 projected-formula-0002775 projected-formula-0002776 projected-formula-0002777 projected-formula-0002778 projected-formula-0002779
```
	For any function $f$, the set $X$ is $f$-\emph{closed} {iff}
```
Line 43 · formal-object, formula, formula-context · records projected-env-000403 projected-formula-0002775 projected-formula-0002776 projected-formula-0002777 projected-formula-0002778 projected-formula-0002779 projected-formula-0002780
```
	$(\forall x \in X)f(x) \in X$. Now define, for any $o$:
```
Line 44 · formal-object, formula, formula-context · records projected-env-000403 projected-formula-0002778 projected-formula-0002779 projected-formula-0002780
```
	$$\closureofunder{f}{o} = \bigcap\Setabs{X}{o \in X\text{ and }X
```
Line 45 · formal-object, formula-context · records projected-env-000403 projected-formula-0002780
```
\text{ is $f$-closed}}$$
```
Line 46 · formal-object · records projected-env-000403
```
\end{defn}
```
Line 48 · formula, formula-context · records projected-formula-0002781 projected-formula-0002782 projected-formula-0002783
```
So $\closureofunder{f}{o}$ is the intersection of all the $f$-closed
```
Line 49 · formula, formula-context · records projected-formula-0002781 projected-formula-0002782 projected-formula-0002783 projected-formula-0002784 projected-formula-0002785 projected-formula-0002786
```
sets with $o$ as !!a{element}. Intuitively, then,
```
Line 50 · formula, formula-context · records projected-formula-0002783 projected-formula-0002784 projected-formula-0002785 projected-formula-0002786
```
$\closureofunder{f}{o}$ is the \emph{smallest} $f$-closed set with $o$
```
Line 51 · formula-context · records projected-formula-0002784 projected-formula-0002785 projected-formula-0002786
```
as !!a{element}. This next result makes that intuitive thought
```
Line 53 · formal-object, formula-context · records projected-env-000405 projected-formula-0002787 projected-formula-0002788
```
\begin{lem}\ollabel{closureproperties}
```
Line 54 · formal-object, formula · records projected-env-000405 projected-formula-0002787 projected-formula-0002788
```
	For any function $f$ and any $o \in A$:
```
Line 55 · formal-object, formula-context · records projected-env-000405 projected-formula-0002787 projected-formula-0002788 projected-formula-0002789
```
	\begin{enumerate}
```
Line 56 · formal-object, formula, formula-context · records projected-env-000405 projected-formula-0002789 projected-formula-0002790 projected-formula-0002791
```
		\item\ollabel{closurehaselem} $o \in \closureofunder{f}{o}$; and
```
Line 57 · formal-object, formula, formula-context · records projected-env-000405 projected-formula-0002789 projected-formula-0002790 projected-formula-0002791 projected-formula-0002792 projected-formula-0002793 projected-formula-0002794
```
		\item\ollabel{closureclosed} $\closureofunder{f}{o}$ is $f$-closed; and
```
Line 58 · formal-object, formula, formula-context · records projected-env-000405 projected-formula-0002790 projected-formula-0002791 projected-formula-0002792 projected-formula-0002793 projected-formula-0002794 projected-formula-0002795
```
		\item\ollabel{closuresmallest} if $X$ is $f$-closed and $o \in
```
Line 59 · formal-object, formula, formula-context · records projected-env-000405 projected-formula-0002792 projected-formula-0002793 projected-formula-0002794 projected-formula-0002795
```
		X$, then $\closureofunder{f}{o} \subseteq X$
```
Line 60 · formal-object, formula-context · records projected-env-000405 projected-formula-0002795
```
	\end{enumerate}
```
Line 61 · formal-object · records projected-env-000405
```
\end{lem}
```
Line 63 · formula-context · records projected-formula-0002796 projected-formula-0002797 projected-formula-0002798
```
\begin{proof}
```
Line 64 · formula, formula-context · records projected-formula-0002796 projected-formula-0002797 projected-formula-0002798 projected-formula-0002799
```
Note that there is at least one $f$-closed set with $o$ as !!a{element}, namely $\ran{f}\cup
```
Line 65 · formula, formula-context · records projected-formula-0002796 projected-formula-0002797 projected-formula-0002798 projected-formula-0002799
```
\{o\}$. So $\closureofunder{f}{o}$, the intersection of \emph{all}
```
Line 66 · formula-context · records projected-formula-0002799
```
such sets, exists. We must now check
```

Line 67 · reference · records reference-000113 reference-000114

[olref reference to sfr:infinite:dedekind:closurehaselem]

[olref reference to sfr:infinite:dedekind:closuresmallest]

Line 69 · formula, formula-context, reference · records projected-formula-0002800 projected-formula-0002801 reference-000115

Concerning \olref{closurehaselem}: $o \in \closureofunder{f}{o}$ as it is an

[olref reference to sfr:infinite:dedekind:closurehaselem]

Line 70 · formula, formula-context · records projected-formula-0002800 projected-formula-0002801
```
intersection of sets which all have $o$ as !!a{element}. 
```
Line 72 · formula, formula-context, reference · records projected-formula-0002802 projected-formula-0002803 projected-formula-0002804 projected-formula-0002805 projected-formula-0002806 projected-formula-0002807 projected-formula-0002808 projected-formula-0002809 projected-formula-0002810 reference-000116
```
Concerning \olref{closureclosed}: suppose $x \in \closureofunder{f}{o}$. So if $o \in X$ and $X$ is $f$-closed, then $x \in X$, and now $f(x) \in X$ as $X$ is
```
```
[olref reference to sfr:infinite:dedekind:closureclosed]
```
Line 73 · formula, formula-context · records projected-formula-0002802 projected-formula-0002803 projected-formula-0002804 projected-formula-0002805 projected-formula-0002806 projected-formula-0002807 projected-formula-0002808 projected-formula-0002809 projected-formula-0002810
```
$f$-closed. So $f(x) \in \closureofunder{f}{o}$.
```
Line 75 · formula, formula-context, reference · records projected-formula-0002811 projected-formula-0002812 reference-000117
```
Concerning \olref{closuresmallest}: quite generally, if $X
```
```
[olref reference to sfr:infinite:dedekind:closuresmallest]
```
Line 76 · formula, formula-context · records projected-formula-0002811 projected-formula-0002812
```
\in C$ then $\bigcap C \subseteq X$.
```
Line 77 · formula-context · records projected-formula-0002812
```
\end{proof}
```
Line 81 · formal-object, formula-context · records projected-env-000408 projected-formula-0002813 projected-formula-0002814
```
\begin{defn}
```
Line 82 · formal-object, formula, formula-context · records projected-env-000408 projected-formula-0002813 projected-formula-0002814 projected-formula-0002815
```
A \emph{Dedekind algebra} is a set $A$ together with a function $f
```
Line 83 · formal-object, formula, formula-context · records projected-env-000408 projected-formula-0002813 projected-formula-0002814 projected-formula-0002815
```
\colon A \to A$ and some $o \in A$  such that:
```
Line 84 · formal-object, formula-context · records projected-env-000408 projected-formula-0002815 projected-formula-0002816
```
	\begin{enumerate}
```
Line 85 · formal-object, formula, formula-context · records projected-env-000408 projected-formula-0002816 projected-formula-0002817
```
		\item \ollabel{ded:proper} $o \notin \ran{f}$
```
Line 86 · formal-object, formula, formula-context · records projected-env-000408 projected-formula-0002816 projected-formula-0002817 projected-formula-0002818
```
		\item \ollabel{ded:injection} $f$ is !!a{injection}
```
Line 87 · formal-object, formula, formula-context · records projected-env-000408 projected-formula-0002817 projected-formula-0002818
```
		\item \ollabel{ded:closure} $A = \closureofunder{f}{o}$
```
Line 88 · formal-object, formula-context · records projected-env-000408 projected-formula-0002818
```
	\end{enumerate}
```
Line 89 · formal-object · records projected-env-000408
```
\end{defn}
```
Line 91 · formula, formula-context · records projected-formula-0002819 projected-formula-0002820 projected-formula-0002821 projected-formula-0002822
```
Since $A = \closureofunder{f}{o}$, our earlier result tells us that
```
Line 92 · formula, formula-context · records projected-formula-0002819 projected-formula-0002820 projected-formula-0002821 projected-formula-0002822
```
$A$ is the smallest $f$-closed set with $o$ as !!a{element}. Clearly a
```
Line 93 · formula-context · records projected-formula-0002820 projected-formula-0002821 projected-formula-0002822
```
Dedekind algebra is Dedekind infinite; just look at clauses
```

Line 94 · reference · records reference-000118 reference-000119

[olref reference to sfr:infinite:dedekind:ded:injection]

[olref reference to sfr:infinite:dedekind:ded:proper]

Line 98 · formal-object · records projected-env-000409
```
\begin{thm}\ollabel{thm:DedekindInfiniteAlgebra}
```

Line 99 · formal-object · records projected-env-000409

If there is a Dedekind infinite set, then there is a Dedekind algebra.

Line 100 · formal-object · records projected-env-000409
```
\end{thm}
```
Line 102 · formula-context · records projected-formula-0002823 projected-formula-0002824
```
\begin{proof}
```
Line 103 · formula, formula-context · records projected-formula-0002823 projected-formula-0002824 projected-formula-0002825 projected-formula-0002826
```
Let $D$ be Dedekind infinite. So there is an injection $g \colon D \to
```
Line 104 · formula, formula-context · records projected-formula-0002823 projected-formula-0002824 projected-formula-0002825 projected-formula-0002826 projected-formula-0002827 projected-formula-0002828 projected-formula-0002829
```
D$ and an element $o  \in D \setminus \ran{g}$. Now let $A =
```
Line 105 · formula, formula-context, reference · records projected-formula-0002825 projected-formula-0002826 projected-formula-0002827 projected-formula-0002828 projected-formula-0002829 projected-formula-0002830 reference-000120
```
[olref reference to sfr:infinite:dedekind:closureproperties]
```
```
\closureofunder{g}{o}$; by \olref{closureproperties}, $A$ exists and $o \in A$. Let $f =
```
Line 106 · formula, formula-context · records projected-formula-0002827 projected-formula-0002828 projected-formula-0002829 projected-formula-0002830
```
\funrestrictionto{g}{A}$. We will show that $A, f, o$ comprise a Dedekind
```
Line 107 · formula-context · records projected-formula-0002830
```
algebra. 
```
Line 109 · formula, formula-context, reference · records projected-formula-0002831 projected-formula-0002832 projected-formula-0002833 reference-000121
```
Concerning \olref{ded:proper}: $o \notin \ran{g}$ and $\ran{f}
```
```
[olref reference to sfr:infinite:dedekind:ded:proper]
```
Line 110 · formula, formula-context · records projected-formula-0002831 projected-formula-0002832 projected-formula-0002833
```
\subseteq \ran{g}$ so $o\notin \ran{f}$.
```
Line 112 · formula, reference · records projected-formula-0002834 projected-formula-0002835 projected-formula-0002836 reference-000122
```
Concerning \olref{ded:injection}: $g$ is an injection on $D$; so $f
```
```
[olref reference to sfr:infinite:dedekind:ded:injection]
```
Line 113 · formula-context · records projected-formula-0002834 projected-formula-0002835 projected-formula-0002836
```
\subseteq g$ must be an injection.
```

Line 115 · formula, reference · records projected-formula-0002837 projected-formula-0002838 projected-formula-0002839 projected-formula-0002840 projected-formula-0002841 projected-formula-0002842 projected-formula-0002843 projected-formula-0002844 projected-formula-0002845 projected-formula-0002846 projected-formula-0002847 reference-000123 reference-000124 reference-000125 reference-000126

Concerning \olref{ded:closure}: by \olref{closureproperties}, $A$ is $g$-closed; a fortiori, $A$ is $f$-closed. So $\closureofunder{f}{o} \subseteq A$ by \olref{closureproperties}. Since also $\closureofunder{f}{o}$ is $f$-closed and $f = \funrestrictionto{g}{A}$, it follows that $\closureofunder{f}{o}$ is $g$-closed. So $A \subseteq \closureofunder{f}{o}$ by \olref{closureproperties}.

[olref reference to sfr:infinite:dedekind:closureproperties]

[olref reference to sfr:infinite:dedekind:ded:closure]

Line 116 · formula-context · records projected-formula-0002837 projected-formula-0002838 projected-formula-0002839 projected-formula-0002840 projected-formula-0002841 projected-formula-0002842 projected-formula-0002843 projected-formula-0002844 projected-formula-0002845 projected-formula-0002846 projected-formula-0002847
```
\end{proof}
```

content/sets-functions-relations/infinite/dedekind-induction.tex

44 exact source-coordinate anchors materialized from the accepted slice ledgers.

Line 10 · structure · records structure-00051

\olsection{Dedekind Algebras and Arithmetical Induction}

Line 16 · formal-object, formula-context · records projected-env-000412 projected-formula-0002848 projected-formula-0002849
```
\begin{thm}[Arithmetical induction]\ollabel{thm:dedinfiniteinduction}
```
Line 17 · formal-object, formula · records projected-env-000412 projected-formula-0002848 projected-formula-0002849
```
Let $N, s, o$ comprise a Dedekind algebra. Then for any set $X$:  
```
Line 18 · formal-object, formula-context · records projected-env-000412 projected-formula-0002848 projected-formula-0002849 projected-formula-0002850 projected-formula-0002851 projected-formula-0002852
```
	\begin{center}
```
Line 19 · formal-object, formula · records projected-env-000412 projected-formula-0002850 projected-formula-0002851 projected-formula-0002852
```
		if $o \in X$ and $(\forall {n} \in N \cap X){s}({n}) \in X$, {then} $N \subseteq X$.
```
Line 20 · formal-object, formula-context · records projected-env-000412 projected-formula-0002850 projected-formula-0002851 projected-formula-0002852
```
	\end{center}
```
Line 21 · formal-object · records projected-env-000412
```
\end{thm}
```
Line 23 · formula-context · records projected-formula-0002853
```
\begin{proof}
```
Line 24 · formula, formula-context · records projected-formula-0002853 projected-formula-0002854 projected-formula-0002855
```
By the definition of a Dedekind algebra, $N = \closureofunder{s}{o}$.
```
Line 25 · formula, formula-context · records projected-formula-0002853 projected-formula-0002854 projected-formula-0002855 projected-formula-0002856
```
Now if both ${o} \in X$ and $(\forall {n} \in N)(n \in X \lif
```
Line 26 · formula, formula-context · records projected-formula-0002854 projected-formula-0002855 projected-formula-0002856
```
{s}({n}) \in X)$, then $N = \closureofunder{s}{o} \subseteq X$.
```
Line 27 · formula-context · records projected-formula-0002856
```
\end{proof}
```

Line 33 · reference · records reference-000127

[olref reference to sfr:infinite:induction:thm:dedinfiniteinduction]

Line 37 · formal-object, formula-context · records projected-env-000415 projected-formula-0002857
```
\begin{cor}\ollabel{natinductionschema}
```
Line 38 · formal-object, formula, formula-context · records projected-env-000415 projected-formula-0002857 projected-formula-0002858
```
Let $N, s, o$ comprise a Dedekind algebra. Then for any formula
```
Line 39 · formal-object, formula, formula-context · records projected-env-000415 projected-formula-0002857 projected-formula-0002858
```
$\phi(x)$, which may have parameters:
```
Line 40 · formal-object, formula-context · records projected-env-000415 projected-formula-0002858 projected-formula-0002859 projected-formula-0002860
```
\begin{center}
```
Line 41 · formal-object, formula, formula-context · records projected-env-000415 projected-formula-0002859 projected-formula-0002860 projected-formula-0002861
```
	if $\phi(o)$ and $(\forall {n} \in N)(\phi(n)\lif
```
Line 42 · formal-object, formula, formula-context · records projected-env-000415 projected-formula-0002859 projected-formula-0002860 projected-formula-0002861
```
	\phi({s}({n})))$, {then} $(\forall n \in N)\phi(n)$
```
Line 43 · formal-object, formula-context · records projected-env-000415 projected-formula-0002861
```
\end{center}
```
Line 44 · formal-object · records projected-env-000415
```
\end{cor}
```
Line 46 · formula-context · records projected-formula-0002862
```
\begin{proof}
```
Line 47 · formula · records projected-formula-0002862
```
Let $X = \Setabs{n \in N}{\phi(n)}$, and now use
```

Line 48 · formula-context, reference · records projected-formula-0002862 reference-000128

[olref reference to sfr:infinite:induction:thm:dedinfiniteinduction]

\olref{thm:dedinfiniteinduction}

Line 51 · formula-context · records projected-formula-0002863

In this result, we spoke of a formula ``having parameters''. What this

Line 52 · formula, formula-context · records projected-formula-0002863 projected-formula-0002864
```
means, roughly, is that for any objects $c_1, \ldots, c_k$, we can
```
Line 53 · formula, formula-context · records projected-formula-0002863 projected-formula-0002864
```
work with $\phi(x, c_1, \ldots, c_k)$. More precisely, we can state
```
Line 54 · formula-context · records projected-formula-0002864 projected-formula-0002865
```
the result without mentioning ``parameters'' as follows. For any
```

Line 55 · formula · records projected-formula-0002865

formula $\phi(x, v_1, \ldots, v_k)$, whose free variables are all

Line 56 · formula-context · records projected-formula-0002865 projected-formula-0002866
```
displayed, we have:
```
Line 57 · formal-object, formula · records projected-env-000417 projected-formula-0002866
```
	\begin{align*}
```
Line 58 · formal-object, formula-context · records projected-env-000417 projected-formula-0002866
```
			\forall v_1 \ldots \forall v_k((&\phi(o, v_1,\ldots, v_k) \land {}\\
```

Line 59 · formal-object · records projected-env-000417

			&	(\forall x \in N)(\phi(x,v_1, \ldots, v_k) \lif \phi(s(x), v_1,\ldots, v_k))) \lif {}\\

Line 60 · formal-object · records projected-env-000417

			&\hspace{3em} (\forall x \in N)\phi(x, v_1,\ldots, v_k))

Line 61 · formal-object · records projected-env-000417
```
	\end{align*}
```
Line 63 · reference · records reference-000129
```
[olref reference to sth:::part]
```

Line 72 · formula-context, reference · records projected-formula-0002867 reference-000130

[olref reference to sth:ord-arithmetic::chap]

after \olref[sth][ord-arithmetic][]{chap}, or perhaps read an alternative

Line 73 · formula, reference · records projected-formula-0002867 reference-000131

[citealt reference to Potter2004]

treatment, such as \citealt[pp.~95--8]{Potter2004}.) But, where $N, s, o$

Line 74 · formula-context · records projected-formula-0002867

comprise a Dedekind algebra, we will ultimately be able to stipulate the

Line 75 · formula-context · records projected-formula-0002868
```
following:
```
Line 76 · formal-object, formula · records projected-env-000418 projected-formula-0002868
```
\begin{align*}
```
Line 77 · formal-object, formula-context · records projected-env-000418 projected-formula-0002868
```
	{a} + {o} &= {a} & & & {a} \times {o} &= {o} & & & {a}^{o} &= s(o)\\
```

Line 78 · formal-object · records projected-env-000418

{a} + {s}({b}) &= {s}({a}+{b}) &&& {a} \times {s}({b}) &= ({a}\times {b}) + {a}  & & & {a}^{{s}({b})} &= {a}^{b} \times {a}

Line 79 · formal-object · records projected-env-000418
```
\end{align*}
```

content/sets-functions-relations/infinite/dedekinds-proof.tex

26 exact source-coordinate anchors materialized from the accepted slice ledgers.

Line 11 · structure · records structure-00052

\olsection{Dedekind's ``Proof'' of the 
Existence of an Infinite Set}

Line 16 · reference · records reference-000132
```
[olref reference to sfr:arith:ref:sec]
```
Line 21 · reference · records reference-000133
```
[olref reference to sfr:arith::chap]
```

Line 25 · formula-context · records projected-formula-0002869

\emph{given any Dedekind infinite set}, we can define a set which will

Line 26 · formula · records projected-formula-0002869
```
behave just like we want~$\Nat$ to behave. 
```
Line 30 · reference · records reference-000134
```
[olref reference to sfr:arith:ref:sec]
```

Line 31 · formula-context · records projected-formula-0002870

emphasized that we would be wrong to think of the definition of

Line 32 · formula · records projected-formula-0002870

$\Real$ as the set of Dedekind cuts as a \emph{discovery}, rather than

Line 33 · formula-context · records projected-formula-0002870

a convenient stipulation. The crucial observation is that the Dedekind

Line 38 · reference · records reference-000135
```
[citeyear reference to Dedekind1888]
```
Line 57 · reference · records reference-000136
```
[citep reference to Dedekind1888]
```
Line 61 · reference · records reference-000137
```
[olref reference to sfr:arith::chap]
```

Line 69 · reference · records reference-000138

[olref reference to sfr:infinite:dedekind:thm:DedekindInfiniteAlgebra]

Line 75 · formula-context · records projected-formula-0002871
```
\begin{quote}
```
Line 76 · formula, formula-context · records projected-formula-0002871 projected-formula-0002872
```
  My own realm of thoughts, i.e., the totality $S$ of all things which
```
Line 77 · formula, formula-context · records projected-formula-0002871 projected-formula-0002872 projected-formula-0002873 projected-formula-0002874 projected-formula-0002875
```
  can be objects of my thought, is infinite. For if $s$ signifies an
```
Line 78 · formula, formula-context · records projected-formula-0002872 projected-formula-0002873 projected-formula-0002874 projected-formula-0002875 projected-formula-0002876
```
  element of~$S$, then the thought $s'$ that~$s$ can be an object of
```
Line 79 · formula, formula-context · records projected-formula-0002873 projected-formula-0002874 projected-formula-0002875 projected-formula-0002876 projected-formula-0002877 projected-formula-0002878 projected-formula-0002879
```
  my thought, is itself an element of~$S$. If we regard this as an
```
Line 80 · formula, formula-context · records projected-formula-0002876 projected-formula-0002877 projected-formula-0002878 projected-formula-0002879
```
  image $\phi(s)$ of the element~$s$, then \dots~$S$ is [Dedekind]
```
Line 81 · formula-context · records projected-formula-0002877 projected-formula-0002878 projected-formula-0002879
```
  infinite, which was to be proved.
```
Line 82 · reference · records reference-000139
```
[citep reference to Dedekind1888]
```

Line 95 · formula-context · records projected-formula-0002880

many things (specifically, infinitely many thoughts). But Dedekind

Line 96 · formula, formula-context · records projected-formula-0002880 projected-formula-0002881
```
also needs to give us a reason to regard~$S$ as a single \emph{set},
```
Line 97 · formula, formula-context · records projected-formula-0002880 projected-formula-0002881
```
with infinitely many !!{element}s, rather than thinking of~$S$ as
```
Line 98 · formula-context · records projected-formula-0002881
```
\emph{some things} (in the plural). 
```
Line 103 · reference · records reference-000140
```
[citet reference to Potter2004]
```

content/sets-functions-relations/infinite/card-sb.tex

67 exact source-coordinate anchors materialized from the accepted slice ledgers.

Line 7 · structure · records structure-00053

\olsection{Appendix: Proving Schr\"oder-Bernstein}

Line 11 · formula-context, reference · records projected-formula-0002882 projected-formula-0002883 projected-formula-0002884 reference-000141
```
Schr\"oder-Bernstein (\olref[sfr][siz][sb]{thm:schroder-bernstein}): if
```
```
[olref reference to sfr:siz:sb:thm:schroder-bernstein]
```
Line 12 · formula, formula-context · records projected-formula-0002882 projected-formula-0002883 projected-formula-0002884 projected-formula-0002885 projected-formula-0002886
```
$\cardle{A}{B}$ and $\cardle{B}{A}$ then $\cardeq{A}{B}$; i.e., given
```
Line 13 · formula, formula-context · records projected-formula-0002882 projected-formula-0002883 projected-formula-0002884 projected-formula-0002885 projected-formula-0002886 projected-formula-0002887
```
!!{injection}s $f \colon A \to B$ and $g \colon B \to A$ there is
```
Line 14 · formula, formula-context · records projected-formula-0002885 projected-formula-0002886 projected-formula-0002887
```
!!a{bijection} $h \colon A \to B$. 
```
Line 19 · reference · records reference-000142
```
[citet reference to Potter2004]
```

Line 21 · formula-context · records projected-formula-0002888

you that this is a theorem---rather like the irrationality of

Line 22 · formula · records projected-formula-0002888

$\sqrt{2}$---for which \emph{many} interesting and different proofs

Line 23 · formula-context · records projected-formula-0002888
```
exist.
```

Line 25 · reference · records reference-000143

[olref reference to sfr:infinite:dedekind:Closure]

Line 26 · formula-context · records projected-formula-0002889
```
let
```
Line 27 · formula · records projected-formula-0002889
```
\[
```
Line 28 · formula-context · records projected-formula-0002889
```
\Closureofunder{f}{B} = \bigcap \Setabs{X}{B \subseteq X 
```
Line 30 · formula-context · records projected-formula-0002890 projected-formula-0002891
```
\]
```
Line 31 · formula, formula-context · records projected-formula-0002890 projected-formula-0002891 projected-formula-0002892 projected-formula-0002893 projected-formula-0002894
```
for each set $B$ and function~$f$. Defined thus,
```
Line 32 · formula, formula-context · records projected-formula-0002890 projected-formula-0002891 projected-formula-0002892 projected-formula-0002893 projected-formula-0002894
```
$\Closureofunder{f}{B}$ is the smallest $f$-closed set containing~$B$,
```
Line 33 · formula-context · records projected-formula-0002892 projected-formula-0002893 projected-formula-0002894
```
in that:
```
Line 35 · formal-object, formula-context · records projected-env-000422 projected-formula-0002895 projected-formula-0002896
```
\begin{lem}\ollabel{Closureprops}
```
Line 36 · formal-object, formula · records projected-env-000422 projected-formula-0002895 projected-formula-0002896
```
	For any function $f$, and any $B$:
```
Line 37 · formal-object, formula-context · records projected-env-000422 projected-formula-0002895 projected-formula-0002896 projected-formula-0002897
```
	\begin{enumerate}
```
Line 38 · formal-object, formula, formula-context · records projected-env-000422 projected-formula-0002897 projected-formula-0002898 projected-formula-0002899
```
		\item\ollabel{Closurehaselem} $B \subseteq \Closureofunder{f}{B}$; and
```
Line 39 · formal-object, formula, formula-context · records projected-env-000422 projected-formula-0002897 projected-formula-0002898 projected-formula-0002899 projected-formula-0002900 projected-formula-0002901 projected-formula-0002902
```
		\item\ollabel{Closureclosed} $\Closureofunder{f}{B}$ is $f$-closed; and
```
Line 40 · formal-object, formula, formula-context · records projected-env-000422 projected-formula-0002898 projected-formula-0002899 projected-formula-0002900 projected-formula-0002901 projected-formula-0002902 projected-formula-0002903
```
		\item\ollabel{Closuresmallest} if $X$ is $f$-closed and $B
```
Line 41 · formal-object, formula, formula-context · records projected-env-000422 projected-formula-0002900 projected-formula-0002901 projected-formula-0002902 projected-formula-0002903
```
		\subseteq X$, then $\Closureofunder{f}{B} \subseteq X$.
```
Line 42 · formal-object, formula-context · records projected-env-000422 projected-formula-0002903
```
	\end{enumerate}
```
Line 43 · formal-object · records projected-env-000422
```
\end{lem}
```

Line 46 · reference · records reference-000144

[olref reference to sfr:infinite:dedekind:closureproperties]

Line 51 · formal-object, formula-context · records projected-env-000424 projected-formula-0002904 projected-formula-0002905 projected-formula-0002906
```
\begin{prop}\ollabel{sbhelper}
```
Line 52 · formal-object, formula, source-correction · records TR007-SOURCE-FORMULA-002 projected-env-000424 projected-formula-0002904 projected-formula-0002905 projected-formula-0002906
```
If $A \subseteq B \subseteq C$ and $A \approx C$, then $\cardeq{\cardeq{A}{B}}{C}$.
```
Line 53 · formal-object, formula-context · records projected-env-000424 projected-formula-0002904 projected-formula-0002905 projected-formula-0002906
```
\end{prop}
```
Line 55 · formula-context · records projected-formula-0002907 projected-formula-0002908
```
\begin{proof}
```
Line 56 · formula, formula-context · records projected-formula-0002907 projected-formula-0002908 projected-formula-0002909
```
Given !!a{bijection}  $f \colon C \to A$, let $F =
```
Line 57 · formula, formula-context · records projected-formula-0002907 projected-formula-0002908 projected-formula-0002909 projected-formula-0002910
```
\Closureofunder{f}{C \setminus B}$ and define a function $g$ with
```
Line 58 · formula, formula-context · records projected-formula-0002909 projected-formula-0002910 projected-formula-0002911
```
domain $C$ as follows:
```
Line 59 · formula, formula-context · records projected-formula-0002910 projected-formula-0002911
```
\[
```
Line 60 · formula-context · records projected-formula-0002911
```
	g(x) = 
```
Line 65 · formula-context · records projected-formula-0002912 projected-formula-0002913
```
\]
```
Line 66 · formula, formula-context · records projected-formula-0002912 projected-formula-0002913 projected-formula-0002914
```
We'll show that $g$ is !!a{bijection} from $C \to B$, from which it
```
Line 67 · formula, formula-context · records projected-formula-0002912 projected-formula-0002913 projected-formula-0002914
```
will follow that $\comp{f^{-1}}{g} \colon A \to B$ is !!a{bijection},
```
Line 68 · formula-context · records projected-formula-0002914
```
completing the proof.
```
Line 70 · formula, formula-context · records projected-formula-0002915 projected-formula-0002916 projected-formula-0002917 projected-formula-0002918
```
First we claim that if $x \in F$ but $y\notin F$ then $g(x) \neq
```
Line 71 · formula, formula-context · records projected-formula-0002915 projected-formula-0002916 projected-formula-0002917 projected-formula-0002918 projected-formula-0002919 projected-formula-0002920 projected-formula-0002921
```
g(y)$. For reductio suppose otherwise, so that $y = g(y) = g(x) =
```
Line 72 · formula, formula-context, reference · records projected-formula-0002918 projected-formula-0002919 projected-formula-0002920 projected-formula-0002921 projected-formula-0002922 reference-000145
```
[olref reference to sfr:infinite:card-sb:Closureprops]
```
```
f(x)$. Since $x \in F$ and $F$ is $f$-closed by \olref{Closureprops},
```
Line 73 · formula, formula-context · records projected-formula-0002919 projected-formula-0002920 projected-formula-0002921 projected-formula-0002922
```
we have $y = f(x) \in F$, a contradiction. 
```
Line 75 · formula, formula-context · records projected-formula-0002923 projected-formula-0002924 projected-formula-0002925 projected-formula-0002926 projected-formula-0002927 projected-formula-0002928
```
Now suppose $g(x) = g(y)$. So, by the above, $x \in F$ iff $y \in F$.
```
Line 76 · formula, formula-context · records projected-formula-0002923 projected-formula-0002924 projected-formula-0002925 projected-formula-0002926 projected-formula-0002927 projected-formula-0002928 projected-formula-0002929 projected-formula-0002930 projected-formula-0002931
```
If $x, y \in F$, then $f(x) = g (x) = g(y) = f(y)$ so that $x = y$
```
Line 77 · formula, formula-context · records projected-formula-0002926 projected-formula-0002927 projected-formula-0002928 projected-formula-0002929 projected-formula-0002930 projected-formula-0002931 projected-formula-0002932
```
since $f$ is !!a{bijection}. If  $x, y \notin F$, then $x = g(x) =
```
Line 78 · formula, formula-context · records projected-formula-0002929 projected-formula-0002930 projected-formula-0002931 projected-formula-0002932
```
g(y) = y$. So $g$ is !!a{injection}.
```
Line 80 · formula, formula-context · records projected-formula-0002933 projected-formula-0002934 projected-formula-0002935 projected-formula-0002936 projected-formula-0002937 projected-formula-0002938
```
It remains to show that $\ran{g} = B$. So fix $x \in B \subseteq C$.
```
Line 81 · formula, formula-context · records projected-formula-0002933 projected-formula-0002934 projected-formula-0002935 projected-formula-0002936 projected-formula-0002937 projected-formula-0002938 projected-formula-0002939 projected-formula-0002940 projected-formula-0002941 projected-formula-0002942 projected-formula-0002943
```
If $x \notin F$, then $g(x) = x$. If $x \in F$, then $x = f(y)$ for
```
Line 82 · formula, formula-context, reference · records projected-formula-0002935 projected-formula-0002936 projected-formula-0002937 projected-formula-0002938 projected-formula-0002939 projected-formula-0002940 projected-formula-0002941 projected-formula-0002942 projected-formula-0002943 reference-000146
```
[olref reference to sfr:infinite:card-sb:Closureprops]
```
```
some $y \in F$, since otherwise $F \setminus \{x\}$ would be $f$-closed and extend $C\setminus B$, which is impossible by \olref{Closureprops}; now $g(y) = f(y) = x$.
```
Line 83 · formula-context · records projected-formula-0002939 projected-formula-0002940 projected-formula-0002941 projected-formula-0002942 projected-formula-0002943
```
\end{proof}
```
Line 85 · formula-context · records projected-formula-0002944 projected-formula-0002945 projected-formula-0002946
```
Finally, here is the proof of the main result. Recall that given a
```
Line 86 · formula · records projected-formula-0002944 projected-formula-0002945 projected-formula-0002946
```
function $h$ and set $D$, we define $\funimage{h}{D} = \Setabs{h(x)}{x
```
Line 87 · formula-context · records projected-formula-0002944 projected-formula-0002945 projected-formula-0002946
```
\in D}$. 
```
Line 89 · formula, formula-context · records projected-formula-0002947 projected-formula-0002948 projected-formula-0002949
```
\begin{proof}[Proof of Schr\"oder-Bernstein] Let $f \colon A \to B$
```
Line 90 · formula, formula-context · records projected-formula-0002947 projected-formula-0002948 projected-formula-0002949 projected-formula-0002950
```
and $g \colon B \to A$ be !!{injection}s. Since $\funimage{f}{A}
```
Line 91 · formula, formula-context · records projected-formula-0002948 projected-formula-0002949 projected-formula-0002950 projected-formula-0002951
```
\subseteq B$ we have that $\funimage{g}{\funimage{f}{A}} \subseteq
```
Line 92 · formula, formula-context · records projected-formula-0002950 projected-formula-0002951 projected-formula-0002952
```
g[B] \subseteq A$. Also, $\comp{f}{g} \colon A \to
```
Line 93 · formula, formula-context · records projected-formula-0002951 projected-formula-0002952 projected-formula-0002953 projected-formula-0002954
```
\funimage{g}{\funimage{f}{A}}$ is an !!{injection} since both $g$ and
```
Line 94 · formula, formula-context · records projected-formula-0002952 projected-formula-0002953 projected-formula-0002954
```
$f$ are; and indeed $\comp{f}{g}$ is !!a{bijection}, just by the way
```
Line 95 · formula-context · records projected-formula-0002953 projected-formula-0002954 projected-formula-0002955
```
we defined its codomain. So
```
Line 96 · formula, formula-context · records projected-formula-0002955 projected-formula-0002956
```
$\cardeq{\funimage{g}{\funimage{f}{A}}}{A}$, and hence by
```
Line 97 · formula, formula-context, reference · records projected-formula-0002955 projected-formula-0002956 projected-formula-0002957 reference-000147
```
[olref reference to sfr:infinite:card-sb:sbhelper]
```
```
\olref{sbhelper} there is !!a{bijection} $h \colon A \to
```
Line 98 · formula, formula-context · records projected-formula-0002956 projected-formula-0002957 projected-formula-0002958 projected-formula-0002959
```
\funimage{g}{B}$. Moreover, $g^{-1}$ is !!a{bijection}
```
Line 99 · formula, formula-context · records projected-formula-0002957 projected-formula-0002958 projected-formula-0002959
```
$\funimage{g}{B} \to B$. So $\comp{h}{g^{-1}} \colon A \to B$ is
```
Line 100 · formula-context · records projected-formula-0002958 projected-formula-0002959
```
!!a{bijection}. 
```

content/sets-functions-relations/sets-functions-relations-complete.tex

0 exact source-coordinate anchors materialized from the accepted slice ledgers.