Kampf den Hopfenspikes!

This is part 2 of my series about the irrefutability of the axiom of choice from ZF. It will mainly introduce concepts about set theory.

Set theory is all about collections. While some set theories use elementary objects, ZF only knows sets. It needs no function symbol, but one binary relation symbol \in. Firstly of course, we notice that collections can usually be denoted by propositions with a free variable. Such collections are called classes. The intuition is that a class A associated with a formula B(x) is the collection \{x|B(x)\} (which is of course not possible for all B). We write x\in A for B(x), and sometimes we associate B itself with the class. We write A\not\in B for \lnot A\in B.

Most important, classes are only syntactical objects. We cannot quantify over them. They are only a convenient form of talking about collections, but everything we do with classes could be done logically directly. For example, if we write A\cup B, we could as well talk about the formula A(x)\vee B(x). Especially, we say that two classes are equal when they contain the same elements.

A first important class is the class \emptyset := \{x|\bot\}. It obviously contains no element. It is the empty class, we will axiomatically postulate that it is a set, the empty set.

Furthermore, there is the class V:=\{x|\bot\rightarrow\bot\}, the universe, which contains all sets. It is not a set, it is a proper class.

Another interesting class, which resembles Russel's paradoxon, is the class R:=\{x|x\not\in x\}. It is not a set: Assume it was a set and R\in R. Then R\not\in R. Contradiction, so R\not\in R, but then R\in R. Contradiction. R cannot be a set. R is a proper class.

The duty of ZF is it now to provide a class of sets, by postulating the existence of sets that can be created from other sets. However, the first axiom we deal with does not give us extra powers of creating sets, but limits the existing sets. It is the axiom of extensionality.

Since we did not want to add axioms for equality, we define equality of sets as it is done in Wikipedia:

 x=y :\Leftrightarrow \forall_z (z\in x\leftrightarrow z\in y) \wedge \forall_z(x\in z\leftrightarrow y\in z)

Then the extensionality axiom sais that two sets containing the same elements are equal, which can be expressed by

(EXT)  \forall_x\forall_y( \forall_z (z\in x \leftrightarrow z\in y) \rightarrow \forall_z(x\in z\leftrightarrow y\in z))

The first axiom giving us a set is the axiom of the empty set. Formally, it can be expressed by \exists_x \forall_y y\not\in x. However, we choose an equivalent, but more convenient notation, using the class V we defined above:

(NUL) \emptyset\in V

Having two sets, we axiomatically postulate the existence of a set containing these two sets, \forall_x\forall_y\exists_z (x\in z\wedge y\in z). Again, we use a more convenient notation

(PAR)
\forall_x\forall_y \{x,y\}\in V

As the high-level-notations should be well-known and as it should be clear how they can be rewritten into what we defined in Part 1, we will continue using high-level-notations.

For every set, there is the union of its elements:

(UNI) \forall_x \bigcup_{y\in x}\{y\} \in V

Then there is the axiom of infinity, which gives us the existence of an infinite set, which will turn out to guarantee the existence of the set of finite (ordinal) numbers. If one has never worked with ordinals before, it is rather counter-intuitive, but as soon as ordinals are definet, it should become clear. Essentially, it sais that there is a set containing \emptyset, and for all elements x it contains, it also contains x\cup\{x\}. Therefore, it contains \emptyset,\{\emptyset\},\{\{\emptyset\},\emptyset\},\ldots.

(INF) \exists_u (\emptyset\in u\wedge\forall_x (x\in u\rightarrow x\cup\{x\}\in u))

Then, for every set b we want a powerset \mathbb{P}(b), containing all subsets of b:

(POW) \forall_b \mathbb{P}(b)\in V

A further boundary for sets is the axiom of foundation, which sais that every nonempty set contains an element which is disjoint to itself. From this axiom follows that there are no infinite \ni-chains.

(FUN) \forall_z (z\neq\emptyset\rightarrow\exists_x(x\in z\wedge x\cap z=\emptyset))

For the final axiom, we need an additional concept. Usually, a binary relation can be considered a set of pairs, and a function can be considered a special type of relation. That is, a function is a relation which is left-unique, that is, if it contains (a,b_1) and (a,b_2), then b_1=b_2. We can extend this notion to classes: A class B is called functor, if it contains only pairs of sets, and if (a,b_1)\in B and (a, b_2)\in B implies b_1=b_2 for all a,b_1,b_2.

As functors are classes, there is no way of quantifying over all of them. The final axiom is therefore not really an axiom (even though it is often considered so), but an axiom scheme, describing infinitely many axioms. It sais that if we have a functor and a set, then the image of that set under the functor is also a set. It is called replacement scheme.

(RPL) For every functor F we have \forall_x \{F(y)|y\in x\}\in V

From the replacement scheme follows the comprehension scheme:

Lemma: For every class B and every set x\in V we have B\cap x\in V.
Proof: We can easily define a functor sending every element a onto \{a\} if a\in B, and onto \emptyset otherwise. Applying (RPL) and (UNI) we then get what we want.

Lemma: There is no infinite \ni-chain
Proof: Assume we had an infinitely long decreasing chain x_1\ni x_2\ni x_3\ni\ldots. Consider x=\bigcup_i \{x_i\}. For an arbitrary y\in x we can find an i such that y=x_i. Therefore, x_{i+1}\in y\cap x, and so, x violates (FUN). Contradiction.


Now we have all axioms of ZF. The critical part, which is the center of our further attention, is the axiom of choice:

(AC) \forall_x \exists_f ((f\mbox{ function on domain }x)\wedge\forall_y((y\in x\wedge y\neq\emptyset)\rightarrow f(y)\in y))

The relevance of this axiom is not immediately clear. It becomes clearer when dealing with well-orderings and ordinals:

Definition: A strict total ordering on a set s is a binary relation R satisfying
  • Transitivity: xRy and yRz imply xRz
  • Trichotomy: xRy or yRx or y=x
  • Irreflexivity: \lnot xRx
for all x,y,z\in s.

Definition: A well-ordering on a set s is a strict total ordering W on s, such that every x\subseteq s has a minimum.

Well-orderings are interesting since their existence for every set is equivalent to the axiom of choice:

Theorem: If every set A has a well-ordering w_A, then the axiom of choice holds.
Proof: Let an arbitrary set A be given. By (UNI), B=\bigcup\limits_{x\in A}x exists, and by assumption, there is a well-ordering w_B. Define f(\emptyset)=\emptyset and let f(x) for x\in A, x\neq\emptyset be the minimum of x regarding w_B. Then this f satisfies the axiom of choice.


Theorem: From the axiom of choice follows that every set has a well-ordering

We will not prove this here. A German version of this proof can be found on Wikipedia.

Well-orderings turn out to be extremely useful, therefore, we are interested in classifying them in a simple way. In the usual way we can define order-isomorphisms as structure-preserving bijective functions, and as usual, isomorphism becomes an equivalence relation, and therefore, we want to find representatives for every equivalence class.

Lemma: Let (x,<) be a well-ordering and y\in x. Then (\{z\in x|z<y\},<) is also a well-ordering, and is not isomorphic to (x,<).
Proof: Trivially (\{z\in x|z<y\},<) is also a well-ordering. Assuming there was an isomorphism f:\{z\in x|z<y\}\rightarrow x, then \{z\in x|f(z)\neq z\} is non-empty and contains a smallest element m such that f(m)\neq m. Then there must be some n\in x such that f(n)=m, but as m was minimal and n\neq m, we know that n>m, therefore f(n)>f(m), so m>f(m), which means that f(f(m))=f(m) since m was minimal, and therefore f(m)>f(f(m))=f(m). Contradiction.

Definition: A set x is called an ordinal if for all y\in x we have y\subseteq x and x is well-ordered by \in. The class of all ordinals is called \operatorname{On}, we will later prove that it is a proper class.

The following definition of natural numbers are examples for finite ordinals:
  • 0:=\emptyset
  • n+1 := n\cup\{n\}
We call the set of these numbers \omega, it is the smallest infinite ordinal.

Lemma: \emptyset\in x for x\in \operatorname{On}
Proof: x contains an \in-minimum y. Assume there was some z\in y, then also z\in x, and y would not be minimal anymore. Contradiction. Thus, y=\emptyset.

Lemma: If y\in x and x\in \operatorname{On}, then y\in \operatorname{On}.
Proof: As y\in x, y\subseteq x, so trivially, y is also well-ordered by \in. Assuming z\in y and t\in z, by transitivity we have t\in y, so every element of y is a subset. y\in \operatorname{On}.

Theorem: If x and y are ordinals whose well-orderings regarding \in are isomorphic, then x=y
Proof: Call the isomorphism f. Assuming f\neq id, there must be a minimal z\in x such that f(z)\neq z. Trivially, f(\emptyset)=\emptyset, so z\neq\emptyset. Therefore, there is some t\in z. Trivially, we have f(z) = \{f(t)|t\in z\}=\{t|t\in z\}=z. Contradiction.□

Theorem: Any two ordinals are comparable.

We will not prove this here.

Definition: For a class A we define A^{<\omega} as the collection of finite sequences of sets inside A.

Theorem: There is a bijective functor G:\operatorname{\operatorname{On}}\rightarrow\omega\times \operatorname{\operatorname{On}}^{<\omega}.
Proof: We show that there exists a well-ordering on \omega\times \operatorname{\operatorname{On}}^{<\omega} such that the class of predecessors of every element is a set. From this, the theorem follows directly. Firstly, on \operatorname{\operatorname{On}}^{<\omega}, define an ordering

pRq :\Leftrightarrow (\max(p) < \max(q)) \vee (\max(p) = \max(q) \wedge \operatorname{dom}(p) < \operatorname{dom}(q)) \vee (\max(p) = \max(q) \wedge \operatorname{dom}(p) = \operatorname{dom}(q) \wedge \exists_i\forall_{j<i} (p_i=q_j\wedge p_i<q_j))

, where max(\emptyset)=0. This is a well-ordering: Firstly, it sorts according to the maximum of the sequence, then according to the length, if both are equivalent, then it uses lexicographical ordering. Form \omega\times \operatorname{\operatorname{On}}^{<\omega} now, define \left<n,p\right><\left<m,q\right> :\Leftrightarrow pRq \vee (p=q \wedge n<m).