\chapter{Zermelo-Fraenkel set theory with the axiom of choice (ZFC)}

Mathematics tries to consider a range of different mathematical objects; however logic is limited in that it only evaluates the truth of WFFs.
A set theory gives us a way of constructing the mathematical objects that we run into in the many fields of mathematics. It extends upon mathematical logic to study all the rest of mathematics.

Essentially, establishing a set theory provides a ground to axiomatize the rest of mathematics.





When we introduced set-builder notation, we made a point of ensuring that it is only allowed to form a set by 'filtering through' an already existing set for all elements satisfying a property; we specifically disallow it from representing all possible objects that satisfy a property.

Why did I place this restriction? If I lifted this restriction we would have \emph{Russel's paradox} and mathematics would be an inconsistent system, which we don't want.

ZFC is the standard set theory in use by mathematicians, and all the concepts we have developed thus far are valid in ZFC.

There exist other set theories one may employ as a basis for mathematics, some mathematicians even use systems called type theories instead of set theories, though the bulk of mathematics (save further set theory, type theory, and category theory) can be done formally in ZFC.

We will discuss these paradoxes in more detail to understand the dangers of allowing certain objects to be called sets. This will be motivation to formally define ZFC by its primitive notions and axioms.



\section{Formalized set theories}

\subsection{Logic}

We use a formal system such as a logic as a foundation to define a formalized set theory due to its precision.

ZFC is traditionally expressed using classical first-order logic, indeed this is the most common logic taught in undergraduate discrete mathematics courses.

Other set theories such as NBG are defined by means of different logics such as second-order logics, intuitionistic logics, and so forth.

\subsection{Von Neumann ordinals}
Technically no objects exist in set theory other than sets.
In practice, we can use sets to construct any of the objects that we wish to use in mathematics (so long as they aren't paradoxical).

As a matter of notation, we will denote a set with a lowercase letter if nowhere in the statement is the set's symbol printed directly on the right hand side of the $\in$ symbol. Otherwise we remain with the standard notation of representing sets with capital letters.




\section{Primitive notions}

The standard formal set theory construction used by mathematicians is ZFC. Due to its popularity, this will be the first formalized set theory that we will develop, showing how they relate to notions of naive set theory and the reasons the axioms are posed the way that they are.

We start with nothing except for classical first order logic, meaning we have the primitive objects, logical connectives, equality relation, and universal quantifiers.

The primitive objects of our theory will be sets; it is called set theory afterall!

\begin{definition}[Set (ZFC)]
A \emph{set} is the primitive object in ZFC.
\end{definition}

We also allow sets to 'contain' other sets by means of the membership relation.

\begin{definition}[Membership relation (ZFC)]
The \emph{membership relation} is a primitive relation in ZFC, meaning that the set on the left is contained by (is an element of) the set on the right.
\[x \in X\]
\end{definition}


\subsection{Notational shortcuts}
Using first-order logic with the membership relation, we can introduce a variety of notational shortcuts to translate notions of naive set theory into ZF.
The membership relation can be used to define the subset relation.
The subset relation acts as a shorthand for the following.

\begin{definition}[Subset relation]
In ZF, the \emph{subset relation} is the following shorthand.
\[Y \subseteq X \iff \forall y  [y \in Y \implies y \in X ]\]
\end{definition}


\[ \forall x \in X [ \varphi (x) ] \iff \forall x [x\in X \implies \varphi(x) ] \]
\[ \exists x \in X [ \varphi (x) ] \iff \exists x [x\in X \land \varphi(x) ] \]


\section{Axioms of ZFC}


Behold, the 9 axioms of ZFC.

\begin{itemize}
\item Axiom of Extensionality
\item Axiom of Regularity
\item Axiom Schema of Specification
\item Axiom of Pairing
\item Axiom of Union
\item Axiom Schema of Replacement
\item Axiom of Infinity
\item Axiom of Powerset
\item Axiom of Choice
\end{itemize}


Extensionality is a way of defining equality for sets.
Regularity disallows certain objects from being sets (i.e objects that would prove paradoxes if allowed to be sets).
Infinity allows sets of infinite cardinality to exist.
The rest of the axioms denote legal ways to construct sets from existing ones.

Note that axiom schema is just an infinite amount of axioms of a similar form. One could use second-order logic to compress an axiom schema into a single axiom, but for the sake of simplicity we won't.

\section{Axiom of extensionality}
Defines what it means for sets to be equal. $=$ is a symbol within first-order logic that has axioms within the logic itself, however a set theory needs to specify further axioms relating to the properties of $=$ on sets.
\begin{axiom}[Axiom of extensionality]
If 2 sets have the the same elements then they are equal.
\[\forall X \forall Y [ \forall z (z \in X \iff z \in Y) \implies X=Y ] \]
\end{axiom}

The other direction is an axiom of first-order logic.

\subsection{Axiom of regularity}

\begin{axiom}[Axiom of regularity]
Every nonempty set $X$ contains an element that is disjoint to $X$
\[ \forall X(\exists x [x \in X] \implies \exists Y[ Y \in X \land \nexists z (z \in X \land z \in Y)])\]
\end{axiom}

This axiom is required to prove that sets cannot have themselves as members

\subsection{Axiom schema of specification}


We will now turn towards axioms that relate to the ways in which we can construct new sets.

In naive set theory, we used set operations to construct new sets; we will see axioms that permit these operations later.
However set builder notation is perhaps the most powerful notion to specify the nature of sets (and will be required in the process of defining the set operations!); we require an axiom that states precisely how set builder notation may be applied to avoid paradoxes.

\begin{axiom}[Axiom schema of specification]
One can use set builder notation only to create subsets.
Specifically, one can construct a subset of $y$ by use of a predicate $\varphi$
\[\forall z\forall w_1 \hdots \forall w_n \exists y \forall x (x \in y \iff [(x \in z) \land \varphi(x, w_1, \hdots, w_n, z)])\]
\end{axiom}

This axiom allows any set of the following form.
\[X = \{x \in Y : \varphi(x) \}\]

The axiom schema of specification restricts set builder notation to consider the predicate on an already existing set, hence set builder notation in ZFC can only create subsets; it cannot create set that is a subset of the 'set of all sets' because this is not actually a set in ZFC (as we will see later).

With this limitation in place,we avoid Russel's paradox because the 'set of all sets' is not actually a set in ZF as we will see.




\subsection{Axiom of pairing}

The axiom schema of specification can make subsets, but we don't have an axiom that allows us to constrcut sets in. That is, rather than creating a set by internally minimizing an existing set, how can we make a new set by combining multiple existing sets?

This axiom starts by allowing (with the help of the axiom schema of specification) the creation of very basic sets; singletons and unordered pairs.

\begin{axiom}[Axiom of pairing]
\[\forall x \forall y [ \exists Z ([x \in Z] \land [y \in Z]) ] \]
\end{axiom}



\subsection{Axiom of union}

We are familar with the set operations of naive set theory, we would like an axiom that allows unions of sets to be sets themselves. Furthermore, we would like to make this axiom to be powerful but also consistent.

\begin{axiom}[Axiom of union]
T
\[\forall \mathcal{F} \exists X \forall E \forall x [x \in E \land Y \in \mathcal{F} \implies x \in X ] \]
\end{axiom}

Looking closely, one sees that this axiom allows the existence of a set that contains all elements of each set in $\mathcal{F}$, but it doesn't necessarily allow the existence of a set that ONLY contains all elements of each set in $\mathcal{F}$; one must pair this with the axiom schema of specification to allow the set union operation to be well defined.



\subsection{Axiom schema of replacement}


\begin{axiom}[Axiom schema of replacement]
The image of a set under any function is a set.
	\[\forall A \forall w_1 \hdots \forall w_n [ \forall x( x \in A \exists! y [\varphi] ) \implies \exists B \forall x (x \in A \implies \exists y ([y \in B] \land \varphi))] \]
\end{axiom}

\subsection{Axiom of infinity}

This axiom requires the notion of a set union and emptyset to be well defined within ZF, indeed the previous axioms ensure these are well defined (we will prove this in a later section).

Taking this for granted and interpeting the von Neumann ordinals as numbers, we can introduce the following axiom which states the existence of a set containing $\mathbb{N}$ (but not necessarily equalling $\mathbb{N}$, we require the axiom schema of specification once again to prove this).

\begin{axiom}[Axiom of infinity]
	\[\exists X [\emptyset \in X  \land \forall y ( y \in X \implies  S(y) \in X ) ]\]
	\[\exists X [\emptyset \in X  \land \forall y ( y \in X \implies  S(y) \in X ) ]\]
\end{axiom}

\subsection{Axiom of power set}

We introduce a necessary axiom for defining the powerset operation.
\begin{axiom}[Axiom of power set]
\[ \forall x \exists y \forall z [(z \subseteq y) \implies (z \subseteq x)] \]
\end{axiom}

Similar to the axiom of unions, one sees that this axiom allows the existence of a set that contains all subsets of $X$, but it doesn't necessarily allow the existence of a set that ONLY contains all subsets of $X$; one must pair this with the axiom schema of specification to allow the powerset operation to be well defined.


\subsection{Axiom of choice}


This axiom was once controversial, though since much of modern mathematics depends on it, it has become a conventional axiom to include in one's set theory. Indeed, one can study how ZFC behaves without the axiom of choice; ZFC without the axiom of choice is called ZF.
We will have much to say about this axiom later on.




\section{Basic results in ZFC}


Now that the axioms of ZF are stated, we use them to obtain the basic notions we had available to us in naive set theory.

\subsection{Existence of the empty set}


Given that at least 1 set exists, one can use the axiom schema of specification to assert the existence of the empty set. It is constructed by using the axiom schema of specification on this (or any other existing) set with a contradiction as its predicate.

\begin{proposition}
Let $w$ be a set, then the empty set exists.
\[\exists \emptyset (\forall X[X \notin \emptyset])\]
\[\emptyset = \{u \in w : (u \in u) \land \not(u \in u)\}\]
\end{proposition}

\subsection{Existence of set unions}

\[\bigcup_{Y \in \mathcal{F}} Y = X\]


If one looks closely, this axiom doesn't actually allow the union of arbitrary sets, but the \emph{union of sets contained within some set}. If it allowed the union of arbitrary sets, we count construct the 'set of all sets', which as I have alluded to before, is not actually a set.


Axiom schema of replacement + axiom of empty set = Axiom schema of specification

\subsection{Existence of power sets}

\[ \mathal{P}(X) = \{ Z \in Y : Z \subseteq X \}\]


If one looks closely, this axiom doesn't actually allow the union of arbitrary sets, but the \emph{union of sets contained within some set}. If it allowed the union of arbitrary sets, we count construct the 'set of all sets', which as I have alluded to before, is not actually a set.


Axiom schema of replacement + axiom of empty set = Axiom schema of specification

\subsection{Sets never contain themselves}

\[\nexists X [ X \in X ] \]








ZF is adequate to define a large portion of mathematics, indeed all the naive set theory in the previous part of this book can be constructed in ZF. however mathematicians today often use ZF along with an additional axiom that proves necessary for certain results spanning various fields of mathematics.

This axiom is the \emph{axiom of choice}.




\section{Axiom of choice}
Historically the most contoversial axiom in mathematics has been the axiom of choice and its equivalent forms (which we will discuss later). Even today, some mathematicians are hesitant to accept the axiom of choice in thei set theories.


\begin{axiom}[Axiom of choice]

\end{axiom}



\subsection{Zermelo's theorem (Well ordeing theorem)}

\begin{theorem}[Zermelo's theorem]
\[ X \]
\[ \exists \leq [ (X,\leq) \text{ is a woset} ] \]
\end{theorem}
That is, with first order logic, ZF with Zermelo's theorem taken axiomatically is equivalent to ZFC

\subsection{Zorn's lemma}


\begin{lemma}[Zorn's lemma]
\[(X,<)\]
\[\forall Y \subseteq X [ (Y,<) \text{ is a toset} Y \implies \text{ has an upper bound}] \implies $Y$ \text{ has a maximal element} \]
\end{lemma}

with first order logic,  ZF with Zorn's lemma taken axiomatically is equivalent to ZFC




















































\chapter{Von Neumann-Bernays-Gödel set theory (NBG)}



Now, ZFC is adequate for most of mathematics, however if we want to (carefully) study such things like universes, we require a more technical set theory. Category theory also requires this; the $\mathbf{Grp}$ 'set' in category theory is some idealized 'set' containing all groups, however in ZFC such a construction is forbidden and it would indeed be paradoxical. THe work around is acknowledging the existence of such a thing as a \emph{class}. A class is a generalization of a set that allows pathological containers like $\mathbf{Grp}$ and $V$, but also any normal set. The 'crazy classes' that can't boil down to a set without becoming paradoxical will be called a proper class; this is the intuition behind NBG.


\section{Classes}


NBG is an extension of ZFC that acknowledges the existence of classes that aren't sets.

\begin{definition}[Class (NBG)]
A \emph{class} is a primitive object in NBG.
A \emph{proper class} is a class that is not a set (we will define sets in NBG soon).
\end{definition}

\begin{definition}[Set (NBG)]
A \emph{set} is a class that is an element of some class.
\end{definition}

\subsection{Proper class}

Though a 'Russel set' is not a set in ZFC, a Russel class does indeed exist in NBG!
A universal class (class containing all sets) exists in NGB!











\part{Advanced}


Von Neumann ordinals
large cardinal numbers

\chapter{Alternativeformalized set theories}
\section{Morse-Kelley set theory (MK)}
\section{Kripke-Platek set theory (KP)}
\section{Tarski-Grothendieck set theory (TG)}