Zermelo-Fraenkel set theory
Zermelo-Fraenkel set theory, or $ZF$, is a first-order theory, in which objects represented by variable symbols are called
sets.
$ZF$ is constructed from the following signature and axioms:
- Signature
Two binary predicate symbols: Equality $=$ and Membership $\in$.
- Axioms
By default, let $a,b,c,s,u,x,y,z,F,S,X,Y$ be any distinct variable symbols.
- $ZF1$. Axiom of extensionality. if $X$ and $Y$ contain the same elements, then $X$ and $Y$ are equal.
$$\forall X\forall Y(\forall u((u\in X)\leftrightarrow(u\in Y))\to(X=Y))$$
- $ZF2$. Axiom of pairing. For any $a$ and $b$, there exists a set that contains exactly a and b.
$$\forall a\forall b\exists c\forall x((x\in c)\leftrightarrow((x=a)\lor (x=b)))$$
- $ZF3$. Axiom schema of specification. For any natural number $n$, let $X, Y, u, w_1, \ldots, w_n$ be any distinct variable symbols,
and let $\varphi$ be any formula with free variables among $X, u, w_1, \ldots, w_n$.
Given any arguments $w_1, \ldots, w_n$ and any set $X$, there exists a set $Y$ that contains
exactly all members of $X$ that have the property represented by $\varphi$.
$$\forall w_1\ldots\forall w_n\forall X\exists Y\forall u((u\in Y)\leftrightarrow((u\in X)\land\varphi))$$
- $ZF4$. Axiom of union. For any $X$ there exists a set $Y$ that is the union of all elements of $X$.
$$\forall X\exists Y\forall u((u\in Y)\leftrightarrow\exists x((x\in X)\land(u\in x)))$$
- $ZF5$. Axiom of power set. For any $X$ there exists a set $Y$ that contains exactly all subsets of $X$.
$$\forall X\exists Y\forall y((y\in Y)\leftrightarrow\forall x((x\in y)\to(x\in X)))$$
- $ZF6$. Axiom of infinity. There exists an infinite set $S$ that contains the empty set and for every $x$ in $S$, the successor of $x$ is also in $S$.
$$\exists S(\forall z(\forall y\neg(y\in z)\to(z\in S))\land\forall x((x\in S)\to
\forall X(\forall u((u\in X)\leftrightarrow((u\in x)\lor(u=x)))\to(X\in S))))$$
- $ZF7$. Axiom schema of replacement. For any natural number $n$, let $X, Y, x, y, w_1, \ldots, w_n$ be any distinct variable symbols,
and let $\varphi$ be any formula with free variables among $X, x, y, w_1, \ldots, w_n$.
Given any arguments $w_1, \ldots, w_n$ and any set $X$, if $\varphi$ defines a function from $X$,
then there exists a set $Y$ that can be taken as the codomain of the function.
$$\forall w_1\ldots\forall w_n\forall X(\forall x((x\in X)\to\exists!y\varphi)\to\exists Y\forall x((x\in X)\to\exists y((y\in Y)\land\varphi)))$$
- $ZF8$. Axiom of foundation. Every non-empty set $S$ contains an element that is disjoint from $S$.
$$\forall S(\exists x(x\in S)\to\exists s((s\in S)\land\neg\exists y((y\in S)\land(y\in s))))$$
Zermelo-Fraenkel set theory with axiom of choice, or $ZFC$, is $ZF$ extended by the following non-logical axiom (we use the same notations as above):
- $ZF9$. Axiom of choice. Given any family $F$ of pairwise disjoint non-empty sets,
there exists a set $S$ that contains exactly one element in common with each of the sets in $F$.
$$\forall F((\forall X((X\in F)\to\exists x(x\in X))\land
\forall X\forall Y(((X\in F)\land(Y\in F))\to(\exists u((u\in X)\land(u\in Y))\to(X=Y))))\to
\exists S\forall X((X\in F)\to\exists!x((x\in S)\land(x\in X))))$$
ZFW
We will use the witness-complete extension of $ZF$, called $ZFW$, as our foundation.
Note.
Note that, the concept of sets is purely semantic.
Syntactically, sets are represented by terms, instead of just variable symbols.
A witness with its arguments together represents a set.
Note.
Form this point on:
- by default, we work on $ZFW$;
- by default, distinct notations of variable symbols represent arbitrary distinct variable symbols;
- we may not state the nature of a notation if it is obvious;
- we may omit parentheses if the resulting notations are unambiguous;
- when we introduce new variable symbols, unless otherwise specified, we implicitly assume that they are chosen to not occur in anything already introduced;
- in general, any unintended collision of variable symbols should be implicitly avoided by replacement of quantifiers and bounded variables with new variable symbols,
and/or generalization and instantiation on free variables with new variable symbols;
- we may use notations like $\varphi(x_1,\ldots,x_n)$ for formulas or $y(x_1,\ldots,x_n)$ for terms to emphasize on the variable symbols $x_1,\ldots,x_n$, which may or may not occur as free variables,
and given terms $t_1,\ldots,t_n$, we may denote $\varphi[t_1/x_1]\ldots[t_n/x_n]$ as $\varphi(t_1,\ldots,t_n)$ and $y[t_1/x_1]\ldots[t_n/x_n]$ as $y(t_1,\ldots,t_n)$;
- when we say "there exists $x$ such that $\varphi$", we may implicitly use the same notation $x$ to represent a witness with arguments of the statement;
- we may use the notation $\{u\subseteq X|\varphi\}$ in place of $\{u\in\mathcal P(X)|\varphi\}$;
- we may use the notation $\forall x_1,\ldots,x_n\in X\varphi$ in place of $\forall x_1\ldots\forall x_n(((x_1\in X)\land\ldots\land(x_n\in X))\to\varphi)$;
- we may use the notation $\exists x_1,\ldots,x_n\in X\varphi$ in place of $\exists x_1\ldots\exists x_n(((x_1\in X)\land\ldots\land(x_n\in X))\land\varphi)$;
- we will allow various notations of quantifiers, if unambiguous.
Notation.
Let $t_1,t_2$ be arbitrary terms, let $x$ be a variable symbol not occurring in $t_1,t_2$,
we will use the following notations:
- non-equality: we use $(t_1\neq t_2)$ to denote $\neg(t_1=t_2)$
- non-membership: we use $(t_1\notin t_2)$ to denote $\neg(t_1\in t_2)$
- subset: we use $(t_1\subseteq t_2)$ to denote $\forall x((x\in t_1)\to(x\in t_2))$
- proper subset: we use $(t_1\subset t_2)$ to denote $((t_1\subseteq t_2)\land\neg(t_2\subseteq t_1))$
Definition.
We say $t_1$ is a superset of $t_2$ if and only if $t_2$ is a subset of $t_1$.
Empty set
There exists a unique set that contains no sets
(show proof).
Proof.
The formula we are trying to prove is $\exists!X\forall u\neg(u\in X)$.
We will be skipping obvious steps in this proof.
$$
\begin{matrix}
1 & \forall w_1\forall X\exists Y\forall u((u\in Y)\leftrightarrow((u\in X)\land\neg(w_1=w_1))) & ZF3 \\
2 & \exists Y\forall u((u\in Y)\leftrightarrow((u\in X)\land\neg(w_1=w_1))) \\
3 & \forall u((u\in f(w_1,X))\leftrightarrow((u\in X)\land\neg(w_1=w_1))) & \text{Witness }f \\
4 & ((u\in f(w_1,X))\leftrightarrow((u\in X)\land\neg(w_1=w_1))) \\
5 & (w_1=w_1) \\
6 & \neg((u\in X)\land\neg(w_1=w_1)) \\
7 & \neg(u\in f(w_1,X)) & \text{From }4,6 \\
8 & \forall u\neg(u\in f(w_1,X)) \\
9 & \exists X\forall u\neg(u\in X) \\
10 & \forall u\neg(u\in\mathcal E) & \text{Witness }\mathcal E \\
11 & \neg(u\in\mathcal E) \\
12 & \forall X\forall Y(\forall u((u\in X)\leftrightarrow(u\in Y))\to(X=Y)) & ZF1 \\
13 & (\forall u((u\in\mathcal E)\leftrightarrow(u\in Y))\to(\mathcal E=Y)) \\
14 & \forall u((\neg(u\in\mathcal E)\land\neg(u\in Y))\to((u\in\mathcal E)\leftrightarrow(u\in Y))) & \text{Tautology} \\
15 & (\forall u(\neg(u\in\mathcal E)\land\neg(u\in Y))\to\forall u((u\in\mathcal E)\leftrightarrow(u\in Y))) \\
16 & (\neg(u\in\mathcal E)\to(\neg(u\in Y)\to(\neg(u\in\mathcal E)\land\neg(u\in Y)))) & \text{Tautology} \\
17 & (\neg(u\in Y)\to(\neg(u\in\mathcal E)\land\neg(u\in Y))) & \text{From }11,16 \\
18 & \forall u(\neg(u\in Y)\to(\neg(u\in\mathcal E)\land\neg(u\in Y))) \\
19 & (\forall u\neg(u\in Y)\to\forall u(\neg(u\in\mathcal E)\land\neg(u\in Y))) \\
20 & (\forall u\neg(u\in Y)\to(\mathcal E=Y)) & \text{From }13,15,19 \\
21 & ((\mathcal E=Y)\to(\forall u\neg(u\in\mathcal E)\to\forall u\neg(u\in Y))) \\
22 & ((\forall u\neg(u\in\mathcal E)\land((\mathcal E=Y)\to(\forall u\neg(u\in\mathcal E)\to\forall u\neg(u\in Y))))\to((\mathcal E=Y)\to\forall u\neg(u\in Y))) & \text{Tautology} \\
23 & (\forall u\neg(u\in\mathcal E)\land((\mathcal E=Y)\to(\forall u\neg(u\in\mathcal E)\to\forall u\neg(u\in Y)))) & \text{From }10,21 \\
24 & ((\mathcal E=Y)\to\forall u\neg(u\in Y)) & \text{From }22,23 \\
25 & (\forall u\neg(u\in Y)\leftrightarrow(\mathcal E=Y)) & \text{From }20,24 \\
26 & \forall Y(\forall u\neg(u\in Y)\leftrightarrow(\mathcal E=Y)) \\
27 & \exists X\forall Y(\forall u\neg(u\in Y)\leftrightarrow(X=Y)) \\
28 & \exists!X\forall u\neg(u\in X)
\end{matrix}
$$
We call this set emptyset and denote it as $\emptyset$.
Note.
From this point on, we will not use formal proofs to prove theorems.
Instead, we will use meta-logical style reasoning, but the underlying logic
is justifiable within $ZFW$.
Proposition.
Equal sets contain the same elements.
(show proof)
Proof.
Suppose $x=y$. Since we have $(u\in x)\leftrightarrow(u\in x)$, by $LA6$, we have $(u\in x)\leftrightarrow(u\in y)$.
Thus $(x=y)\to\forall u((u\in x)\leftrightarrow(u\in y))$ and hence $\forall x\forall y((x=y)\to\forall u((u\in x)\leftrightarrow(u\in y)))$.
Note.
Combining axiom of extensionality and the above proposition, two sets are equal if and only if they contain the same elements.
Proposition.
Equal sets must simultaneously belong or not belong to a set.
(show proof)
Proof.
Suppose $a=b$. Note that either $a\in X$ or $a\notin X$, thus either $(a\in X)\land(a=b)$ or $(a\notin X)\land(a=b)$.
If $(a\in X)\land(a=b)$, then $b\in X$, thus $(a\in X)\leftrightarrow(b\in X)$.
If $(a\notin X)\land(a=b)$, then $b\notin X$, thus $(a\in X)\leftrightarrow(b\in X)$.
Hence $(a=b)\to((a\in X)\leftrightarrow(b\in X))$, and we have $\forall a\forall b((a=b)\to\forall X((a\in X)\leftrightarrow(b\in X)))$.
$\blacksquare$
Set-builder notation
Let $n$ be a meta-logical natural number.
let $\varphi$ be a formula with free variables among $X,u,w_1,\ldots,w_n$.
Then by axiom schema of specification, there exists, and thus uniquely exists, a set $Y$ such that a set $u$ is in $Y$ if and only if $u$ is in $X$ and $\varphi$ is satisfied.
We will denote the set $Y$ as $$\{u\in X|\varphi\}$$
Enumeration notation
Let $n$ be a meta-logical natural number.
Given sets $x_1,\ldots,x_n$, there exists a unique set $X$ such that a set $u$ is in $X$ if and only if $u$ is equal to one of $x_1,\ldots,x_n$
(show proof).
Proof.
In first-order language, this means
- $\exists!X\forall u((u\in X)\leftrightarrow((u=x_1)\lor\ldots\lor(u=x_n)))$ if $n$ is non-zero, and
- $\exists!X\forall u(u\notin X)$ if $n$ is $0$.
The case $0$ is proven already, which is instantiated by the empty set.
Suppose the case $n$ is proven.
Given sets $x_1,\ldots,x_{S(n)}$, there exists some set $X_n$ such that a set $u$ is in $X_n$ if and only if $u$ is equal to one of $x_1,\ldots,x_n$.
By axiom of pairing, there exists a set $Y_{S(n)}$ such that for all $u$, $u\in Y_{S(n)}$ if and only if $u=x_{S(n)}$ or $u=x_{S(n)}$, if and only if $u=x_{S(n)}$.
Again by axiom of pairing, there exists a set $Z_{S(n)}$ such that for all $u$, $u\in Z_{S(n)}$ if and only if $u=X_n$ or $u=Y_{S(n)}$.
By axiom of union, there exists a set $X_{S(n)}$ such that for all $u$, $u\in X_{S(n)}$ if and only if for some $w\in Z_{S(n)}$, $u\in w$.
If a set $u$ is in $X_{S(n)}$, then for some $w\in Z_{S(n)}$, $u\in w$.
Then $w=X_n$ or $w=Y_{S(n)}$, thus $u\in X_n$ or $u\in Y_{S(n)}$.
- If $n$ is $0$, then $u\notin X_n$, thus $u\in Y_{S(n)}$ , implying $u=x_{S(n)}$, which is one of $x_1,\ldots,x_{S(n)}$.
- If $n$ is non-zero:
- if $u\in X_n$, then $(u=x_1)\lor\ldots\lor(u=x_n)$, thus $u$ is in one of $x_1,\ldots,x_{S(n)}$;
- if $u\in Y_{S(n)}$, then $u=x_{S(n)}$, which is one of $x_1,\ldots,x_{S(n)}$.
In all cases, $u$ is in one of $x_1,\ldots,x_{S(n)}$.
For the other direction, suppose $u$ is in one of $x_1,\ldots,x_{S(n)}$, which means $(u=x_1)\lor\ldots\lor(u=x_{S(n)})$.
- If $n$ is $0$, then we have $u=x_{S(n)}$, thus $u\in Y_{S(n)}$
Note that $Y_{S(n)}\in Z_{S(n)}$, thus for some $w\in Z_{S(n)}$, $u\in w$. And we have $u\in X_{S(n)}$.
- If $n$ is non-zero, then either $(u=x_1)\lor\ldots\lor(u=x_n)$ or $u=x_{S(n)}$.
We show above that if $u=x_{S(n)}$, then $u\in X_{S(n)}$.
If $(u=x_1)\lor\ldots\lor(u=x_n)$, then $u\in X_n$.
Note that $X_n\in Z_{S(n)}$, thus for some $w\in Z_{S(n)}$, $u\in w$. And we have $u\in X_{S(n)}$.
In all cases, $u\in X_{S(n)}$.
We have shown that a set $u$ is in $X_{S(n)}$ if and only if $u$ is equal to one of $x_1,\ldots,x_{S(n)}$.
By axiom of extensionality, this set is unique.
Hence the case $S(n)$ is proven.
By meta-logical induction, given any meta-logical natural number $n$, the case $n$ is proven.
$\blacksquare$
We will denote this set as $$\{x_1,\ldots,x_n\}$$
Note.
By definition, $\{\}=\emptyset$.
Proposition.
There is no set that contains itself.
(show proof)
Proof.
Suppose for contradiction that there exists $x$ such that $x\in x$.
Then by axiom of foundation, for some $u\in\{x\}$, no set is in both $\{x\}$ and $u$.
But then we have $u=x$ and $x\in x$, thus $x\in\{x\}$ and $x\in u$, a contradiction.
Note.
The above proposition implies that there is no set of all sets, because such a set would contain itself.
Union
Given a set $X$, by axiom of union, there exists, and thus uniquely exists, a set $Y$ such that a set $u$ is in $Y$ if and only if there exists $x\in X$ such that $u\in x$.
We will denote the set $Y$ as $$\bigcup X$$
Given sets $a,b$, we denote $\bigcup\{a,b\}$ as $a\cup b$.
Proposition.
$x\in X$ implies $x\subseteq\bigcup X$.
(show proof)
Proof.
Suppose $u\in x$ and $x\in X$, then $u\in\bigcup X$.
Thus $x\in X$ implies $x\subseteq\bigcup X$.
$\blacksquare$
Proposition.
$x\in a\cup b$ if and only if $x\in a$ or $x\in b$.
(show proof)
Proof.
If $x\in a\cup b$, then for some $c\in\{a,b\}$, $x\in c$.
Then $c=a$ or $c=b$, thus $x\in a$ or $x\in b$.
Suppose $x\in a$ or $x\in b$.
If $x\in a$, then $x\in a$ and $a\in\{a,b\}$, thus $x\in a\cup b$.
Similarly, if $x\in b$ then $x\in a\cup b$.
$\blacksquare$
Intersection
Given a non-empty set $X$, there exists a set $S_X$ in $X$, and
the set $\{u\in S_X|\forall x((x\in X)\to(u\in x))\}$ is the unique set such that a set $u$ is in it if and only if for all $x\in X$ we have $u\in x$.
We denote this set as $$\bigcap X$$
Given sets $a,b$, we denote $\bigcap\{a,b\}$ as $a\cap b$.
Proposition.
Suppose $X$ is non-empty, then $x\in X$ implies $\bigcap X\subseteq x$.
(show proof)
Proof.
Suppose $x\in X$ and $u\in\bigcap X$, then $u\in x$.
Thus $x\in X$ implies $\bigcap X\subseteq x$.
$\blacksquare$
Proposition.
$x\in a\cap b$ if and only if $x\in a$ and $x\in b$.
(show proof)
Proof.
If $x\in a\cap b$, then for all $c\in\{a,b\}$, $x\in c$.
Since $a\in\{a,b\}$ and $b\in\{a,b\}$, we have $x\in a$ and $x\in b$.
Suppose $x\in a$ and $x\in b$.
If $c\in\{a,b\}$, then $c=a$ or $c=b$.
In both cases, we have $x\in c$.
Thus $x\in a\cap b$.
$\blacksquare$
Disjoint
Given sets $x,y$, we say $x$ and $y$ are disjoint if and only if $(x\cap y)=\emptyset$.
Given a set $X$, we say $X$ is pairwise disjoint if and only if
$$\forall a\forall b(((a\in X)\land(b\in X)\land((a\cap b)\neq\emptyset))\to(a=b))$$
Difference
Given sets $x,y$, we define $x\setminus y$ as $\{u\in x|u\notin y\}$.
Complement
If we are given a set $X$ that contains all objects in consideration with respect to the given context,
then for a subset $S$ of $X$, the complement of $S$, denoted $S^c$, is $X\setminus S$.
Power set
Given a set $X$, by axiom of power set, there exists, and thus uniquely exists, a set $Y$ such that
a set $u$ is in $Y$ if and only if $u$ is a subset of $X$.
We denote the set $Y$ as $\mathcal P(X)$.
Ordered pair
Given sets $a,b$, an ordered pair $(a,b)$ is defined as $\{\{a\},\{a,b\}\}$.
When we say a set $p$ is an ordered pair of sets $A$ and $B$, we mean for some $a\in A$ and $b\in B$, $p=(a,b)$.
Proposition.
Given sets $a,b$, let $p$ denote $(a,b)$, then we have
$$a=\cup\cap p\quad\text{and}\quad b=\cup\{u\in\cup p|((\cup p\neq\cap p)\to(u\notin\cap p))\}$$
(show proof)
Proof.
Note that $p=(a,b)=\{\{a\},\{a,b\}\}$, implying $p$ is non-empty.
Clearly, $\cup p=\{a,b\}$ and $\cap p=\{a\}$. So $\cup\cap p=\cup\{a\}=a$.
- If $a=b$, then $\cup p=\{a\}$, and $\cup p=\cap p$, so we have $(\cup p\neq\cap p)\to(u\notin\cap p)$,
implying $\{u\in\cup p|((\cup p\neq\cap p)\to(u\notin\cap p))\}=\cup p=\{a\}$, so
$\cup\{u\in\cup p|((\cup p\neq\cap p)\to(u\notin\cap p))\}=a=b$.
- If $a\neq b$, then $\cup p\neq\cap p$.
-
If $u=a$, then $u\in\cap p$, so $u\notin\{u\in\cup p|((\cup p\neq\cap p)\to(u\notin\cap p))\}$.
-
If $u=b$, then $u\in\cup p$ and $u\notin\cap p$, so $u\in\{u\in\cup p|((\cup p\neq\cap p)\to(u\notin\cap p))\}$.
-
If $u\neq a$ and $u\neq b$, then $u\notin\cup p$, so $u\notin\{u\in\cup p|((\cup p\neq\cap p)\to(u\notin\cap p))\}$.
Hence, $u\in\{u\in\cup p|((\cup p\neq\cap p)\to(u\notin\cap p))\}$ if and only if $u=b$, implying
$\{u\in\cup p|((\cup p\neq\cap p)\to(u\notin\cap p))\}=\{b\}$ and thus
$\cup\{u\in\cup p|((\cup p\neq\cap p)\to(u\notin\cap p))\}=b$.
Therefore, we conclude that $\cup\{u\in\cup p|((\cup p\neq\cap p)\to(u\notin\cap p))\}=b$.
$\blacksquare$
Note.
By the above proposition, given a set $p$, if there exist sets $a$ and $b$ such that $p=(a,b)$, then
$$p=(\cup\cap p,\cup\{u\in\cup p|((\cup p\neq\cap p)\to(u\notin\cap p))\})$$
Proposition.
Given sets $a,b,c,d$, if $(a,b)=(c,d)$, then $a=c$ and $b=d$.
(show proof)
Proof.
Suppose $(a,b)=(c,d)$. Let $p$ denote $(a,b)$ and $q$ denote $(c,d)$.
Then $a=\cup\cap p=\cup\cap q=c$
and $b=\cup\{u\in\cup p|((\cup p\neq\cap p)\to(u\notin\cap p))\}=\cup\{u\in\cup q|((\cup q\neq\cap q)\to(u\notin\cap q))\}=d$.
$\blacksquare$
Cartesian product
Given sets $A$ and $B$,
we define the Cartesian product of $A$ and $B$, denoted $A\times B$, as
$\{u\in\mathcal P(\mathcal P(A\cup B))|\exists a\exists b((a\in A)\land(b\in B)\land(u=(a,b)))\}$.
Then a set $p$ is in $A\times B$ if and only if $p$ is an ordered pair of $A$ and $B$
(show proof).
Proof.
Suppose $p\in A\times B$, then there exist $a\in A$ and $b\in B$ such that $p=(a,b)$, meaning that $p$ is an ordered pair of $A$ and $B$.
If $p$ is an ordered pair of $A$ and $B$, then there exist $a\in A$ and $b\in B$ such that $p=(a,b)$.
Thus $\{a\},\{a,b\}\in\mathcal P(A\cup B)$,
and hence $p=(a,b)=\{\{a\},\{a,b\}\}\in\mathcal P(\mathcal P(A\cup B))$.
Therefore, $p\in A\times B$.
$\blacksquare$
Function
Given sets $f,X,Y$, we say $f$ is a function from $X$ to $Y$, denoted $f:X\to Y$,
if and only if $f\in\mathcal P(X\times Y)$ and for all $x\in X$, there exists a unique $y$ such that $(x,y)\in f$.
We will denote a witness of "there exists a unique $y$ such that $(x,y)\in f$", with arguments $f$ and $x$, by $f(x)$,
so that given any $f:X\to Y$ and $x\in X$, we have $(x,f(x))\in f$, and for all $y$, $(x,y)\in f$ implies $f(x)=y$.
If $f$ is a function from $X$ to $Y$, then $X$ is called the domain of $f$, $Y$ is called the codomain of $f$,
and $\{y\in Y|\exists x\in X,f(x)=y\}$ is called the range of $f$.
Function without codomain
Given sets $f,X$, we say $f$ is a function from $X$ if
for all $u\in f$, there exist $a,b$ such that $a\in X$ and $u=(a,b)$, and
for all $x\in X$, there exists a unique $y$ such that $(x,y)\in f$.
By axiom schema of replacement, there exists $Y$ such that $f$ is a function from $X$ to $Y$.
Equality of functions
Given $f:X\to Y$ and $g:X\to Z$, if for all $x\in X$, $f(x)=g(x)$, then $f=g$.
(show proof)
Proof.
Let $u\in f$, then $u\in X\times Y$, so for some $x\in X$ and $y\in Y$, $u=(x,y)$.
Then we have $(x,y)\in f$, implying $g(x)=f(x)=y$.
Note that $(x,g(x))\in g$, hence $(x,y)\in g$ and thus $u\in g$.
By a symmetric argument, if $u\in g$, then $u\in f$.
Therefore $f=g$.
$\blacksquare$
Independence of range on codomain
Suppose $f$ is both a function from $X$ to $Y$ and a function from $X$ to $Z$,
then $$\{y\in Y|\exists x\in X,f(x)=y\}=\{y\in Z|\exists x\in X,f(x)=y\}$$
(show proof)
Proof.
Let $y\in\{y\in Y|\exists x\in X,f(x)=y\}$.
Then for some $x\in X$, $f(x)=y$.
Since $f\subseteq X\times Z$ and $(x,f(x))\in f$, we have $y=f(x)\in Z$.
Thus $y\in\{y\in Z|\exists x\in X,f(x)=y\}$.
By a symmetric argument, we have the other direction.
$\blacksquare$
Proposition.
Given $f:X\to Y$, suppose $V$ is the range of $f$, then $f$ is a function from $X$ to $Z$ if and only if $V\subseteq Z$.
(show proof)
Proof.
Suppose $f$ is a function from $X$ to $Z$.
Let $y\in V$, then for some $x\in X$, $f(x)=y$.
Since $f\subseteq X\times Z$ and $(x,f(x))\in f$, we have $y=f(x)\in Z$.
Thus $V\subseteq Z$.
Suppose $V\subseteq Z$. We only need to show that $f\in\mathcal P(X\times Z)$.
Let $u\in f$. Since $f\subseteq X\times Y$, there exists $x\in X$ and $y\in Y$ such that $u=(x,y)$, thus $(x,y)\in f$.
Since $x\in X$, we have $f(x)=y$.
Then $y\in\{y\in Y|\exists x\in X,f(x)=y\}=V\subseteq Z$.
Thus $u=(x,y)\in X\times Z$.
And we have shown that $f\in\mathcal P(X\times Z)$.
$\blacksquare$
Defining functions with formulas
Given $X$ and $Y$ and a formula $\varphi(x,y)$
such that for all $x\in X$ there exists a unique $y\in Y$ that satisfies $\varphi(x,y)$,
$$\{u\in(X\times Y)|\forall x\forall y((x,y)=u\to\varphi(x,y))\}$$
defines a function $f$ from $X$ to $Y$
(show proof).
Proof.
Clearly $f\in\mathcal P(X\times Y)$.
Let $x'\in X$, then there exists a unique $y^*\in Y$ that satisfies $\varphi(x',y^*)$.
Thus $(x',y^*)\in X\times Y$, and $(x,y)=(x',y^*)$ implies $x'=x$ and $y^*=y$, which implies $\varphi(x',y)\to\varphi(x,y)$ and $\varphi(x',y^*)\to\varphi(x',y)$,
and since we have $\varphi(x',y^*)$, we have $\varphi(x,y)$.
We have shown that $(x',y^*)\in f$.
Now suppose $(x',y'')\in f$, then $y''\in Y$.
Since $\forall x\forall y((x,y)=(x',y'')\to\varphi(x,y))$, we have $\varphi(x',y'')$.
And by uniqueness of $y\in Y$ that satisfies $\varphi(x',y)$, we have $y^*=y''$.
We have shown that there exists a unique $y'$ such that $(x',y')\in f$.
Thus $f$ is a function from $X$ to $Y$.
$\blacksquare$
And we say $f:X\to Y$ is defined by $\varphi(x,y)$ with $x$ as input and $y$ as output.
Proposition.
Given $X$ and $Y$, suppose $y(x)$ is some term such that for all $x\in X$, $y(x)\in Y$,
then we can define a function $f:X\to Y$ such that for all $x\in X$, $f(x)=y(x)$.
(show proof)
Proof.
Note that for all $x'\in X$, $y(x')\in Y$ and $y(x')=y(x')$.
Trivially, if $z\in Y$ and $z=y(x')$, then $z=y(x')$.
Thus given $x'\in X$, there exists a unique $y'\in Y$ such that $y'=y(x')$.
Then we can define a function $f:X\to Y$ by $y'=y(x')$ with $x'$ as input and $y'$ as output.
Let $x\in X$, then $(x,y(x))\in X\times Y$, and if $(x',y')=(x,y(x))$, then $y'=y(x)=y(x')$.
Hence $(x,y(x))\in f$, and therefore $f(x)=y(x)$.
$\blacksquare$
Proposition.
Given $X$, suppose $y(x)$ is some term, then for some $Y$,
we can define a function $f:X\to Y$ such that for all $x\in X$, $f(x)=y(x)$.
(show proof)
Proof.
Clearly, for all $x\in X$, there exists a unique $y'$ such that $y'=y(x)$.
Then by axiom schema of replacement, there exists $Y$ such that for all $x\in X$, there exists $y'\in Y$ such that $y'=y(x)$, implying $y(x)\in Y$.
Then by the above proposition, we can define a function $f:X\to Y$ such that for all $x\in X$, $f(x)=y(x)$.
$\blacksquare$
Implicit range notation
Suppose we have a term $y(x)$ and a formula $\varphi(x)$ such that there exists a set $X$ such that for all $x$, $x\in X$ if and only if $\varphi(x)$.
Then for some $Y$, we can define a function $f:X\to Y$ such that for all $x\in X$, $f(x)=y(x)$.
We use the notation
$$\{y(x):\varphi(x)\}$$
to denote the range of $f$.
Note that $u\in\{y(x):\varphi(x)\}$ if and only if there exists $x$ such that $\varphi(x)$ and $y(x)=u$
(show proof).
Proof.
Suppose $u\in\{y(x):\varphi(x)\}$. Then there exists $x\in X$ such that $f(x)=u$.
Since $x\in X$, we have $\varphi(x)$ and $f(x)=y(x)$, thus $y(x)=u$.
Suppose there exists $x$ such that $\varphi(x)$ and $y(x)=u$.
Since $\varphi(x)$, we have $x\in X$, thus $f(x)=y(x)=u$ and $u=f(x)\in Y$.
Hence $u\in\{y(x):\varphi(x)\}$.
$\blacksquare$
Proposition.
Suppose we have terms $y_1(x),y_2(x)$ and a formula $\varphi(x)$ such that there exists a set $X$ with $x\in X$ if and only if $\varphi(x)$.
If for all $x$ such that $\varphi(x)$, we have $y_1(x)=y_2(x)$, then $\{y_1(x):\varphi(x)\}=\{y_2(x):\varphi(x)\}$.
(show proof)
Proof.
Let $u\in\{y_1(x):\varphi(x)\}$, then there exists $x$ such that $\varphi(x)$ and $y_1(x)=u$,
thus $y_2(x)=y_1(x)=u$, hence $u\in\{y_2(x):\varphi(x)\}$.
By a symmetric argument, if $u\in\{y_2(x):\varphi(x)\}$ then $u\in\{y_1(x):\varphi(x)\}$.
Therefore $\{y_1(x):\varphi(x)\}=\{y_2(x):\varphi(x)\}$.
$\blacksquare$
Restriction
Given $f:X\to Y$, and $U\subseteq X$,
$$\{u\in(U\times Y)|u\in f\}$$
is a function from $U$ to $Y$, called the restriction of $f$ on $U$, and denoted $f|_U$.
Note that for all $x\in U$, $f|_U(x)=f(x)$.
Image
Given $f:X\to Y$, and $U\subseteq X$,
the range of $f|_U$ is called the image of $f$ on $U$, denoted $f(U)$.
Note that $y\in f(U)$ if and only if there exists $x\in U$ such that $f(x)=y$.
Preimage
Given $f:X\to Y$, and $V\subseteq Y$,
$$\{x\in X|f(x)\in V\}$$
is called the preimage of $f$ on $V$, denoted $f^{-1}(V)$.
Proposition.
Given $f:X\to Y$ and $x\in U\subseteq X$, we have $f(x)\in f(U)$.
(show proof)
Proof.
Since $x\in U$ and $f(x)=f(x)$, there exists $u\in U$ such that $f(u)=f(x)$, thus $f(x)\in f(U)$.
$\blacksquare$
Proposition.
Given $f:X\to Y$ and $V\subseteq U\subseteq X$, we have $f(V)\subseteq f(U)$.
(show proof)
Proof.
If $y\in f(V)$, then there exists $x\in V$ such that $f(x)=y$, thus there exists $x\in U$ such that $f(x)=y$, hence $y\in f(U)$.
$\blacksquare$
Proposition.
Given $f:X\to Y$ and $T\subseteq S\subseteq Y$, we have $f^{-1}(T)\subseteq f^{-1}(S)$.
(show proof)
Proof.
If $x\in f^{-1}(T)$, then $x\in X$ and $f(x)\in T$, thus $x\in X$ and $f(x)\in S$, hence $x\in f^{-1}(S)$.
$\blacksquare$
Proposition.
Given $f:X\to Y$, $U\subseteq X$, and $V\subseteq Y$, we have $U\subseteq f^{-1}(f(U))$ and $f(f^{-1}(V))\subseteq V$.
(show proof)
Proof.
Let $x\in U$, then $x\in X$ and $f(x)\in f(U)$, thus $x\in f^{-1}(f(U))$.
Let $y\in f(f^{-1}(V))$, then there exists $x\in f^{-1}(V)$ such that $f(x)=y$,
thus $y=f(x)\in V$.
$\blacksquare$
Injectivity
Given $f:X\to Y$, if for all $x_1,x_2\in X$, $f(x_1)=f(x_2)$ implies $x_1=x_2$, then $f$ is said to be injective.
Surjectivity
Given $f:X\to Y$, if for all $y\in Y$, there exists $x\in X$ such that $f(x)=y$, then $f$ is said to be surjective.
Bijectivity
Given $f:X\to Y$, if $f$ is both injective and surjective, then $f$ is said to be bijective.
Proposition.
Given $f:X\to Y$, $f$ is bijective if and only if for all $y\in Y$, there exists a unique $x\in X$ such that $f(x)=y$.
(show proof)
Proof.
Suppose $f$ is bijective, then it is both injective and surjective.
By surjectivity, there exists $x\in X$ such that $f(x)=y$.
Now suppose we have $x'\in X$ such that $f(x')=y$, then by injectivity, we have $x=x'$.
Thus there exists a unique $x\in X$ such that $f(x)=y$.
Suppose for all $y\in Y$, there exists a unique $x\in X$ such that $f(x)=y$.
Let $y\in Y$, then there trivially exists $x\in X$ such that $f(x)=y$, thus $f$ is surjective.
Now suppose $x_1,x_2\in X$ and $f(x_1)=f(x_2)$.
Since $f(x_1)\in Y$, there exists a unique $x\in X$ such that $f(x)=f(x_1)$.
Since $x_1\in X$ and $f(x_1)=f(x_1)$, by uniqueness we have $x_1=x$.
Since $x_2\in X$ and $f(x_2)=f(x_1)$, by uniqueness we have $x_2=x$.
Thus $x_1=x_2$. And we have shown that $f$ is injective.
Since $f$ is both injective and surjective, it is bijective.
$\blacksquare$
Inverse function
Given bijective $f:X\to Y$,
$$\{u\in(Y\times X)|\forall y\forall x((y,x)=u\to f(x)=y)\}$$
is a function from $Y$ to $X$
(show proof),
Proof.
Let $g=\{u\in(Y\times X)|\forall y\forall x((y,x)=u\to f(x)=y)\}$
Clearly, $g$ is a subset of $Y\times X$.
Let $y'\in Y$, by surjectivity of $f$, there exists $x^*\in X$ such that $f(x^*)=y'$.
If $(y,x)=(y',x^*)$, then $y=y'$ and $x=x^*$, thus $f(x)=y$.
We have shown that $(y',x^*)\in g$.
Suppose $(y',x'')\in g$, then $f(x'')=y'$, and by injectivity of $f$, $x''=x^*$.
We have shown that there exists a unique $x'$ such that $(y',x')\in g$.
Therefore, $g$ is a function from $Y$ to $X$.
$\blacksquare$
called the inverse function of $f$, and denoted $f^{-1}$.
Proposition.
Given bijective $f:X\to Y$, for all $x\in X$, $f^{-1}(f(x))=x$, and for all $y\in Y$, $f(f^{-1}(y))=y$.
(show proof)
Proof.
Let $x\in X$, then $f(x)\in Y$, so $(f(x),x)\in Y\times X$.
Since if $(y',x')=(f(x),x)$, then $f(x')=f(x)=y'$, we have $(f(x),x)\in f^{-1}$,
thus $f^{-1}(f(x))=x$.
Let $y\in Y$, then there exists $x\in X$ such that $f(x)=y$.
Hence $f(f^{-1}(y))=f(f^{-1}(f(x)))=f(x)=y$.
$\blacksquare$
Proposition.
Inverse functions are bijective.
(show proof)
Proof.
Let $f:X\to Y$ be bijective.
Suppose $y_1,y_2\in Y$ and $f^{-1}(y_1)=f^{-1}(y_2)$.
Then $y_1=f(f^{-1}(y_1))=f(f^{-1}(y_2))=y_2$.
Thus $f^{-1}$ is injective.
Suppose $x\in X$, then $f(x)\in Y$ and $f^{-1}(f(x))=x$.
Thus $f^{-1}$ is surjective.
$\blacksquare$
Proposition.
Given bijective $f:X\to Y$, $$(f^{-1})^{-1}=f$$
(show proof)
Proof.
Since $f^{-1}:Y\to X$ is bijective, $(f^{-1})^{-1}$ is a function from $X$ to $Y$.
Let $x\in X$, then there exists $y\in Y$ such that $f^{-1}(y)=x$,
thus $$(f^{-1})^{-1}(x)=(f^{-1})^{-1}(f^{-1}(y))=y=f(f^{-1}(y))=f(x)$$
Therefore $(f^{-1})^{-1}=f$.
$\blacksquare$
Proposition.
Given $f:X\to Y$ and $g:Y\to X$, if for all $x\in X$, $g(f(x))=x$, and for all $y\in Y$, $f(g(y))=y$, then $f$ is bijective and $g=f^{-1}$.
(show proof)
Proof.
Suppose $x_1,x_2\in X$ and $f(x_1)=f(x_2)$, then $x_1=g(f(x_1))=g(f(x_2))=x_2$. Thus $f$ is injective.
Let $y\in Y$, then $g(y)\in X$ and $f(g(y))=y$. Thus $f$ is surjective.
We have shown that $f$ is bijective.
Let $y\in Y$, then there exists $x\in X$ such that $f(x)=y$, thus $g(y)=g(f(x))=x=f^{-1}(f(x))=f^{-1}(y)$.
Therefore $g=f^{-1}$.
$\blacksquare$
Proposition.
Given bijective $f:X\to Y$ and $U\subseteq X$, let $V=f(U)$, then $f|_U:U\to V$ is bijective and $$(f|_U)^{-1}=(f^{-1})|_V$$
(show proof)
Proof.
Clearly, $f|_U$ is a function from $U$ to $V$, which is the range of $f|_U$.
Let $x_1,x_2\in U$ and $f|_U(x_1)=f|_U(x_2)$, then $f(x_1)=f|_U(x_1)=f|_U(x_2)=f(x_2)$, then by injectivity of $f$, $x_1=x_2$.
Thus $f|_U:U\to V$ is injective. Let $y\in V$, then $y\in\{v\in Y|\exists u\in U,f|_U(u)=v\}$,
thus there exists $x\in U$ such that $f|_U(x)=y$, implying $f|_U:U\to V$ is surjective.
Note that both $(f|_U)^{-1}$ and $(f^{-1})|_V$ are functions from $V$.
Let $y\in V$, then there exists $x\in U$ such that $f|_U(x)=y$, and thus $f(x)=f|_U(x)=y$.
Hence $$(f|_U)^{-1}(y)=(f|_U)^{-1}(f|_U(x))=x=f^{-1}(f(x))=f^{-1}(y)=(f^{-1})|_V(y)$$
Therefore $(f|_U)^{-1}=(f^{-1})|_V$.
$\blacksquare$
Proposition.
Given bijective $f:X\to Y$ and $V\subseteq Y$, the preimage of $f$ on $V$ equals the image of $f^{-1}$ on $V$.
(show proof)
Proof.
Let $x\in\{u\in X|f(u)\in V\}$. Then $x\in X$ and $f(x)\in V$, and we have $f^{-1}(f(x))=x$.
Hence $x\in\{u\in X|\exists v\in V, f^{-1}(v)=u\}=\{u\in X|\exists v\in V, f^{-1}|_V(v)=u\}$.
Let $x\in\{u\in X|\exists v\in V, f^{-1}|_V(v)=u\}$, then $x\in X$ and for some $v\in V$, $f^{-1}(v)=x$.
Thus $f(x)=f(f^{-1}(v))=v\in V$. Hence $x\in\{u\in X|f(u)\in V\}$.
$\blacksquare$
Note.
The above proposition shows that the notation $f^{-1}(V)$ is unambiguous when $f$ is bijective.
Proposition.
Given bijective $f:X\to Y$, $U\subseteq X$, and $V\subseteq Y$, we have $f^{-1}(f(U))=U$ and $f(f^{-1}(V))=V$.
(show proof)
Proof.
Let $x\in U$, then $f(x)\in f(U)$, thus $x=f^{-1}(f(x))\in f^{-1}(f(U))$.
Let $x\in f^{-1}(f(U))$, then $x\in X$ and for some $y\in f(U)$, $f^{-1}(y)=x$,
thus $y\in Y$ and for some $u\in U$, $f(u)=y$. Hence $x=f^{-1}(f(u))=u\in U$.
We have shown that $f^{-1}(f(U))=U$, and by a symmetric argument, we have $f(f^{-1}(V))=(f^{-1})^{-1}(f^{-1}(V))=V$.
$\blacksquare$
Composite function
Given $f:A\to B$ and $g:C\to D$, then $$\{u\in (f^{-1}(C)\times D)|\forall x\forall y(u=(x,y)\to(y=g(f(x))))\}$$
is a function from $f^{-1}(C)$ to $D$
(show proof),
Proof.
Let $h=\{u\in (f^{-1}(C)\times D)|\forall x\forall y(u=(x,y)\to(y=g(f(x))))\}$.
Clearly, $h$ is a subset of $f^{-1}(C)\times D$.
Suppose $x\in f^{-1}(C)$, then $f(x)\in C$ and $g(f(x))\in D$, thus $(x,g(f(x)))\in f^{-1}(C)\times D$.
Since if $(x,g(f(x)))=(x',y')$, then $y'=g(f(x))=g(f(x'))$, we have $(x,g(f(x)))\in h$.
Suppose $(x,y)\in h$, then if $(x,y)=(x',y')$, we have $y=y'=g(f(x'))=g(f(x))$.
We have shown that there exists a unique $y$ such that $(x,y)\in h$.
Therefore $h$ is a function from $f^{-1}(C)$ to $D$.
$\blacksquare$
denoted $(g\circ f)$. Note that for all $x\in f^{-1}(C)$, $$(g\circ f)(x)=g(f(x))$$
Proposition.
Given $f:A\to B$, $g:C\to D$, $h:E\to F$, $$h\circ(g\circ f)=(h\circ g)\circ f$$
(show proof)
Proof.
$h\circ(g\circ f)$ is a function from $(g\circ f)^{-1}(E)$ to $F$
and $(h\circ g)\circ f$ is a function from $f^{-1}(g^{-1}(E))$ to $F$.
Let $u\in(g\circ f)^{-1}(E)$, then $u\in f^{-1}(C)$ and $(g\circ f)(u)\in E$, thus $(g\circ f)(u)=g(f(u))$ and $g(f(u))\in E$.
Since $f(u)\in C$, $f(u)\in g^{-1}(E)$. Since $u\in A$, $u\in f^{-1}(g^{-1}(E))$.
For the other direction, let $u\in f^{-1}(g^{-1}(E))$, then $f(u)\in g^{-1}(E)$ and $g(f(u))\in E$.
Since $g^{-1}(E)\subseteq C$, $u\in f^{-1}(C)$, thus $(g\circ f)(u)=g(f(u))$ and $(g\circ f)(u)\in E$.
Hence $u\in(g\circ f)^{-1}(E)$.
We have shown that $(g\circ f)^{-1}(E)$=$f^{-1}(g^{-1}(E))$, and we will denote these sets as $S$.
Let $u\in S$, then $u\in f^{-1}(C)$ and $f(u)\in g^{-1}(E)$ as shown above, thus $$(h\circ(g\circ f))(u)=h((g\circ f)(u))=h(g(f(u)))=(h\circ g)(f(u))=((h\circ g)\circ f)(u)$$
Hence $h\circ(g\circ f)=(h\circ g)\circ f$.
$\blacksquare$
Proposition.
Given bijective $f:X\to Y$ and $g:Y\to Z$, $g\circ f$ is bijective and $$(g\circ f)^{-1}=f^{-1}\circ g^{-1}$$
(show proof)
Proof.
$g\circ f$ is clearly a function from $X$ to $Z$.
Suppose $x_1,x_2\in X$ and $(g\circ f)(x_1)=(g\circ f)(x_2)$, then $g(f(x_1))=g(f(x_2))$,
thus by injectivity of $g$, $f(x_1)=f(x_2)$, and by injectivity of $f$, $x_1=x_2$.
Hence $g\circ f$ is injective. Let $z\in Z$, then by surjectivity of $g$, there exists $y\in Y$ such that $g(y)=z$,
and by surjectivity of $f$, there exists $x\in X$ such that $f(x)=y$, thus $(g\circ f)(x)=g(f(x))=g(y)=z$.
Hence $g\circ f$ is surjective. We have shown that $g\circ f$ is bijective.
Clearly, both $(g\circ f)^{-1}$ and $f^{-1}\circ g^{-1}$ are functions from $Z$ to $X$.
Let $z\in Z$, then there exists $x\in X$ such that $(g\circ f)(x)=z$,
thus $$(g\circ f)^{-1}(z)=(g\circ f)^{-1}((g\circ f)(x))=x=f^{-1}(f(x))=f^{-1}(g^{-1}(g(f(x))))=(f^{-1}\circ g^{-1})((g\circ f)(x))=(f^{-1}\circ g^{-1})(z)$$
Therefore $(g\circ f)^{-1}=f^{-1}\circ g^{-1}$.
$\blacksquare$
Note.
With the notations we now have, we can rewrite axiom of infinity as $\exists S((\emptyset\in S)\land\forall x((x\in S)\to((x\cup\{x\})\in S)))$
(show proof).
Proof.
Denote a witness of the axiom by $S^*$, which is a constant symbol, then we have
$$\text{(1) }\forall z(\forall y\neg(y\in z)\to(z\in S^*))$$
and
$$\text{(2) }\forall x((x\in S^*)\to\forall X(\forall u((u\in X)\leftrightarrow((u\in x)\lor(u=x)))\to(X\in S^*)))$$
From (1), we have
$$(\forall y\neg(y\in\emptyset)\to(\emptyset\in S^*))$$
Since, by definition of $\emptyset$, we have
$$\forall y\neg(y\in\emptyset)$$
we conclude that
$$\text{(3) }(\emptyset\in S^*)$$
From (2), by LA2, we have
$$((x\in S^*)\to(\forall u((u\in(x\cup\{x\}))\leftrightarrow((u\in x)\lor(u=x)))\to((x\cup\{x\})\in S^*)))$$
Clearly, we have $$\forall u((u\in(x\cup\{x\}))\leftrightarrow((u\in x)\lor(u=x)))$$
thus $$((x\in S^*)\to((x\cup\{x\})\in S^*))$$
and hence $$\text{(4) }\forall x((x\in S^*)\to((x\cup\{x\})\in S^*))$$
Therefore, from (3) and (4), $$\exists S((\emptyset\in S)\land\forall x((x\in S)\to((x\cup\{x\})\in S)))$$
$\blacksquare$
For an arbitrary set $X$, we will denote the formula $((\emptyset\in X)\land\forall x((x\in X)\to((x\cup\{x\})\in X)))$ by $\mathcal I(X)$.
Natural number
By axiom of infinity, we have $\exists S\mathcal I(S)$.
Denote a witness of this by $C$, then we have $\mathcal I(C)$.
Denote $\{A\in\mathcal P(C)|\mathcal I(A)\}$ by $I$,
then $C\in I$, so $I$ is non-empty.
Denote $\cap I$ by $N$, then a set $n$ is called a natural number if and only if $n\in N$.
Note that $N$ is a term with no free variables and we have $\mathcal I(N)$
(show proof).
Proof.
$\emptyset$ is in every set in $I$, so $\emptyset\in N$.
Suppose a set $x$ is in $N$, then $x$ is in every set in $I$,
so $(x\cup\{x\})$ is in every set in $I$, so $(x\cup\{x\})$ is in $N$.
$\blacksquare$
Since for all $n\in N$, $n\cup\{n\}\in N$, we can define a function $S:N\to N$ such that for all $n\in N$, $S(n)=n\cup\{n\}$, called the
successor function.
Note that we can use meta-logical recursion to define a meta-logical function $f$ from meta-logical natural numbers to the collection of terms such that
- $f(0)=\emptyset$, and
- for all meta-logical natural number $n$, $f(S^*(n))$ and $S(f(n))$ are identical, where $S^*$ is the meta-logical successor function.
By meta-logical induction, for all meta-logical natural number $n$, we have $f(n)\in N$.
Given a meta-logical natural number $n$, we use the numeral of $n$ to represent the term $f(n)$.
Proposition.
For all $n\in N$, $S(n)\neq0$.
(show proof)
Proof.
Given $n\in N$, clearly $n\in S(n)$, thus $S(n)\neq0$.
$\blacksquare$
Induction theorem
Suppose $\varphi(n)$ is a formula.
If we have $\varphi(0)$, and for every $n\in N$,
$\varphi(n)$ implies $\varphi(S(n))$, then for every $n\in N$ we have $\varphi(n)$.
(show proof)
Proof.
Suppose $\varphi(0)$ and for every $n\in N$,
$\varphi(n)$ implies $\varphi(S(n))$.
Consider $\{u\in N|\varphi(u)\}$, denoted $A$.
Since $0\in N$ and $\varphi(0)$, we have $0\in A$.
If $n\in A$, then $n\in N$ and $\varphi(n)$, so $S(n)\in N$ and $\varphi(S(n))$,
which means $S(n)\in A$. Hence we have $\mathcal I(A)$.
Using the same notations as above, since $A\subseteq N\subseteq C$, we have $A\in \mathcal P(C)$.
Since we also have $\mathcal I(A)$, we know $A\in I$, which then implies $N\subseteq A$, and hence $N=A$.
Then we conclude that for every $n\in N$ we have $\varphi(n)$.
$\blacksquare$
Proposition.
For all $n\in N$, $n\subset N$.
(show proof)
Proof.
We will use induction theorem.
For the base case, since $0$ is $\emptyset$, we have $0\subset N$.
Now take as inductive hypothesis that $n\in N$ and $n\subset N$.
If $x\in S(n)$, then either $x=n$ or $x\in n$.
If $x=n$, then $x\in N$. If $x\in n$, since $n\subset N$, we have $x\in N$.
Thus $S(n)\subseteq N$. Since $n\in N$, we have $S(n)\in N$, but then since $S(n)\notin S(n)$, we have $S(n)\subset N$.
This concludes the inductive step.
By induction theorem, for every $n\in N$ we have $n\subset N$.
$\blacksquare$
Proposition.
For all $n\in N$, for all $x\in n$, we have $x\subset n$.
(show proof)
Proof.
We will use induction theorem.
For the base case, since $0$ is $\emptyset$, we have $\neg(x\in 0)$,
so for all $x$, $x\in 0$ implies $x\subset 0$.
Now take as inductive hypothesis that $n\in N$ and for all $x$, $x\in n$ implies $x\subset n$.
If $x\in S(n)$, then either $x=n$ or $x\in n$:
- If $x=n$, since no set contains itself, we have $n\notin n$, $n\in S(n)$, and $n\subseteq S(n)$,
which together imply $n\subset S(n)$, and hence $x\subset S(n)$.
- If $x\in n$, then we have $x\subset n$. Since $n\subseteq S(n)$, we have $x\subset S(n)$.
In both cases we have $x\subset S(n)$.
Hence for all $x$, $x\in S(n)$ implies $x\subset S(n)$.
This concludes the inductive step.
By induction theorem, for every $n\in N$ we have that for all $x$, $x\in n$ implies $x\subset n$.
$\blacksquare$
Proposition.
For all $n\in N$, if $n\neq0$, then there exists $m\in N$ such that $S(m)=n$.
(show proof)
Proof.
Let $\varphi(n)$ denote the formula "if $n\neq0$, then there exists $m\in N$ such that $S(m)=n$".
Trivially, we have $\varphi(0)$.
Suppose $n\in N$ and $\varphi(n)$, we have $S(n)=S(n)$, thus there exists $m\in N$ such that $S(m)=S(n)$, implying we have $\varphi(S(n))$.
By induction, for all $n\in N$, we have $\varphi(n)$.
$\blacksquare$
Proposition.
Suppose $\varphi(n)$ is a formula. If $n\in N$, $\varphi(0)$, and
for all $k\in n$, $\varphi(k)$ implies $\varphi(S(k))$, then we have $\varphi(n)$.
(show proof)
Proof.
Fix $n\in N$ and suppose $\varphi(0)$ and for all $k\in n$, $\varphi(k)$ implies $\varphi(S(k))$.
Let $\psi(k)$ be the formula "if $k\in n$, then $\varphi(k)$".
Since $\varphi(0)$, we have $\psi(0)$.
Suppose $k\in N$ and $\psi(k)$.
- If $S(k)\in n$, then $S(k)\subset n$, thus $k\in n$, and we have $\varphi(k)$, hence we also have $\varphi(S(k))$, and thus $\psi(S(k))$.
- If $S(k)\notin n$, then we have $\psi(S(k))$.
Then by induction, for all $k\in N$, we have $\psi(k)$.
- If $n=0$, then by $\varphi(0)$, we have $\varphi(n)$.
- If $n\neq0$, then for some $m\in N$ we have $S(m)=n$, implying $m\in n$.
Since $m\in N$, we have $\psi(m)$, and since $m\in n$, we have $\varphi(m)$, and $\varphi(m)$ implies $\varphi(S(m))$.
Hence we have $\varphi(S(m))$, which is $\varphi(n)$.
$\blacksquare$
Proposition.
The successor function is injective.
(show proof)
Proof.
Suppose $n,m\in N$ and $S(n)=S(m)$, then $((n\cup\{n\})=(m\cup\{m\}))$, so either $n=m$ or $n\in m$,
and either $m=n$ or $m\in n$.
Suppose $n\neq m$, then $n\in m$ and $m\in n$, but by the above lemma, we then have $n\subset m$ and $m\subset n$,
and hence $n\subseteq m$ and $m\subseteq n$, which then implies $m=n$, a contradiction.
Therefore, $n,m\in N$ and $S(n)=S(m)$ imply $n=m$. This proves injectivity of $S$.
$\blacksquare$
Proposition.
Given arbitrary sets $m,n$, if $m,n\in N$ then we have exactly one of $m\in n$, $n\in m$, $m=n$.
(show proof)
Proof.
We will first prove that if $m,n\in N$ then we have at least one of $m\in n$, $n\in m$, $m=n$.
Denote that we have at least one of $m\in n$, $n\in m$, $m=n$ by $\varphi(m,n)$,
denote $\{s\in N|\varphi(x,s)\}$ by $C(x)$,
and denote $\{r\in N|C(r)=N\}$ by $I$.
Since $0=0$, we have $\varphi(0,0)$, so $0\in C(0)$. Suppose $a\in N$ and $a\in C(0)$,
then $\varphi(0,a)$,
- if $0\in a$, then $0\in S(a)$, so $\varphi(0,S(a))$;
- if $a\in 0$, we have a contradiction, hence $\varphi(0,S(a))$;
- if $a=0$, then $0\in S(a)$, so $\varphi(0,S(a))$.
And we conclude that $a\in N$ and $a\in C(0)$ imply $S(a)\in C(0)$.
So by induction, $C(0)=N$, hence $0\in I$.
Suppose $a\in N$ and $a\in I$, then $C(a)=N$, so $\varphi(a,0)$,
- if $a\in 0$, we have a contradiction, hence $\varphi(S(a),0)$;
- if $0\in a$, then $0\in S(a)$, so $\varphi(S(a),0)$;
- if $a=0$, then $0\in S(a)$, so $\varphi(S(a),0)$.
And we conclude that $0\in C(S(a))$.
Suppose $b\in N$ and $b\in C(S(a))$, then $\varphi(S(a),b)$,
- if $S(a)\in b$, then $S(a)\in S(b)$, so $\varphi(S(a),S(b))$;
- if $b\in S(a)$, then either $b=a$ or $b\in a$,
- if $b=a$, then $S(a)=S(b)$, so $\varphi(S(a),S(b))$;
- if $b\in a$, then $b\subset a$; note that
$C(a)=N$, we have $\varphi(a,S(b))$,
- if $a\in S(b)$, then either $a=b$ or $a\in b$,
- if $a=b$, then $S(a)=S(b)$, so $\varphi(S(a),S(b))$;
- if $a\in b$, then $a\subset b$, a contradiction, hence $\varphi(S(a),S(b))$;
- if $S(b)\in a$, then $S(b)\in S(a)$, so $\varphi(S(a),S(b))$;
- if $a=S(b)$, then $S(b)\in S(a)$, so $\varphi(S(a),S(b))$;
- if $S(a)=b$, then $S(a)\in S(b)$, so $\varphi(S(a),S(b))$.
And we conclude that $b\in N$ and $b\in C(S(a))$ imply $S(b)\in C(S(a))$.
So by induction, $C(S(a))=N$, hence $S(a)\in I$.
Note that we are working under the assumption that $a\in N$ and $a\in I$,
so we conclude that $a\in N$ and $a\in I$ imply $S(a)\in I$.
Again by induction, we have that $I=N$.
If $m,n\in N$, then $m\in I$, or $C(m)=N$, so $n\in C(m)$, or $\varphi(m,n)$,
we have at least one of $m\in n$, $n\in m$, $m=n$.
We now prove that if $m,n\in N$, then we have at most one of $m\in n$, $n\in m$, $m=n$.
Suppose $m,n\in N$, then $m\in n$ implies $m\subset n$, and $n\in m$ implies $n\subset m$.
Clearly, we have at most one of $m\subset n$, $n\subset m$, $m=n$.
Hence we have at most one of $m\in n$, $n\in m$, $m=n$.
Combining the above results, we conclude that $m,n\in N$ implies that we have
at least and at most one of $m\in n$, $n\in m$, $m=n$;
that is, we have exactly one of $m\in n$, $n\in m$, $m=n$.
$\blacksquare$
Order on natural numbers
For natural numbers $m$ and $n$, we denote $(m\in n)$ by $(m\lt n)$ or $(n\gt m)$,
and $((m\in n)\lor(m=n))$ by $(m\le n)$ or $(n\ge m)$.
Proposition.
For all $m,n,k\in N$, if $m\lt n$ and $n\lt k$, then $m\lt k$.
(show proof)
Proof.
Fix $m,n,k\in N$.
Suppose $m\lt n$ and $n\lt k$, then $m\in n$ and $n\in k$, so $m\subset n$ and $n\subset k$, hence $m\subset k$.
- If $m\in k$, then we have $m\lt k$;
- if $k\in m$, then $k\lt m$, so $k\subset m$, a contradiction;
- if $k=m$, we have a contradiction.
Hence we conclude that $m\lt k$.
$\blacksquare$
Proposition.
A non-empty set of natural numbers has a least element.
(show proof)
Proof.
Suppose $M\subseteq N$ is non-empty.
Suppose for contradiction that it has no least element.
Then clearly $0\notin M$.
Let $n\in N$. Suppose for inductive hypothesis that for all $k\le n$, $k\notin M$.
Then if $S(n)\in M$, it would be the least element of $M$.
Thus for all $k\le S(n)$, $k\notin M$.
By induction, for all $n\in N$, for all $k\le n$, $k\notin M$.
But then $M=\emptyset$, a contradiction.
Hence $M$ has a least element.
$\blacksquare$
Lemma.
For all $m,n\in N$, if $m\lt n$, then $S(m)\le n$.
(show proof)
Proof.
Fix $m,n\in N$, suppose $m\lt n$ and $\neg(S(m)\le n)$, then neither $S(m)\in n$ nor $S(m)=n$,
but we have exactly one of $S(m)\in n$, $n\in S(m)$, $S(m)=n$, so we have $n\in S(m)$,
then either $n\in m$ or $n=m$, but then we already have $m\in n$, a contradiction.
Hence we have either $\neg(m\lt n)$ or $S(m)\le n$, which is just "$m\lt n$ implies $S(m)\le n$".
Hence for all $m,n\in N$, if $m\lt n$, then $S(m)\le n$.
$\blacksquare$
Recursion theorem
For arbitrary sets $X,a,f$, if $a\in X$ and $f:X\to X$,
then there exists a unique function $u:N\to X$ such that $u(0)=a$ and for every $n\in N$, $u(S(n))=f(u(n))$.
(show proof)
Proof.
Consider $\{A\in\mathcal P(N\times X)|(((0,a)\in A)\land\forall n\forall x(((n,x)\in A)\to((S(n),f(x))\in A)))\}$, denoted $I$.
Clearly $N\times X$ is in $I$, so $I$ is non-empty.
So we can define $u$ to be $\cap I$, then $u$ is a subset of $N\times X$,
and clearly,
- $(0,a)\in u$, and
- $(n,x)\in u$ implies $(S(n),f(x))\in u$.
Now consider $\{n\in N|\exists!x((n,x)\in u)\}$, denoted $C$.
Suppose $0\notin C$, since $(0,a)\in u$, there exists some $b\neq a$ such that $(0,b)\in u$.
Denote $u\setminus\{(0,b)\}$ by $u'$. Since $(0,a)\in u$ and $(0,a)\notin\{(0,b)\}$,
$(0,a)\in u'$; if $(n,x)\in u'$, then $(n,x)\in u$, so $(S(n),f(x))\in u$,
but then, since $n\in N$, $S(n)\neq0$, so $(S(n),f(x))\notin\{(0,b)\}$, and hence $(S(n),f(x))\in u'$.
We have shown that $u'\in I$, so $u\subseteq u'$, a contradiction.
Therefore, $0\in C$.
Suppose there exists some $n^*\in C$ such that $S(n^*)\notin C$,
then $n^*\in N$ and for some unique $x^*$ we have $(n^*,x^*)\in u$, thus $(S(n^*),f(x^*))\in u$.
Since $S(n^*)\in N$, in order for $S(n^*)$ to not be in $C$, there has to be some $y\neq f(x^*)$,
such that $(S(n^*),y)\in u$. Denote $u\setminus\{(S(n^*),y)\}$ by $u'$.
Since $(0,a)\in u$ and $(0,a)\notin\{(S(n^*),y)\}$, $(0,a)\in u'$.
If $(n,x)\in u'$, then $(n,x)\in u$, so $(S(n),f(x))\in u$.
- Suppose $n=n^*$, then $x=x^*$ by uniqueness, so $f(x)\neq y$.
- Suppose $n\neq n^*$, since $S$ is injective, we have $S(n)\neq S(n^*)$.
In both cases we have $(S(n),f(x))\notin\{(S(n^*),y)\}$,
and we conclude that $(S(n),f(x))\in u'$.
We have shown that $u'\in I$, so $u\subseteq u'$, a contradiction.
Therefore, $n\in C$ implies $S(n)\in C$.
And we have that for all $n\in N$, $n\in C$ implies $S(n)\in C$.
By induction, for all $n\in N$, $n\in C$.
Since $u$ is a subset of $N\times X$, and for all $n\in N$, there exists a unique $x$ such that $(n,x)\in u$,
$u$ is a function from $N$ to $X$.
Since $(0,a)\in u$, we have $u(0)=a$.
let $n\in N$, then $(n,u(n))\in u$, thus $(S(n),f(u(n)))\in u$, implying $u(S(n))=f(u(n))$.
Now suppose $u'$ is a function from $N$ to $X$ such that $u'(0)=a$ and for all $n\in N$, $u'(S(n))=f(u'(n))$.
Then $u'(0)=a=u(0)$, and given $n\in N$, if $u'(n)=u(n)$, then $u'(S(n))=f(u'(n))=f(u(n))=u(S(n))$.
Thus by induction, for all $n\in N$, $u'(n)=u(n)$. Hence $u'=u$.
$\blacksquare$
Addition of natural numbers
For every natural number $m$, by recursion theorem we can define a function $S_m:N\to N$
such that $S_m(0)=m$ and for every $n\in N$, $S_m(S(n))=S(S_m(n))$.
Then the formula $\forall a\forall b((x=(a,b))\to(y=S_a(b)))$ defines a function $+:(N\times N)\to N$.
Given natural numbers $m,n$, we denote $+((m,n))$ by $m+n$.
Note that $m+n=S_m(n)$, thus $m+S(n)=S(m+n)$.
Proposition.
$0$ is an additive identity for natural numbers: for all $n\in N$, $n+0=n$ and $0+n=n$.
(show proof)
Proof.
Suppose $n\in N$, we immediately have $$n+0=S_n(0)=n$$
So for all $n\in N$, we have $n+0=S_n(0)=n$.
For the other equality, we use induction.
For base case, we have $$0+0=0$$
For inductive step, suppose $n\in N$ and $0+n=n$, then
$$0+S(n)=S(0+n)=S(n)$$
By induction, for all $n\in N$, we have $0+n=n$.
$\blacksquare$
Proposition.
Addition of natural numbers is associative: for all $m,n,k\in N$, $(m+n)+k=m+(n+k)$,
and commutative: for all $m,n\in N$, $m+n=n+m$.
(show proof)
Proof.
Fix $m,n\in N$.
For base case, we have $$(m+n)+0=m+n=m+(n+0)$$
For inductive step, suppose $k\in N$ and $(m+n)+k=m+(n+k)$, then
$$(m+n)+S(k)=S((m+n)+k)=S(m+(n+k))=m+S(n+k)=m+(n+S(k))$$
By induction, for all $k\in N$, we have $(m+n)+k=m+(n+k)$.
Hence for all $m,n,k\in N$, we have $(m+n)+k=m+(n+k)$.
This proves associativity.
For base case, suppose $n\in N$, we have $$0+n=n=n+0$$
So for all $n\in N$ we have $0+n=n+0$.
The inductive step itself requires an induction, as follows.
Suppose $m\in N$ and for all $n\in N$ we have $m+n=n+m$,
for base case of the inner induction,
we have $$S(m)+0=S(m)=0+S(m)$$
For inductive step of the inner induction, suppose $n\in N$ and $S(m)+n=n+S(m)$, then
$$S(m)+S(n)=S(S(m)+n)=S(n+S(m))=S(S(n+m))=S(S(m+n))=S(m+S(n))=S(S(n)+m)=S(n)+S(m)$$
By induction, for all $n\in N$, we have $S(m)+n=n+S(m)$.
Note that we are working under the assumption that $m\in N$ and for all $n\in N$ we have $m+n=n+m$.
We have shown that $m\in N$ and for all $n\in N$ we have $m+n=n+m$ together imply for all $n\in N$ we have $S(m)+n=n+S(m)$.
This completes the inductive step.
By induction, for all $m\in N$, for all $n\in N$, we have $m+n=n+m$.
Hence for all $m,n\in N$, we have $m+n=n+m$.
This proves commutativity.
$\blacksquare$
Proposition.
For all $m,n,k\in N$, if $m\lt n$, then $m+k\lt n+k$ and $k+m\lt k+n$.
(show proof)
Proof.
Fix $m,n\in N$.
For base case, if $m\lt n$,
since $m+0=m=0+m$ and $n+0=n=0+n$, we have that
$m+0\lt n+0$ and $0+m\lt 0+n$.
So if $m\lt n$, then $m+0\lt n+0$ and $0+m\lt 0+n$.
For inductive step, suppose $k\in N$ and if $m\lt n$, then $m+k\lt n+k$ and $k+m\lt k+n$.
If $m\lt n$, we have $m+k\lt n+k$ by inductive hypothesis, thus $S(m+k)\le n+k\lt S(n+k)$.
Since $S(m+k)=m+S(k)$ and $S(n+k)=n+S(k)$,
we have $m+S(k)\lt n+S(k)$; since $m+S(k)=S(k)+m$ and $n+S(k)=S(k)+n$,
we also have $S(k)+m\lt S(k)+n$.
By induction, we have that for all $k\in N$, if $m\lt n$, then $m+k\lt n+k$ and $k+m\lt k+n$.
Hence, for all $m,n,k\in N$, if $m\lt n$, then $m+k\lt n+k$ and $k+m\lt k+n$.
$\blacksquare$
Proposition.
For all $m,n,k\in N$, $m+n=0$ if and only if $m=0$ and $n=0$.
(show proof)
Proof.
Suppose $m+n=0$. If $m\neq0$, then $m\gt0$, thus $m+n\gt0+n=n\ge0$, a contradiction.
If $n\neq0$, then $n\gt0$, thus $m+n\gt m+0=m\ge0$, a contradiction.
The other direction is trivial.
$\blacksquare$
Proposition.
For all $m,n\in N$, if $m\le n$, then there exists a unique $k\in N$ such that $m+k=n$.
(show proof)
Proof.
Fix $m\in N$.
For base case, if $m\le0$, then $m=0$, thus $m+0=0+0=0$.
If $m+k=0$ for some $k\in N$, then $k=m+k=0$.
For inductive step, suppose $n\in N$ and if $m\le n$, then there exists a unique $k\in N$ such that $m+k=n$.
If $m\le S(n)$, then either $m=S(n)$ or $m\le n$.
- If $m=S(n)$, then $m+0=S(n)$. If $m+k=S(n)$ for some $k\in N$, then $m+k=m+0$, implying $k=0$.
- If $m\le n$, then there exists a unique $k\in N$ such that $m+k=n$.
Thus $m+S(k)=S(m+k)=S(n)$.
If $m+l=S(n)$ for some $l\in N$, then $m+l=m+S(k)$, implying $l=S(k)$.
Thus if $m\le S(n)$, then there exists a unique $k\in N$ such that $m+k=S(n)$.
By induction, for all $n\in N$, then there exists a unique $k\in N$ such that $m+k=n$.
$\blacksquare$
Subtraction on natural numbers
For all $p\in\{u\in N\times N|\exists m,n\in N,m\ge n\land u=(m,n)\}$, denoted $D$, there exists a unique $k\in N$ such that
there exist $m,n\in N$ such that $p=(m,n)$ and $n+k=m$.
Thus we can define a function $-:D\to N$ by the formula "there exist $m,n\in N$ such that $p=(m,n)$ and $n+k=m$" with $p$ as input and $k$ as output.
Then given $m,n\in N$ such that $m\ge n$, $(m,n)\in D$, and we have $n+-((m,n))=m$.
If we denote $-((m,n))$ by $m-n$, then we have $n+(m-n)=m$.
Multiplication of natural numbers
For every natural number $m$, by recursion theorem we can define a function $P_m:N\to N$
such that $P_m(0)=0$ and for every $n\in N$, $P_m(S(n))=S_m(P_m(n))$.
Then the formula $\forall a\forall b((x=(a,b))\to(y=P_a(b)))$ defines a function $\times:(N\times N)\to N$.
Given natural numbers $m,n$, we denote $\times((m,n))$ by $m\times n$, or simply $mn$.
Note that $mn=P_m(n)$, thus $mS(n)=m+(mn)$.
Note.
By default, multiplication has priority over addition.
Thus expressions like $m+mn$ is equivalent to $m+(mn)$.
Proposition.
For natural numbers, multiplication with $0$ equals $0$: for all $n\in N$, $n0=0$ and $0n=0$.
(show proof)
Proof.
Suppose $n\in N$, we immediately have $$n0=P_n(0)=0$$
So for all $n\in N$, we have $n0=0$.
For the other equality, we use induction.
For base case, we have $$0\times 0=0$$
For inductive step, suppose $n\in N$ and $0n=0$, then
$$0S(n)=0+0n=0+0=0$$
By induction, for all $n\in N$, we have $0n=0$.
$\blacksquare$
Proposition.
$1$ is an multiplicative identity for natural numbers: for all $n\in N$, $n1=n$ and $1n=n$.
(show proof)
Proof.
Suppose $n\in N$, we have $$n1=nS(0)=n+n0=n+0=n$$
So for all $n\in N$, we have $n1=n$.
For the other equality, we use induction.
For base case, we have $$1\times 0=0$$
For inductive step, suppose $n\in N$ and $1n=n$, then
$$1S(n)=1+1n=1+n=n+1=n+S(0)=S(n+0)=S(n)$$
By induction, for all $n\in N$, we have $1n=n$.
$\blacksquare$
Proposition.
Multiplication distributes over addition for natural numbers: for all $m,n,k\in N$, $m(n+k)=mn+mk$ and $(m+n)k=mk+nk$.
(show proof)
Proof.
Fix $m,n\in N$.
For base case, we have $$m(n+0)=mn=mn+0=mn+m0$$
For inductive step, suppose $k\in N$ and $m(n+k)=mn+mk$, then
$$m(n+S(k))=mS(n+k)=m+m(n+k)=m+(mn+mk)=(m+mn)+mk=(mn+m)+mk=mn+(m+mk)=mn+mS(k)$$
By induction, for all $k\in N$, we have $m(n+k)=mn+mk$.
Fix $m,n\in N$.
For base case, we have $$(m+n)0=0=0+0=m0+n0$$
For inductive step, suppose $k\in N$ and $(m+n)k=mk+nk$, then
$$(m+n)S(k)=(m+n)+(m+n)k=(m+n)+(mk+nk)=(n+m)+(mk+nk)=((n+m)+mk)+nk=(n+(m+mk))+nk=((m+mk)+n)+nk=(m+mk)+(n+nk)=mS(k)+nS(k)$$
By induction, for all $k\in N$, we have $(m+n)k=mk+nk$.
$\blacksquare$
Proposition.
Multiplication of natural numbers is associative: for all $m,n,k\in N$, $(mn)k=m(nk)$,
and commutative: for all $m,n\in N$, $mn=nm$.
(show proof)
Proof.
Fix $m,n\in N$.
For base case, we have $$(mn)0=0=m0=m(n0)$$
For inductive step, suppose $k\in N$ and $(mn)k=m(nk)$, then
$$(mn)S(k)=mn+(mn)k=mn+m(nk)=m(n+nk)=m(nS(k))$$
By induction, for all $k\in N$, we have $(mn)k=m(nk)$.
Hence for all $m,n,k\in N$, we have $(mn)k=m(nk)$.
This proves associativity.
For base case, suppose $n\in N$, we have $$0n=0=n0$$
So for all $n\in N$ we have $0n=n0$.
The inductive step itself requires an induction, as follows.
Suppose $m\in N$ and for all $n\in N$ we have $mn=nm$,
for base case of the inner induction,
we have $$S(m)0=0=0S(m)$$
For inductive step of the inner induction, suppose $n\in N$ and $S(m)n=nS(m)$, then
$$S(m)S(n)=S(m)+S(m)n=S(m)+nS(m)=nS(m)+S(m)=nS(m)+1S(m)=(n+1)S(m)=(n+S(0))S(m)=S(n+0)S(m)=S(n)S(m)$$
By induction, for all $n\in N$, we have $S(m)n=nS(m)$.
Note that we are working under the assumption that $m\in N$ and for all $n\in N$ we have $mn=nm$.
We have shown that $m\in N$ and for all $n\in N$ we have $mn=nm$ together imply for all $n\in N$ we have $S(m)n=nS(m)$.
This completes the inductive step.
By induction, for all $m\in N$, for all $n\in N$, we have $mn=nm$.
Hence for all $m,n\in N$, we have $mn=nm$.
This proves commutativity.
$\blacksquare$
Proposition.
For all $m,n,k\in N$, if $k\neq0$ and $m\lt n$, then $mk\lt nk$ and $km\lt kn$.
(show proof)
Proof.
Fix $m,k\in N$ such that $k\neq0$.
For base case, if $m\lt 0$, we trivially have $mk\lt 0k$ and $km\lt k0$.
For inductive step, suppose $n\in N$ and if $m\lt n$, then $mk\lt nk$ and $km\lt kn$.
If $m\lt S(n)$, then $m\le n$, thus $km=mk\le nk\lt k+nk=k+kn=kS(n)=S(n)k$.
By induction, for all $n\in N$, if $m\lt n$, then $mk\lt nk$ and $km\lt kn$.
$\blacksquare$
Proposition.
For all $m,n\in N$, $mn=0$ if and only if $m=0$ or $n=0$.
(show proof)
Proof.
If $m\neq0$ and $n\neq0$, then $n\gt0$, thus $mn\gt m0=0$, implying $mn\neq0$.
Hence if $mn=0$ then $m=0$ or $n=0$.
The other direction is trivial.
$\blacksquare$
Proposition.
For all $m,n\in N$, if $n\neq0$, then there exists a unique pair of natural numbers $q,r$ such that $r\lt n$ and $m=nq+r$.
(show proof)
Proof.
Fix $n\in N$ such that $n\neq0$.
For base case, we have $0\lt n$ and $0=n0+0$.
For inductive step, suppose $m\in N$ and there exists a pair of natural numbers $q,r$ such that $r\lt n$ and $m=nq+r$.
Then $S(r)\le n$.
- If $S(r)\lt n$, then $S(r)\lt n$ and $S(m)=S(nq+r)=nq+S(r)$.
- If $S(r)=n$, then $0\lt n$ and $S(m)=nq+S(r)=nq+n=nS(q)+0$.
By induction, for all $m\in N$, there exists a pair of natural numbers $q,r$ such that $r\lt n$ and $m=nq+r$.
Given $m,n\in N$ such that $n\neq0$, if for some $q,r,q',r'\in N$, we have $r\lt n$, $m=nq+r$, $r'\lt n$, and $m=nq'+r'$,
then $nq+r=nq'+r'$.
Assume $q\gt q'$, then $q'+(q-q')=q$, thus $q-q'\gt0$ and $nq=nq'+n(q-q')$, implying $n(q-q')\gt0$ and hence $nq\gt nq'$.
If $r\ge r'$, then $nq+r\ge nq+r'\gt nq'+r'$, a contradiction.
Thus $r\lt r'$. Then $r'=r+(r'-r)$, and we have $(nq'+r)+n(q-q')=nq+r=nq'+r'=(nq'+r)+(r'-r)$, implying $n(q-q')=r'-r$.
Since $q-q'\gt0$, we have $q-q'\ge1$, thus $n(q-q')\ge n1=n\gt r'\ge r'-r$, a contradiction.
By a symmetric argument, $q\lt q'$ also leads to a contradiction.
Hence $q=q'$. Then we have $nq=nq'$, thus $r=r'$.
$\blacksquare$
Division of natural numbers
For all $p\in N\times(N\setminus\{0\})$, there exists a unique $s\in N\times N$ such that there exist $m,n,q,r\in N$ such that
$p=(m,n)$, $s=(q,r)$, $r\lt n$, and $m=nq+r$.
Thus we can define a function $\divsymbol:N\times(N\setminus\{0\})\to N\times N$ by the formula
"there exist $m,n,q,r\in N$ such that $p=(m,n)$, $s=(q,r)$, $r\lt n$, and $m=nq+r$" with $p$ as input and $s$ as output.
Note that we can define a function that maps a pair of natural numbers $p$ to the first element, denoted $p_0$,
and a function that maps a pair of natural numbers $p$ to the second element, denoted $p_1$.
We call the composite function $p\mapsto\divsymbol(p)_0$ natural number division and
the composite function $p\mapsto\divsymbol(p)_1$ modulo operation.
Given natural number $m$ and non-zero natural number $n$, we denote $\divsymbol((m,n))_0$ by $m\divsymbol n$ and $\divsymbol((m,n))_1$ by $m\bmod n$,
which are called the quotient and remainder of the division of $m$ by $n$.
Then we have $m\bmod n\lt n$ and $m=n(m\divsymbol n)+(m\bmod n)$.
Proposition.
For all $m\in N$ and $n\in N\setminus\{0\}$, $mn\divsymbol n=m$ and $mn\bmod n=0$.
(show proof)
Proof.
Trivial.
$\blacksquare$
Proposition.
For all $k,m\in N$ and $n\in N\setminus\{0\}$,
- $(m\bmod n)\bmod n=m\bmod n$;
- $(m+k)\bmod n=((m\bmod n)+(k\bmod n))\bmod n$;
- $(mk)\bmod n=((m\bmod n)(k\bmod n))\bmod n$.
(show proof)
Proof.
Since $m\bmod n\lt n$ and $m\bmod n=n0+m\bmod n$, we have $(m\bmod n)\bmod n=m\bmod n$.
Since $m=n(m\divsymbol n)+(m\bmod n)$ and $k=n(k\divsymbol n)+(k\bmod n)$,
we have $$m+k=n((m\divsymbol n)+(k\divsymbol n))+((m\bmod n)+(k\bmod n))$$
Since $$(m\bmod n)+(k\bmod n)=n(((m\bmod n)+(k\bmod n))\divsymbol n)+(((m\bmod n)+(k\bmod n))\bmod n)$$
and $((m\bmod n)+(k\bmod n))\bmod n\lt n$,
we have $(m+k)\bmod n=((m\bmod n)+(k\bmod n))\bmod n$.
Since $m=n(m\divsymbol n)+(m\bmod n)$ and $k=n(k\divsymbol n)+(k\bmod n)$,
we have $$mk=n(n(m\divsymbol n)(k\divsymbol n)+(m\divsymbol n)(k\bmod n)+(m\bmod n)(k\divsymbol n))+(m\bmod n)(k\bmod n)$$
Since $$(m\bmod n)(k\bmod n)=n(((m\bmod n)(k\bmod n))\divsymbol n)+(((m\bmod n)(k\bmod n))\bmod n)$$
and $((m\bmod n)(k\bmod n))\bmod n\lt n$,
we have $(mk)\bmod n=((m\bmod n)(k\bmod n))\bmod n$.
$\blacksquare$
Proposition.
For all $k,m\in N$ and $n\in N\setminus\{0\}$, if $k\lt m$, $k\divsymbol n\le m\divsymbol n$.
(show proof)
Proof.
If $k\lt m$, then for some $l\in N$, we have $k+l=m$.
Thus $$
(n(k\divsymbol n)+(k\bmod n))+(n(l\divsymbol n)+(l\bmod n))
=k+l
=m
=n(m\divsymbol n)+((k+l)\bmod n)
=n(m\divsymbol n)+((k\bmod n)+(l\bmod n))\bmod n$$
Since $$(k\bmod n)+n(l\divsymbol n)+(l\bmod n)\ge(k\bmod n)+(l\bmod n)\ge((k\bmod n)+(l\bmod n))\bmod n$$
we have $n(k\divsymbol n)\le n(m\divsymbol n)$.
Since $n\neq0$, we have $k\divsymbol n\le m\divsymbol n$.
$\blacksquare$
Exponentiation of natural numbers
For every natural number $m$, by recursion theorem we can define a function $E_m:N\to N$
such that $E_m(0)=1$ and for every $n\in N$, $E_m(S(n))=P_m(E_m(n))$.
Then the formula $\forall a\forall b((x=(a,b))\to(y=E_a(b)))$ defines a function $\wedge:(N\times N)\to N$.
Given natural numbers $m,n$, we denote $\wedge((m,n))$ by $m\wedge n$, or simply $m^n$.
Note that $m^n=E_m(n)$, thus $m^{S(n)}=m(m^n)$.
Note.
By default, exponentiation has priority over multiplication.
Thus expressions like $mm^n$ is equivalent to $m(m^n)$.
Note.
With this definition, $0^0=1$.
Proposition.
For all $k\in N$, $1^k=1$.
(show proof)
Proof.
For base case, $1^0=E_1(0)=1$.
For inductive step, suppose $k\in N$ and $1^k=1$, then
$1^{S(k)}=1\times 1^k=1\times 1=1$.
By induction, for all $k\in N$, $1^k=1$.
$\blacksquare$
Proposition.
Exponentiation of natural numbers has the following properties: for all $m,n,k\in N$,
- $(mn)^k=m^kn^k$
- $m^{n+k}=m^nm^k$
- $m^{nk}={(m^n)}^k$
(show proof)
Proof.
The first equation is proven as follows.
Fix $m,n\in N$.
For base case, we have $$(mn)^0=1=1\times 1=m^0n^0$$
For inductive step, suppose $k\in N$ and $(mn)^k=m^kn^k$, then
$$(mn)^{S(k)}=(mn)(mn)^k=(mn)(m^kn^k)=(nm)(m^kn^k)=((nm)m^k)n^k=(n(mm^k))n^k=((mm^k)n)n^k=(mm^k)(nn^k)=m^{S(k)}n^{S(k)}$$
By induction, for all $k\in N$, we have $(mn)^k=m^kn^k$.
Hence for all $m,n,k\in N$, we have $(mn)^k=m^kn^k$.
The second equation is proven as follows.
Fix $m,n\in N$.
For base case, we have $$m^{n+0}=m^n=m^n1=m^nm^0$$
For inductive step, suppose $k\in N$ and $m^{n+k}=m^nm^k$, then
$$m^{n+S(k)}=m^{S(n+k)}=mm^{n+k}=m(m^nm^k)=(mm^n)m^k=(m^nm)m^k=m^n(mm^k)=m^nm^{S(k)}$$
By induction, for all $k\in N$, we have $m^{n+k}=m^nm^k$.
Hence for all $m,n,k\in N$, we have $m^{n+k}=m^nm^k$.
The third equation is proven as follows.
Fix $m,n\in N$.
For base case, we have $$m^{n0}=m^0=1={(m^n)}^0$$
For inductive step, suppose $k\in N$ and $m^{nk}={(m^n)}^k$, then
$$m^{nS(k)}=m^{n+nk}=m^nm^{nk}=(m^n){(m^n)}^k={(m^n)}^{S(k)}$$
By induction, for all $k\in N$, we have $m^{nk}={(m^n)}^k$.
Hence for all $m,n,k\in N$, we have $m^{nk}={(m^n)}^k$.
$\blacksquare$
Proposition.
For all $m,n\in N$, $m^n=0$ if and only if $m=0$ and $n\neq0$.
(show proof)
Proof.
Suppose $m\in N\setminus\{0\}$. Then $m^0=1\neq0$ and suppose $n\in N$ and $m^n\neq0$,
then $m^{S(n)}=mm^n\neq0$. By induction, for all $n\in N$, $m^n\neq0$.
If $m\in N$ and $n=0$, we have $m^n=1\neq0$.
We have shown that given $m,n\in N$, if $m^n=0$ then $m=0$ and $n\neq0$.
Suppose $m=0$. For base case, if $0\neq0$ then $m^0=0$.
Suppose $n\in N$ and if $n\neq0$ then $m^n=0$.
Then $m^{S(n)}=mm^n=0$.
By induction, for all $n\in N$, if $n\neq0$ then $m^n=0$.
We have shown that given $m,n\in N$, if $m=0$ and $n\neq0$ then $m^n=0$.
$\blacksquare$
Proposition.
For all $m,n,k\in N$, if $k\neq0$ and $m\lt n$, then $m^k\lt n^k$.
(show proof)
Proof.
Fix $m,n\in N$ such that $m\lt n$.
For base case, if $0\neq0$, then $m^0\lt n^0$.
For inductive step, suppose $k\in N$ and if $k\neq0$, then $m^k\lt n^k$.
Then $m^k\le n^k$.
Since $m\lt n$, $n\neq0$, thus $n^k\neq0$.
Then we have $m^{S(k)}=mm^k\le mn^k\lt nn^k=n^{S(k)}$.
By induction, for all $k\in N$, if $k\neq0$, then $m^k\lt n^k$.
$\blacksquare$
Proposition.
For all $m,n,k\in N$, if $k\gt 1$ and $m\lt n$, then $k^m\lt k^n$.
(show proof)
Proof.
Fix $m,k\in N$ such that $k\gt 1$.
For base case, if $m\lt 0$, then $k^m\lt k^0$.
For inductive step, suppose $n\in N$ and if $m\lt n$, then $k^m\lt k^n$.
If $m\lt S(n)$, then $m\le n$, thus $k^m\le k^n$.
Since $k\neq0$, $k^n\neq0$, thus $k^n\lt kk^n=k^{S(n)}$.
By induction, for all $n\in N$, if $m\lt n$, then $k^m\lt k^n$.
$\blacksquare$
Tuple
Given a set $X$ and a natural number $n$,
we call a function from $n$ to $X$ an $n$-tuple of $X$.
Note that the set $\mathcal P(n\times X)$ contains every $n$-tuple of $X$,
hence the collection of all $n$-tuples of $X$ is a set, denoted $X^n$.
Given an $n$-tuple $t$ of $X$ and a natural number $k\lt n$,
we usually denote $t(k)$ by $t_k$, and we may denote $t$ as $(t_0,\ldots,t_{n-1})$.
Note that an $n$-tuple $t$ of $X$ may also refer to a function from $\{1,\ldots,n\}$ to $X$,
in which case we say $t$ is an $n$-tuple with indexes shifted by $1$,
and we may write $t$ as $(t_1,\ldots,t_n)$.
Sequence
Given a set $X$, we call a function from $N$ to $X$ a sequence of $X$.
Note that the set $\mathcal P(N\times X)$ contains every sequence of $X$,
hence the collection of all sequences of $X$ is a set.
Given a sequence $s$ of $X$ and a natural number $n\in N$,
we usually denote $s(n)$ by $s_n$, and we may denote $s$ as $(s_n)_{n\in N}$ or just $(s_n)$.
Note that a sequence $s$ of $X$ may also refer to a function from $N^+$, the non-zero natural numbers, to $X$,
in which case we say $s$ is a sequence with indexes shifted by $1$,
and we may write $s$ as $(s_n)_{n\in N^+}$.
Infinity
Given a set $X$,
if there exists $n\in N$, such that there exists a bijection from $n$ to $X$,
then we say the cardinality of $X$, denoted $|X|$, is $n$, and we say $X$ is finite,
otherwise we say $X$ is infinite.
If either $X$ is finite or there exists a bijection from $N$ to $X$,
we say $X$ is countable, otherwise we say $X$ is uncountable.
Proposition.
A finite set has a unique cardinality in $N$.
(show proof)
Proof.
We will first show that, if $m,n$ are natural numbers, then there is a bijection between $m$ and $n$ if and only if $m=n$.
Clearly, $\emptyset$, as an empty function, is a bijection between $0$ and $0$.
Suppose $n\neq0$, then $n$ is not empty, so there is no bijection between $0$ and $n$.
We have that, as a base case for induction, there is a bijection between $0$ and $n$ if and only if $n=0$.
Now take as inductive hypothesis that for all natural number $k\le m$, there is a bijection between $k$ and $n$ if and only if $n=k$.
Then for all $n\le m$, there is no bijection between $m+1$ and $n$.
Trivially, there is a bijection between $m+1$ and $m+1$.
The only case remaining is between $m+1$ and $n$ such that $n\gt m+1$.
Suppose $f$ is a bijection from $m+1$ to $n$ with $n\gt m+1$.
Then the restriction $f|_m$ of $f$ on $m$ is a bijection from $m$ to $n\setminus\{f(m)\}$.
Define $g:n-1\to n\setminus\{f(m)\}$ such that $g(k)=k$ if $k\lt f(m)$ and $g(k)=k+1$ otherwise,
then $g$ is clearly a bijection.
Thus, $g^{-1}\circ f|_m$ is a bijection from $m$ to $n-1$.
But $m\neq n-1$, so there is no bijection between $m$ and $n-1$, a contradiction.
Hence, there is no bijection between $m+1$ and $n$ such that $n\gt m+1$.
This concludes the inductive step.
And we have shown that, for all natural numbers $m,n$, there is a bijection between $m$ and $n$ if and only if $m=n$.
Suppose $X$ is a finite set.
Let $m,n$ be natural numbers such that there exist a bijection between $n$ and $X$ and a bijection between $m$ and $X$.
Then there is a bijection between $n$ and $m$, implying $m=n$.
We have shown that $X$ has a unique cardinality in $N$.
$\blacksquare$
Proposition.
No finite set has a bijection from $N$ to itself.
(show proof)
Proof.
We will first show that, for all natural number $n$, there is no bijection between $n$ and $N$.
Since $N$ is non-empty, there is no bijection between $0$ and $N$.
Take as inductive hypothesis that there is no bijection between $m$ and $N$.
Suppose there is a bijection $f$ from $m+1$ to $N$.
Then the restriction $f|_m$ of $f$ on $m$ is a bijection from $m$ to $N\setminus\{f(m)\}$.
Define $g:N\to N\setminus\{f(m)\}$ such that $g(k)=k$ if $k\lt f(m)$ and $g(k)=k+1$ otherwise,
then $g$ is clearly a bijection.
Thus, $g^{-1}\circ f|_m$ is a bijection from $m$ to $N$, a contradiction.
Hence, there is no bijection between $m+1$ and $N$.
This concludes the inductive step.
We have shown that for all natural number $n$, there is no bijection between $n$ and $N$.
Suppose $X$ is a finite set. Let $n=\abs{X}$.
If there exists a bijection between $N$ and $X$,
then there is a bijection between $n$ and $N$, a contradiction.
Therefore, no finite set has a bijection from $N$ to itself.
$\blacksquare$
Lemma.
Let $n\in N$, then for every subset $S$ of $n$, there exists $m\le n$ such that there is a bijection from $m$ to $S$.
(show proof)
Proof.
The base case for $0$ is trivial.
Now suppose for every subset $S$ of $n$, there exists $m\le n$ such that there is a bijection from $m$ to $S$.
Then for every subset $S'$ of $n+1$, either $n\in S'$ or $n\notin S'$.
If $n\notin S'$, then $S'$ is a subset of $n$, so there exists $m\le n\lt n+1$ such that there is a bijection from $m$ to $S'$.
If $n\in S'$, then $S'\setminus\{n\}$ is a subset of $n$, so there exists $m\le n$ such that there is a bijection $f$ from $m$ to $S'\setminus\{n\}$.
Define $f':m+1\to S'$ by $f'(k)=f(k)$ if $k\in m$ and $f'(m)=n$,
then $f'$ is a bijection from $m+1$ to $S'$. Note that $m+1\le n+1$.
By induction, for all $n\in N$, for every subset $S$ of $n$, there exists $m\le n$ such that there is a bijection from $m$ to $S$.
$\blacksquare$
Proposition.
Suppose $\abs{A}=n$ for some $n\in N$ and $B\subseteq A$, then there exists $m\le n$ such that $\abs{B}=m$, and $\abs{A\setminus B}=n-m$.
(show proof)
Proof.
Let $f_A$ be a bijection from $n$ to $A$,
Let $S$ be the preimage of $f_A$ on $B$, then $S$ is a subset of $n$,
so there exists $m\le n$ such that there is a bijection $f_S$ from $m$ to $S$.
Now define $f:m\to B$ by $f(k)=(f_A\circ f_S)(k)$,
then $f$ is a bijection from $m$ to $B$.
Note that there also exists $l\le n$ such that there is a bijection $f_{n\setminus S}$ from $l$ to $n\setminus S$.
Define $g:l\to A\setminus B$ by $g(k)=(f_A\circ f_{n\setminus S})(k)$, then $g$ is a bijection from $l$ to $A\setminus B$.
Define $h:m+l\to n$ by:
- if $k\in m$, then $h(k)=(f_A^{-1}\circ f)(k)$;
- if $k\notin m$, then $h(k)=(f_A^{-1}\circ g)(k-m)$.
Then $h$ is a bijection. Hence $n=m+l$, or $l=n-m$.
$\blacksquare$
Proposition.
Suppose $\abs{A}=n$ and $\abs{B}=m$ for some $n,m\in N$, then $$\abs{A\cup B}=\abs{A}+\abs{B}-\abs{A\cap B}$$
(show proof)
Proof.
Let $f_A$ be a bijection from $n$ to $A$ and $f_B$ be a bijection from $m$ to $B$,
then there exists $l\le m$ such that there exists a bijection $f_{A\cap B}$ from $l$ to $A\cap B$,
and there exists a bijection $f_{A\setminus B}$ from $n-l$ to $A\setminus B$.
Now define $f:m+(n-l)\to A\cup B$ by:
- if $k\in m$, then $f(k)=f_B(k)$;
- if $k\notin m$, then $h(k)=f_{A\setminus B}(k-m)$.
Then $f$ is a bijection. Hence $$\abs{A\cup B}=n+m-l=\abs{A}+\abs{B}-\abs{A\cap B}$$
$\blacksquare$
Repeated operation
Suppose we have a non-empty set $X$, a function $f:N\to X$, and an operation $\cdot:X\times X\to X$.
Then we can define a function $\mathscr F:N\times X\to N\times X$ by $\mathscr F((k,x))=(S(k),x\cdot f(S(k)))$.
Thus by recursion theorem, we can define a function $u:N\to N\times X$ such that $u(0)=(0,f(0))$ and $u(S(k))=\mathscr F(u(k))$.
Finally, we can define a function $F:N\to X$ that maps each $k$ to the second element of $u(k)$,
then $F(n)$ represents $f(0)\cdot\ldots\cdot f(n)$.
By induction, we can see that the first element of $u(n)$ is $n$ and $F(S(n))=F(n)\cdot f(S(k))$.
Note that this applies to repeated pairwise union or intersection as well.
Properties of repeated operations are usually provable by induction straightforwardly.
Note.
Let $\mathcal F$ be the meta-logical function that maps meta-logical natural numbers to corresponding terms.
By meta-logical induction, for all meta-logical natural number $n$, $\{\mathcal F(1),\ldots,\mathcal F(n)\}=\{1,\ldots,\mathcal F(n)\}$.
Also by meta-logical induction, given a formula $\varphi(x)$, for all non-zero meta-logical natural number $n$,
$\varphi(\mathcal F(1))\land\ldots\land\varphi(\mathcal F(n))$ is equivalent to $\varphi(j)$ for all $j\in\{\mathcal F(1),\ldots,\mathcal F(n)\}$.
Tuple without codomain
Let $n$ be a natural number.
An $n$-tuple without codomain is a function from $n$, or $1,\ldots,n$ if indexes are shifted by $1$.
A tuple without codomain can also be formed from a meta-logical tuple of terms.
By meta-logical induction, we have that for all meta-logical natural number $n$,
let $(t_1,\ldots,t_n)$ be a meta-logical tuple of terms,
then there exists a function $F$ from $\{\mathcal F(1),\ldots,\mathcal F(n)\}$ such that $(F(\mathcal F(1))=t_1)\land\ldots\land(F(\mathcal F(n))=t_n)$.
We denote this function as $(t_1,\ldots,t_n)$, which is a $\mathcal F(n)$-tuple without codomain,
and we call it a tuple of the sets $t_1,\ldots,t_n$.
Repeated Cartesian product
Let $X$ be an $n$-tuple without codomain.
Then $X_1\times\ldots\times X_n$ represents the set of $n$-tuples $T$ of $\bigcup_{j\in\{1,\ldots,n\}}X_j$
such that $T_j\in X_j$ for all $j\in\{1,\ldots,n\}$.
Suppose $n$ is a non-zero meta-logical natural number and
$(X_1,\ldots,X_n)$ is a tuple of the sets $X_1,\ldots,X_n$, let $T$ be an element of the repeated Cartesian product of $(X_1,\ldots,X_n)$, denoted $X_1\times\ldots\times X_n$,
then $(T_{\mathcal F(1)}\in X_1)\land\ldots\land(T_{\mathcal F(n)}\in X_n)$.
Conversely, suppose we have $x_1,\ldots,x_n$ such that $(x_1\in X_1)\land\ldots\land(x_n\in X_n)$,
then $(x_1,\ldots,x_n)\in X_1\times\ldots\times X_n$.
Proposition.
There is no infinite descending $\in$-sequence.
Formally, there is no set $X$ such that
- for all $x\in N$ there is exactly one $y$ such that $(x,y)\in X$, and
- for all $n\in N$, for all $a,b$ such that $(n,a),(S(n),b)\in X$, we have $b\in a$.
(show proof)
Proof.
Suppose for contradiction that such set $X$ exists.
By axiom schema of replacement, there exists a set $Y$ such that
for all $x\in N$ there is exactly one $y\in Y$ such that $(x,y)\in X$,
which defines a function $f:N\to Y$, such that for all $n\in N$, $(n,f(n))\in X$.
Thus given $n\in N$, we have $f(S(n))\in f(n)$.
Let $U$ be the range of $f$.
Then $U$ is clearly non-empty, thus by axiom of foundation,
Some $y\in U$ is disjoint from $U$.
Since $y\in U$, some $n\in N$ has $f(n)=y$.
But then $f(S(n))\in y\cap U$, a contradiction.
$\blacksquare$
Relation
Given a set $S$ and a natural number $n$, an $n$-ary relation on $S$ is a subset of $S^n$.
By default, when we define a relation $\sim$ on $S$ it is implicitly assumed that $\sim$ is binary.
A subset of $S\times S$, instead of $S^2$, can also be regarded as a binary relation on $S$.
Given $a,b\in S$, we often denote $(a,b)\in \sim$ by $a\sim b$ and $(a,b)\notin \sim$ by $a\nsim b$.
A relation is often defined by $$\{u\in S\times S|\forall a,b\in S(u=(a,b)\to\varphi(a,b))\}$$
for some formula $\varphi(a,b)$,
then for all $a,b\in S$, $a\sim b$ if and only if $\varphi(a,b)$.
Hence, we often write "for all $a,b\in S$, $a\sim b$ if and only if $\varphi(a,b)$" to represent the definition above,
and we say that $\sim$ is defined by $\varphi$ with $a$ and $b$, in that order, as variables.
Note that $\gt,\lt,\ge,\le$ naturally define relations on natural numbers,
and their properties naturally transfer to their corresponding relations.
Partition
Given a set $X$, a partition of $X$ is a pairwise disjoint collection $S$ such that $\cup S=X$.
Definition.
We say a tuple $T$ is pairwise disjoint if and only if for all $i,j$ in domain of $T$,
if $T_i$ and $T_j$ are not disjoint, then $i=j$.
Indexed partition
Given a set $X$, an indexed partition of $X$ is a pairwise disjoint tuple $T$ such that $\cup_i T_i=X$.
Proposition.
Given sets $X$ and $Y$,
given an indexed partition $T$ of $X$,
and given a tuple $F$ that shares the same domain as $T$
and for each $i$ in domain of $T$, $F_i$ is a function from $T_i$ to $Y$,
then $\bigcup_i F_i$ is a function from $X$ to $Y$,
such that for all $j$ in domain of $T$, $\p{\bigcup_i F_i}|_{T_j}=F_j$.
(show proof)
Proof.
Denote the domain of $T$ by $D$.
Let $p\in\bigcup_i F_i$, then for some $i\in D$, $p\in F_i\subseteq T_i\times Y\subseteq X\times Y$.
Thus $\bigcup_i F_i\subseteq X\times Y$.
Let $x\in X$, then for some $i\in D$, $x\in T_i$, thus $(x,F_i(x))\in F_i\subseteq\bigcup_i F_i$.
If $(x,y)\in\bigcup_i F_i$, then for some $j\in D$, $(x,y)\in F_j$, thus $x\in T_j$, implying $T_i$ and $T_j$ are not disjoint, hence $i=j$.
Now we have $(x,y)\in F_i$, thus $y=F_i(x)$. Hence there exists a unique $y$ such that $(x,y)\in\bigcup_i F_i$.
We have shown that $\bigcup_i F_i$ is a function from $X$ to $Y$.
Let $j\in D$ and $x\in T_j$, then $(x,\p{\bigcup_i F_i}|_{T_j}(x))\in\p{\bigcup_i F_i}|_{T_j}\subseteq\bigcup_i F_i$.
Thus for some $i\in D$, $(x,\p{\bigcup_i F_i}|_{T_j}(x))\in F_i$, implying $x\in T_i$ and hence $i=j$.
Hence $(x,\p{\bigcup_i F_i}|_{T_j}(x))\in F_j$, and we have $\p{\bigcup_i F_i}|_{T_j}(x)=F_j(x)$.
We conclude that $\p{\bigcup_i F_i}|_{T_j}=F_j$.
$\blacksquare$
Equivalence relation
A relation $\sim$ on a set $S$ is called an equivalence relation when it has the following properties:
- 1. Reflexivity. $\forall x\in S(x\sim x)$
- 2. Symmetry. $\forall x,y\in S(x\sim y\to y\sim x)$
- 3. Transitivity. $\forall x,y,z\in S((x\sim y\land y\sim z)\to x\sim z)$
Given an equivalence relation $\sim$ on $S$ and $x\in S$, we denote $\{u\in S|u\sim x\}$ by $[x]$,
called an
equivalence class of $x$ with respect to $\sim$.
Then $\{[x]:x\in S\}$, the set of equivalence classes with respect to $\sim$, is a partition of $S$
(show proof).
Proof.
Suppose $U\in\{[x]:x\in S\}$, then for some $x\in S$, $U=[x]=\{u\in S|u\sim x\}$, and thus $U\subseteq S$.
Suppose $A,B\in\{[x]:x\in S\}$ and $A\cap B\neq\emptyset$.
Then for some $a\in S$, $A=[a]$, and for some $b\in S$, $B=[b]$.
Since $A\cap B$ is non-empty, there exists $c\in A\cap B=[a]\cap[b]$.
Then $c\sim a$ and $c\sim b$, and thus $a\sim b$.
Hence $A=[a]=[b]=B$.
Suppose $u\in\bigcup\{[x]:x\in S\}$, then for some $y\in\{[x]:x\in S\}$, $u\in y$, and for some $x\in S$, $y=[x]$.
Thus $u\in[x]\subseteq S$, implying $u\in S$.
Suppose $u\in S$, then $u\in[u]$ and $[u]\in\{[x]:x\in S\}$, thus $u\in\bigcup\{[x]:x\in S\}$.
$\blacksquare$
Partial order
Let $\preceq$ be a binary relation on a set $S$.
If $\preceq$ has the following properties:
- for all $x\in S$, $x\preceq x$;
- for all $x,y\in S$, if $x\preceq y$ and $y\preceq x$, then $x=y$;
- for all $x,y,z\in S$, if $x\preceq y$ and $y\preceq z$, then $x\preceq z$;
then $\preceq$ is called a partial order on $S$.
Total order
Let $(S,\preceq)$ be a partially ordered set.
If for all $x,y\in S$, either $x\preceq y$ or $y\preceq x$,
then $\preceq$ is called a total order on $S$.
Clearly, if we define $x\prec y$ by $x\preceq y$ and $x\neq y$,
then for all $x,y\in S$, we have exactly one of $x\prec y$, $x=y$, $y\prec x$.
Well-order
Let $(S,\preceq)$ be a totally ordered set.
If every non-empty subset $E$ of $S$ has a least element $x^*$ given by $\preceq$,
such that for all $x\in E$, $x^*\preceq x$,
then $\preceq$ is called a well-order on $S$.
Chain
Let $(S,\preceq)$ be a partially ordered set.
If $A\subseteq S$ such that $\preceq$ is a total order on $A$,
then $A$ is called a chain in $S$.
Choice function
Given any family $F$ of non-empty sets, a function $f:F\to\cup F$ such that for all $X\in F$, $f(X)\in X$ is called a choice function of $F$.
Note.
The formula listed as $ZF9$ is provable in $ZFW$
(show proof).
Proof.
Let $F$ be a family of pairwise disjoint non-empty sets.
Let $X\in F$, then $\exists x(x\in X)$.
Let $\mathcal F$ be a witness function defined by $\exists x(x\in X)$,
then $\mathcal F(X)\in X$.
Now consider the set $\{u\in\bigcup F|\exists Y((Y\in F)\land(u=\mathcal F(Y)))\}$.
Let $X\in F$, then $\mathcal F(X)\in X$, thus $\mathcal F(X)\in\bigcup F$ and $\exists Y((Y\in F)\land(\mathcal F(X)=\mathcal F(Y)))$,
and we have $\mathcal F(X)\in\{u\in\bigcup F|\exists Y((Y\in F)\land(u=\mathcal F(Y)))\}$.
If some set $z$ has $z\in X$ and $z\in\{u\in\bigcup F|\exists Y((Y\in F)\land(u=\mathcal F(Y)))\}$,
Then for some $Y\in F$, $z=\mathcal F(Y)$. Since $\mathcal F(Y)\in Y$, we have $z\in Y$.
Since $X,Y\in F$ and $z\in X\cap Y$, we have $X=Y$, thus $\mathcal F(X)=\mathcal F(Y)=z$.
Hence there exists a unique $x$ such that $x\in\{u\in\bigcup F|\exists Y((Y\in F)\land(u=\mathcal F(Y)))\}$ and $x\in X$,
implying that $x\in\{u\in\bigcup F|\exists Y((Y\in F)\land(u=\mathcal F(Y)))\}$
contains exactly one element in common with each of the sets in $F$.
$\blacksquare$
Axiom of choice
Every family of non-empty sets has a choice function
(show proof).
Proof.
Suppose $F$ is a set such that we have $\forall X(X\in F\to\exists x(x\in X))$.
Let $\mathcal F$ be a witness function defined by $\exists x(x\in X)$,
then we have $\exists x(x\in X)\to \mathcal F(X)\in X$.
If $X\in F$, then $\exists x(x\in X)$, implying $\mathcal F(X)\in X$, and thus $\mathcal F(X)\in\cup F$.
Thus we can define a function $f:F\to\cup F$ such that $f(X)=\mathcal F(X)$.
Since for all $X\in F$, $f(X)=\mathcal F(X)\in X$, $f$ is a choice function of $F$.
$\blacksquare$
From this point on, we will refer to this, instead of the one we gave above, as axiom of choice.
Note.
Suppose we have a formula of the form "for all $x\in X$ there exists $y\in Y$ such that $\varphi(x,y)$" where $Y$ is non-empty.
With $a$ as input and $b$ as output, the formula $b=\{u\in Y|\varphi(a,u)\}$
defines a function $\mathcal F$ from $X$ to $\mathcal P(Y)\setminus\{\emptyset\}$.
By axiom of choice, there exists a choice function $\mathcal C$ from $\mathcal P(Y)\setminus\{\emptyset\}$ to $Y$.
Then the composite function $\mathcal C\circ\mathcal F$ is a function from $X$ to $Y$,
and for all $c\in X$, we have $\varphi(c,(\mathcal C\circ\mathcal F)(c))$.
By "let $f:X\to Y$ be a function that maps every $x\in X$ to a $y\in Y$ such that $\varphi(x,y)$",
we are implicitly defining $f$ to be $\mathcal C\circ\mathcal F$.
This applies to similar formulas with unique existence as well.
Zorn's lemma
Let $(S,\preceq)$ be a non-empty partially ordered set.
If every chain $C$ in $S$ has an upper bound in $S$, an element $s\in S$ such that $c\preceq s$ for all $c\in C$,
then $S$ has a maximal element, an element $s^*\in S$ such that $s^*\preceq s$ implies $s^*=s$ for all $s\in S$.
(show proof)
Proof.
Let $(S,\preceq)$ be a non-empty partially ordered set.
Denote the set of all chains in $S$ by $\mathcal C$.
Then $(\mathcal C,\subseteq)$ is a partially ordered set.
Our main goal is to show that $S$ has a maximal chain,
a chain $C^*\in \mathcal C$ such that if $C^*\cup\{s\}$ is a chain then $s\in C^*$ for all $s\in S$.
By axiom of choice, there exists a choice function $f:\mathcal P(X)\setminus\{\emptyset\}\to X$.
For each chain $C\in\mathcal C$, denote $\{u\in X|u\notin C\land C\cup\{u\}\in\mathcal C\}$ by $C'$.
Then define a function $g:\mathcal C\to\mathcal C$ by
- $g(C)=C$ if $C'=\emptyset$, and
- $g(C)=C\cup\{f(C')\}$ if $C'\neq\emptyset$.
Now we can define towers $\mathcal T$ in $S$ as subsets of $\mathcal C$ with the following properties:
- (1) $\emptyset\in\mathcal T$;
- (2) for all $C$, $C\in\mathcal T$ implies $g(C)\in\mathcal T$;
- (3) if $\mathcal D\subseteq\mathcal T$ is a chain in $\mathcal C$, then $\cup\mathcal D\in\mathcal T$.
$\mathcal C$ is itself a tower in $S$: (1) and (2) are clearly satisfied.
For (3), suppose $\mathcal D\subseteq\mathcal T$ is a chain in $\mathcal C$,
if $a,b\in\cup\mathcal D$, then for some $A,B\in\mathcal D$ we have $a\in A$ and $b\in B$.
Since $\mathcal D$ is a chain in $\mathcal C$, either $A\subseteq B$ or $B\subseteq A$, so either $a,b\in A$ or $a,b\in B$.
Since $A$ and $B$ are both chains in $S$, we have $a\preceq b$ or $b\preceq a$.
We have shown that $\cup\mathcal D$ is a chain in $S$, so $\cup\mathcal D\in\mathcal C$.
Since there exists a tower in $S$, we can define $\mathcal T_0$ to be the intersection of all towers in $S$.
Then $\mathcal T_0$ is also a tower:
- (1) For each tower $\mathcal T$ in $S$, $\emptyset\in\mathcal T$, so $\emptyset\in\mathcal T_0$.
- (2) For all $C$, if $C\in\mathcal T_0$, then for each tower $\mathcal T$ in $S$, $C\in\mathcal T$,
so $g(C)\in\mathcal T$, therefore $g(C)\in\mathcal T_0$.
- (3) Suppose $\mathcal D\subseteq\mathcal T_0$ is a chain in $\mathcal C$,
then $\mathcal D\subseteq\mathcal T_0\subseteq\mathcal T$ for every tower $\mathcal T$ in $S$,
hence $\cup\mathcal D\in\mathcal T$, therefore $\cup\mathcal D\in\mathcal T_0$.
Our sub-goal is to show that $\mathcal T_0$ is a chain in $\mathcal C$.
Denote $\{A\in\mathcal T_0|\forall B\in\mathcal T_0,(A\subseteq B\lor B\subseteq A)\}$ by $\mathcal E$,
then $\mathcal E$ is a tower in $S$:
- (1) Since $\emptyset\in\mathcal T_0$ and for each $B\in\mathcal T_0$, $\emptyset\subseteq B$, we know $\emptyset\in\mathcal E$.
- (2) Let $A\in\mathcal E$,
Since $A\in\mathcal E\in\mathcal T_0$, and $T_0$ is a tower, we have $g(A)\in T_0$.
Denote $\{B\in\mathcal T_0|g(A)\subseteq B\lor B\subseteq A\}$ by $\mathcal F$,
then $\mathcal F$ is a tower in $S$:
- (1) Since $\emptyset\in\mathcal T_0$ and $\emptyset\subseteq A$, we know $\emptyset\in\mathcal F$.
- (2) Let $B\in\mathcal F$, then either $g(A)\subseteq B$ or $B\subseteq A$.
Since $B\in\mathcal F\in\mathcal T_0$, and $T_0$ is a tower, we have $g(B)\in T_0$.
Since $A\in\mathcal E$ and $g(B)\in T_0$, we have either $A\subseteq g(B)$ or $g(B)\subseteq A$.
- If $g(A)\subseteq B$, then $g(A)\subseteq g(B)$, so $g(B)\in\mathcal F$.
- If $B\subseteq A$:
- If $A\subseteq g(B)$, we have $B\subseteq A\subseteq g(B)$, so either $A=B$ or $A=g(B)$,
- if $A=B$, then $g(A)\subseteq g(B)$, so $g(B)\in\mathcal F$;
- if $A=g(B)$, then $g(B)\subseteq A$, so $g(B)\in\mathcal F$.
- If $g(B)\subseteq A$, we have $g(B)\in\mathcal F$.
In all cases, $g(B)\in\mathcal F$.
- (3) Suppose $\mathcal D\subseteq\mathcal F$ is a chain in $\mathcal C$,
then $\mathcal D\subseteq\mathcal F\subseteq\mathcal T_0$; since $\mathcal T_0$ is a tower, we have $\cup\mathcal D\in\mathcal T_0$.
For each $B\in\mathcal D$, since $B\in\mathcal F$, either $g(A)\subseteq B$ or $B\subseteq A$.
- If for all $B\in\mathcal D$, $B\subseteq A$, then for all $u\in\cup\mathcal D$, there exists $D\in\mathcal D$ such that $u\in D$,
then $D\subseteq A$, so $u\in A$; therefore, $\cup\mathcal D\subseteq A$.
- If there exists $B\in\mathcal D$ such that not $B\subseteq A$, then $g(A)\subseteq B\subseteq\cup\mathcal D$.
In both cases, either $\cup\mathcal D\subseteq A$ or $g(A)\subseteq\cup\mathcal D$, so $\cup\mathcal D\in\mathcal F$.
Clearly, we have both $\mathcal F\subseteq\mathcal T_0$ and $\mathcal T_0\subseteq\mathcal F$, so $\mathcal T_0=\mathcal F$.
So if $B\in\mathcal T_0$, we also have $B\in\mathcal F$, then we have either $g(A)\subseteq B$ or $B\subseteq A\subseteq g(A)$.
Therefore, $g(A)\in\mathcal E$.
- (3) Suppose $\mathcal D\subseteq\mathcal E$ is a chain in $\mathcal C$,
then $\mathcal D\subseteq\mathcal E\subseteq\mathcal T_0$; since $\mathcal T_0$ is a tower, we have $\cup\mathcal D\in\mathcal T_0$.
Now let $B\in\mathcal T_0$. For each $A\in\mathcal D$, since $A\in\mathcal E$,
either $A\subseteq B$ or $B\subseteq A$.
- If for all $A\in\mathcal D$, $A\subseteq B$, then for all $u\in\cup\mathcal D$, there exists $D\in\mathcal D$ such that $u\in D$,
then $D\subseteq B$, so $u\in B$; therefore, $\cup\mathcal D\subseteq B$.
- If there exists $A\in\mathcal D$ such that not $A\subseteq B$, then $B\subseteq A\subseteq\cup\mathcal D$.
In both cases, either $\cup\mathcal D\subseteq B$ or $B\subseteq\cup\mathcal D$, so $\cup\mathcal D\in\mathcal E$.
Clearly, we have both $\mathcal E\subseteq\mathcal T_0$ and $\mathcal T_0\subseteq\mathcal E$, so $\mathcal T_0=\mathcal E$.
Given $A,B\in\mathcal T_0$, we have $A\in\mathcal E$, so $A\subseteq B$ or $B\subseteq A$.
Therefore, we have shown that $\mathcal T_0$ is a chain in $\mathcal C$.
Let $C^*=\cup\mathcal T_0$. Since $\mathcal T_0$ is a chain in $\mathcal C$, by property (3) of towers, $C^*=\cup\mathcal T_0\in\mathcal T_0$.
Then by property (2) of towers, $g(C^*)\in\mathcal T_0$. Hence, $g(C^*)\subseteq\cup\mathcal T_0=C^*$.
Since $g(C^*)\subseteq C^*\subseteq g(C^*)$, we have $g(C^*)=C^*$, implying ${C^*}'=\emptyset$.
Let $s\in S$. If $C^*\cup\{s\}$ is a chain, then $s\in C^*$.
We have shown that $S$ has a maximal chain, which is $C^*$.
Since every chain in $S$ has an upper bound, $C^*$ has an upper bound $c^*$.
Let $s\in S$, if $c^*\preceq s$, then for all $c\in C^*$, $c\preceq c^*\preceq s$, so $c\preceq s$.
Since we also have $s\preceq s$, $C^*\cup\{s\}$ is a chain, then $s\in C^*$, hence $s\preceq c^*$, therefore $s=c^*$.
We have shown that $c^*$ is a maximal element in $S$.
$\blacksquare$
Well-ordering principle
Every set is well-orderable.
(show proof)
Proof.
Let $X$ be a set. Let $W$ be the collection of pairs $(S,\preceq)$ such that $S\subseteq X$ and $\preceq$ well-orders $S$.
Define a relation $\preceq_W$ on $W$ by $(S,\preceq)\preceq_W(S',\preceq')$ if and only if
- $S\subseteq S'$,
- $\preceq$ is the restriction of $\preceq'$ on $S$, and
- for all $s\in S$ and $s'\in S'\setminus\{S\}$, $s\preceq' s'$.
Then $\preceq_W$ is clearly a partial order on $W$.
Note that $(\emptyset,\emptyset)\in W$.
Now we will show that every chain in $W$ has an upper bound in $W$.
Let $C$ be a chain in $W$.
Define $\cup C$ by $\cup_{(S,\preceq)\in C} S$ and $\preceq_{\cup C}$ by $\cup_{(S,\preceq)\in C} \preceq$
We will first show that $(\cup C,\preceq_{\cup C})\in W$.
Clearly, we have $\cup C\subseteq X$.
Now we need to show that $\preceq_{\cup C}$ well-orders $\cup C$:
- $\preceq_{\cup C}$ is a relation on $\cup C$: if $p\in\preceq_{\cup C}$, then for some $(S,\preceq)\in C$, $p\in\preceq$, so $p\in S\times S$, thus $p\in\cup C\times \cup C$.
- $\preceq_{\cup C}$ is a partial order on $\cup C$:
- Let $x\in\cup C$, then for some $(S,\preceq)\in C$, $x\in S$, so $x\preceq x$, so $x\preceq_{\cup C}x$.
- Let $x,y\in\cup C$, if $x\preceq_{\cup C}y$ and $y\preceq_{\cup C}x$, then for some $(S,\preceq),(S',\preceq')\in C$,
$x\preceq y$ and $y\preceq' x$. Since $C$ is a chain, either $(S,\preceq)\preceq_W(S',\preceq')$ or $(S',\preceq')\preceq_W(S,\preceq)$.
So one of $\preceq$ and $\preceq'$ is a restriction of the other, so either $x\preceq y$ and $y\preceq x$, or $x\preceq' y$ and $y\preceq' x$.
We have $x=y$ in either case.
- Let $x,y,z\in\cup C$, if $x\preceq_{\cup C}y$ and $y\preceq_{\cup C}z$, by the same reasoning as above,
there exists $(S,\preceq)\in C$ such that $x\preceq y$ and $y\preceq z$, so we have $x\preceq z$, and hence $x\preceq_{\cup C}z$.
- $\preceq_{\cup C}$ is a total order on $\cup C$: let $x,y\in\cup C$, then for some $(S,\preceq),(S',\preceq')\in C$, $x\in S$ and $y\in S'$.
Since $C$ is a chain, either $(S,\preceq)\preceq_W(S',\preceq')$ or $(S',\preceq')\preceq_W(S,\preceq)$.
So one of $S$ and $S'$ is a subset of the other. So either $x,y\in S$ or $x,y\in S'$, we either have $x\preceq y$ or $y\preceq x$, or have $x\preceq' y$ and $y\preceq' x$.
In either case, either $x\preceq_{\cup C}y$ or $y\preceq_{\cup C}x$.
- $\preceq_{\cup C}$ is a well-order on $\cup C$: Let $T$ be a non-empty subset of $\cup C$.
Let $t\in T$, then $t\in\cup C$, so for some $(S,\preceq)\in C$, $t\in S$.
Let $s$ be a least element of $T\cap S$ given by $\preceq$.
Let $t'\in T$. If $t'\in S$, then $s\preceq t'$, so $s\preceq_{\cup C} t'$.
If $t'\notin S$, since for some $(S',\preceq')\in C$, $t'\in S'$,
and $C$ being a chain implies $(S,\preceq)\preceq_W(S',\preceq')$,
we have $s\preceq't'$, and hence $s\preceq_{\cup C}t'$.
So $s$ is a least element of $T$ given by $\preceq_{\cup C}$.
Therefore, $(\cup C,\preceq_{\cup C})\in W$.
The next goal is to show that $(\cup C,\preceq_{\cup C})$ is an upper bound of $C$.
For all $(S,\preceq)\in C$:
- $S\subseteq \cup C$.
- Clearly, $\preceq\subseteq\preceq_{\cup C}\cap (S\times S)$.
Suppose $p\in\preceq_{\cup C}\cap (S\times S)$, then for some $(S',\preceq')\in C$, $p\in\preceq'$.
Since $C$ is a chain, one of $\preceq$ and $\preceq'$ is a restriction of the other.
If $\preceq$ is the restriction of $\preceq'$ on $S$, since $p\in\preceq'\cap (S\times S)$, $p\in\preceq$.
If $\preceq'$ is a restriction of $\preceq$, then $p\in\preceq$.
So $p\in\preceq$ in either case. Hence $\preceq=\preceq_{\cup C}\cap (S\times S)$.
- Let $s\in S$ and $s'\in \cup C\setminus\{S\}$, then for some $(S',\preceq')\in C$, $s'\in S'$.
Since $C$ is a chain, we have $(S,\preceq)\preceq_W(S',\preceq')$.
Note that $s'\in S'\setminus\{S\}$, so $s\preceq's'$, and hence $s\preceq_{\cup C}s'$.
Therefore, $(S,\preceq)\preceq_W(\cup C,\preceq_{\cup C})$.
Since $(W,\preceq_W)$ is a non-empty partially ordered set such that every chain in $W$ has an upper bound in $W$,
by Zorn's lemma, $W$ has a maximal element $(S^*,\preceq)$.
Suppose for contradiction that $S^*\neq X$.
Let $x^*\in X\setminus\{S^*\}$, define a relation $\preceq'$ on $S^*\cup\{x^*\}$ such that $\preceq'$ contains exactly
- $(x^*,x^*)$,
- $(x,x^*)$, for all $x\in S^*$, and
- $p$, for all $p\in\preceq$.
Then $\preceq'$ clearly well-orders $S^*\cup\{x^*\}$.
And we have $(S^*,\preceq)\preceq_W(S^*\cup\{x^*\},\preceq')$ but $(S^*,\preceq)\neq(S^*\cup\{x^*\},\preceq')$,
a contradiction to $(S^*,\preceq)$ being a maximal element in $W$.
Therefore, $S^*=X$, which implies that $X$ is well-orderable by $\preceq$.
$\blacksquare$