And now onto the last serious topic, one even more basic than Peano arithmetic. The axiom system we'll be using for set theory is ZFC (ZermeloFraenkel set theory with the axiom of choice).
1Set Theory¶
1.1Notation¶
The $\sum$ signature for this system is $\{ \in \}$ which is a binary relation symbol and that's it.
We often will write $x \not \in X$ instead of $\lnot(x \in X)$
$x \subseteq y$ abbreviates $\forall z (z \in x \to z \in y)$. $\subseteq$ is read as "is a subset of". $\subset$, on the other hand, means "is a proper subset of" and does not include the possibility that $x$ and $y$ are the same set. We won't be using
1.2Russell's paradox¶
Consider the set $R = \{x: x \notin X \}$ is $R \in R$? This is called Russell's paradox.
If yes then $R \notin R$ but then... contradiction.
The usual way out of this paradox: $R$ is not a set.
1.3Axioms of Set Theory¶
Most axioms of set theory are constructive principles, for making sets.
1.3.1Extensionality¶
$\forall x \forall y (\forall z (z \in x \iff z \in y) \to x = y)$ (a set is completely defined by what things it has as elements)
We can also write extensionality as $\forall x \forall y (x = y \leftrightarrow (x \subset y \wedge y \subset x))$.
Note that extensionality tells us something about the nature of sets, but doesn't actually give us any. The next axiom does, however.
1.3.2Empty set axiom¶
$\exists x \forall y (y \notin x)$ (there is a set that has no elements)
This is called the empty set, which can be defined as follows: $\varnothing = \{y : y \neq y) = \{\}$. By extensionality, there is only one such set.
1.3.3Comprehension (separation) scheme¶
The sweeping construction principle.
Let $\Phi(x, \bar{y})$ be the $\Sigma$formula $\forall y (y \notin x)$. We then have the following axiom:
$$\forall \bar{y} [ \forall z (\exists w \forall x (x \in w \iff (x \in z \land \Phi(x, \bar{y})))]$$
In other words, there must be a set $z$ that is "bigger" than $w$^{1}. But we need $z$ first^{what?}.
N.B. for all $x, y, z$:
 $x \subseteq x$
 $x \subseteq y \land y \subseteq z \to x = y$
 $x \subseteq y \land y \subseteq z \to x \subseteq z$
 $\varnothing \subseteq x$
 $x \subseteq \varnothing \iff x = \varnothing$
1.3.4Pairing¶
$\forall x \forall y \exists z (x \in z \land y \in z)$ (note: $x$ and $y$ can be equal)
Accepting this, we can now show the existence of a set $Z$ such that $\varnothing \in Z$.
In fact, an instance of comprehension now gives us $\{ \varnothing \}$  the set composed of only the empty set  which we can think of as the number "1" (with the empty set being the number "0"). $\Phi(x)$ in this case is $\forall u (u \in x)$.^{what does this mean?}
Now that we have two things to play with, let's make more! But first, let's look at singletons:
1.3.5Singletons¶
A singleton x ($\{ x \}$) is the set with only x as an element.
A "doubleton $x, y$" is $\{x,y\}$ where $x \neq y$.
We can now form some more sets: $\{\{ \varnothing \}\}$ from before, and $\{\varnothing, \{\varnothing\}\}$ ("2", as it has two elements). Or, $\{ 1 \}$ and $\{0, 1\}$.
Now, we would like to get $\{0, 1, 2\} = 3$ but we can't yet make a set with three elements, as pairing doesn't guarantee us anything beyond "2". We can form $\{0, 1\}$ and $\{2\}$, but because we don't have any sort of "union" axiom yet, we can't really do anything with that.
1.3.6Intersections¶
We can, however, form an axiom for intersections. We define $z \cap y$ as the set $w = \{ x \in z: x \in y\}$, where $\Phi(x, y)$ is $x \in y$.
We can also form $z \backslash y$: $\{x \in z : x \notin y$.
1.3.7Unions¶
(Not the kind that likes to go on strike, the other kind)
$\forall x \exists y (\forall z \forall w (z \in w \land w \in x \to z \in y))$ (so $y$ is the union of all the $x$'s  $\bigcup x$
We can now form finite and infinite sets. If the sets in $x$ are $z_1, z_2, z_3, \ldots$ then $\bigcup x = z_1 \cup z_2 \cup \ldots$. $A \cup B = \bigcup \{A, B \}$; $3 = \cup \{ \{0,1\}, \{2\}\}$. We can also form 4, 5, 6 etc.

As Russell's paradox demonstrates, some care needs to be taken about accepting the "set" $\{, x \Phi (x)\}$. This isn't really relevant though. ↩