In the previous chapters, we have repeatedly brought up a metamathematical context, such as the use of the Axiom of Choice, or Solovay’s model in which every set of reals is measurable. But we have not really distinguished between results in a formal theory and in the metatheory, mostly because we did not really establish a formal theory to begin with. We have treated descriptive set theory like most other mathematical theories in that we defined our basic objects (Polish spaces, Borel sets, etc.) and then started proving facts about them “the usual way”, as we would prove facts about commutative rings or locally compact topological spaces. But in order to make better sense of the metamathematical issues, we have to “pause” and talk a bit about the axioms of set theory.
Comprehension and Russell’s Antinomy¶
To develop set theory formally as a theory of first order logic, we first need to fix the language. We want to consider the notion of a set as foundational (with the intention to develop everything else from it), we provide only one binary relation symbol, . We will denote this as the language of set theory, .
How can we axiomatize the concept of set?
In his famous 1895 paper “Beiträge zu Begründung der transfiniten Mengenlehre” Cantor (1895), Georg Cantor writes
Unter einer “Menge” verstehen wir jede Zusammenfassung von bestimmten wohlunterschiedenen Objekten unserer Anschauung oder unseres Denkens (welche die “Elemente” von genannt werden) zu einem Ganzen.
This can be translated approximately as: A set is any collection of certain distinct objects of our intuition or our thought into a whole.
We can try to make this more precise as follows:
For every property exists a set of all objects having property : .
This can be formalized in the language of set theory as an axiom scheme: For every -formula ,
(Comprehension)
This axiom, however, is contradictory.
We obtain similar contradictions if we choose as the formula
Regarding the existence of sets, we have to distinguish between
- classes, which we will denote by capital letters (for some specific, important classes we will also use boldface) and
- sets, denoted in this context by lower case letters .
An arbitrary property will define a corresponding class
As we saw above, classes are not necessarily sets: some are “too large” to be a set, as for example the class of all sets,
Classes that are not sets are called proper classes.
You should keep in mind that, in the formal theory , we do not have variables for classes, so the definition above is informal. Any class variable, as well as expressions like , should be seen as abbreviations for a formal expression using the underlying formula. There are formal systems (such as Bernays-Gödel set theory) that use classes explicitly, but they are used less frequently.
The Axioms of ¶
We begin with the Axiom of Extensionality, which is essential for the equality relation between sets.
Consequently, two sets coincide if they have the same elements.
The basic idea of the Zermelo-Fraenkel axiom system is that we avoid introducing sets that are “too large” (and hence would lead to contradictions) by allowing new sets only if they can be “generated” from a given set by a number of fixed, well-behaved operations.
So let us postulate that at least one set exists:
This axiom is not strictly necessary, as the existence of a set also follows from other axioms in (or usually even from the underlying axioms of first-order logic). But it is good to have it as a starting point here for emphasis.
We have seen we cannot use full comprehension for sets. In its place we introduce the scheme of Separation. Let be a -formula in which does not occur as a free variable.
By Extensionality, the set is unique. Note that there is one axiom for every formula , so Separation is an axiom scheme.
Separation allows us to select from any class those elements that are in a given set and collect them in a set
Next, we have
This axioms allows to form pairs of sets, specifically
While for the pair set the order is not important, we have for the ordered pair
Hence, we can introduce binary relations as classes of ordered pairs
As usual, by identifying functions with their graphs, we can introduce functions as a special kind of relation:
We write to denote that fact that is a function.
Further elementary axioms:
In words, if defines a function, then the image of any set under that function is a set. Note that, as in the case of Separation, is allowed to have parameters, which we dropped here to improve readability.
It follows that, for a given set , the following classes are sets:
The axiom of Infinity is a “pure” set existence axiom, that is, it does not depend on another set already existing. It therefore renders the axiom of Set Existence above redundant. It also implies the existence of the set (the set theoretic version of the natural numbers), along with the operation .
Using , we can introduce the other basic number sets:
- , where . Multiplication on can be defined inductively (see below).
- , where .
- We can extend the linear order of to and then to in the usual way. Then we can introduce the real numbers as the set of Dedekind cuts:
We complete the list of axioms with the Axiom of Foundation:
As we discussed before, Foundation rules out, for example, that a set can be an element of itself. More precisely, the axiom states that -relation is well-founded on any set.
We can also formalize the Axiom of Choice in the language of set theory:
We denote the axiom system as , Zermelo-Fraenkel with Choice.
- Cantor, G. (1895). Beiträge zur Begründung der transfiniten Mengenlehre. Mathematische Annalen, 46(4), 481–512.