Modern Zermelo-Fraenkel set theory is currently the official rulebook for doing most mathematics. For this reason alone it is worth our attention, since our development of computability will be given in set theory. But it also formalizes the demonstration of existence claims in mathematics and illustrates the kind of free-wheeling assumptions that made constructivists nervous. Nobody knows if it is consistent. Gödel's theorem will tell us that if it is consistent, it can't tell us that it is. But even if it did tell us it was consistent we wouldn't care because it would have told us if it were inconsistent anyway.
The language L of set theory is a marvel to behold. It is just the logical language L with one binary relation added:
x in y.
All of the symbols in calculus are definable in set theory in terms of the relation x in y. For legibility, I will replace the
"official" form
- (x in y)
with
(x notin y).
Axioms are just statements that you can stick into a proof wherever you want without further justification. If you want, you can assume that the power set of a given set always exists. Or you can assume that pink elephants exist. Assumptions are as easy to make as they are to write down. These are the axioms of ZF set theory.
Some set exists. We don't assume anything else about it, and the E elimination rule of logic makes sure that we don't fool ourselves into thinking that we do!
(Set Existence) Ex x = x.
Actually, this axiom is redundant because it follows from our logic.
The axiom of extensionality says that sets with the same elements are identical.
Ay Az (Ax(x in y <---> x in z) ---> y = z).
There is no color , shape, or other characteristic about whatever it is that holds all the elements together. That lopsided circle with a ball and an a dog in it that they showed you in grade school therefore wasn't really a set, since two lopsided circles with different shapes would be distinct even though they have the same elements.
Extensionality doesn't have an existensial quantifier, so it isn't used to prove existence. It is used to prove uniqueness, which is essential for the introduction of function symbols into the language.
The original set theories of Gottlob Frege and Georg Cantor assumed the following, which we will most definitely not assume. Let P(x, z1, ..., zn) be a formula of L free in x, z1, ..., zn. Then the following is an axiom:
Az1, ..., Azn, Ey Ax (x in y <---> P(x, z1, ..., zn)) [comprehension].
Thus, comprehension is not a single axiom, but an axiom schema, each instance of which is an axiom. Nothing prevents a set of axioms from being infinite, so long as you say which sentences count as axioms. After all, the point is to know what you get to put in a proof without further justification.
The axiom says that for each z1, ..., zn, we are entitled to assume the existence of a set whose members are exactly the sets x satisfying P(x, z1, ..., zn). In other words, comprehension turns definable properties into things (sets). This is reminiscent to Plato's trick of turning the predicate "is even" into an object: the Form of Evenness.
Naive comprehension is the immediate source of Russell's paradox. Here is an official derivation. Note that squiggly braces have nothing to do with it. They are introduced by an explicit definition, and hence could not introduce an inconsistency unless it could be derived from the axioms without them. Choose P(x) = not (x in x). Then we have:
By the [ _|_ ] rule, every Q follows from naive comprehension. You may be wondering how we get _|_ from A <---> -A in step 4. Well, let's do it once.
Is this proof intuitionistically valid?
Zermelo's idea was to block this argument by means of a slight modification of the comprehension axiom, which is called separation. This one is official:
Az1, ..., Azn, Az, Ey, Ax (x in y <---> x in z & P(x, z1, ..., zn)) [separation].
The idea is that separation yields only a subset y of a set z that is already known to exist. Thus, P(x, z1, ..., zn) is a "plan" for "carving" y out of a block z of given material. The plan may be fine, but if there is no sufficiently big block of marble available, it can't be produced.
Watch what happens when we try to re-run Russell's paradox using this axiom:
It doesn't work. Suppose we give ourselves enough marble to work with. Since assuming is as easy as writing, let's overcome the restrictiveness of zermelo's comprehension axiom by means of the...
Mother of all axioms: Ey Ax (x in y).
This says that some set contains all sets. So it must contain itself as well. And the singleton containing itself, etc. Well, assumptions are easy to make, as I said. Now, together with comprehension, we have:
So Russell returns if we assume we have enough marble to carve the Russell set out of. But we don't assume [mother] and we hope we haven't assumed enough for the Russell set to come back, though we can't really be sure.
Note that if we put a subproof line next to the whole proof just given, it is actually an intuitionistically valid proof that
Theorem 1: ZF |- not Ew Ax (x in w).
So there you have it: the bigger they are, the harder they fall! Russell's paradox has been tamed to prove a theorem.
Keeping with the David and Goliath theme, the littlest thing does exist. We are going to introduce the empty set. I will call it "0", which will turn out to be entirely appropriate when we construct the natural numbers.
"0" is a constant symbol. But it is not a constant symbol in L. We have to introduce it . A constant symbol may be thought of as a 0-ary function symbol. In general, here is how to introduce a function symbol without getting into trouble.
Let P(x1, ..., xn, , y) be a formula of L free in x, y. Let T be a set of axioms. Suppose the axioms are such that
T |- Ax1 ... Axn Ey P(x1, ..., xn, y).
T |- Ax1 ... Axn Ay Az P(x1, ..., xn, y) & P(x1, ..., xn ,z) ---> y = z.
Then we may introduce a new symbol f into the language and use the symbol's definition:
Ax1 ... Axn Ay f(x1, ..., xn) = y <---> P(x1, ..., xn, y) [defn f]
as a new axiom. Existence and uniqueness come out of the quantifier rules automatically, once the definition is allowed into proofs. That's why you better make sure you can prove them before you add it! Just watch:
What justifies this procedure? Just that if we always follow it, we have the property that the theorems of T in L are exactly the theorems in L that are provable from T together with the definition of f. We say that the definition conservatively extends T. Thus, definitions may serve to shorten proofs, but they never allow us to prove things we couldn't have proved without them. IF, that is, we follow the rules just outlined.
Let's introduce the constant (0-ary function symbol) 0 according to the above rule. Choose
P(y) = Ax x notin y.
Now we must find derivations witnessing:
For existence, we have
For uniqueness, we have
Note that at this level, we shouldn't be getting too uptight about dinky propositional logic UNLESS we are particularly interested in intuitionistic as opposed to classical results. Eventually, you will be so used to the axioms that you can apply them without writing them down first, and similarly for definitions. But there must always be a reference tot he axiom or definition when you do so. Also, for now, quantifier rules should always be applied rigorously.
Now we are entitled to use the constant (0-ary function symbol) 0, together with the definition
Ay (0 = y <---> Ax x notin y) [defn 0].
This may look funny, but it is just a 0-ary instance of the familiar
Ax1 ... Axn Ay f(x1, ..., xn) = y <---> P(x1, ..., xn, y)
You are no doubt thinking that it would have been much easier to just say 0 = {x in z: not x = x}, where z is an arbitrary existing set. But where are those wonderful squiggly brackets {x in z: P(x)}? Not in L. So they must be introduced by a definition.
What the heck are those squiggly brackets anyway? They should denote a set y carved out of some given set z according to "plan" P(x). Hence, despite their strange appearance, they denote a distinct function symbol introduced into L for each choice of P(x). This becomes apparent if we write them more conventionally as
{x in z: P(x)} = fP(z).
Logic doesn't really care if you use funny symbols for function symbols, as long as you use the notation consistently. For f(x, y) you could write x___y, if you like. Don't get hung up staring at notation trying to guess what it might mean. Find the definition. That's all that matters.
So we must show existence and uniqueness in order to introduce this funny looking function symbol. It's easy! Let the set theoretic relation defining comprehension be
Q(z, y) = Ax x in y <---> x in z & P(x)
We need to show
Existence is a one liner. That's what comprehension is for.
Az Ey (Ax x in y <---> x in z & P(x)) [comprehension]
Uniqueness is also easy. That's what extensionality is for.
A proof like this can be streamlined.
Here is a streamlined version. You won't lose any points for a proof like this. You will earn the grader's undying gratitude.
Now we can introduce the squiggly brackets notation with a definition:
{x in z: P(x)} = y <----> Ax (x in y <---> x in z & P(x)).
Again, this looks more normal in usual function notation:
fP(z) = y <----> Ax (x in y <---> x in z & P(x)).
Exercise 1: Use the new notation to define the function intersect(c), which returns the intersection of all the sets in c.
Comprehension is a powerful tool for carving pretty sets out of big lumpy sets. But we don't have any big lumpy sets. We have only the empty set. That's not too exciting.
Maybe we can get more. How about {0, 0}? Nope. We don't get anything out of the air. We don't get anything unless we assume it into being or prove it to exist from other assumptions. Now we just plain assume that every two sets are elements of another set. Nothing subtle about that.
Ax Ay Ez (x in z & y in z) [pairing]
Now consider the definition
{x, y} = z <---> Aw w in z <---> w = x or w = y.
We have to justify it by showing the existence and uniqueness of z.
Uniqueness is easy.
Yippee. Now we have 0 and we can make pairs. We can also define without further ado:
{x} = {x, x}.
Existence and uniqueness come immediately from the fact that {x, x} is already a term in the extended language.
We can also define
<x, y> = {x, {x, y}}.
So we have infinitely many sets that look like binary trees:
0, {0}, {0, {0}}, {{0}, {0, {0}}, {{0}, {0, {0}}
And we have a clunky way to represent finite sequences.
<x, y, z> = <<x, y>, z>.
Later, we will represent finite sequences as functions on a finite initial segment of the natural numbers, but we don't have even finite functions and relations yet.
Still, not bad for such a dumpy axiom.
Now if we had the set of natural numbers and we could form unions and cross products and power sets, we'd be cooking. But we can't do any of that yet. We have to assume every bit of it, with a separate existence axiom for each. Do you understand now why some mathematicians might have felt queasy about this? Where is the certitude? Where is the intersubjecivity? Where is the guarantee of consistency? Assume, assume, assume.
We would like to let Uz be the union of all sets yin z. But we don't know that such a set exists. Intuitively it should, since it is no "bigger" than z. So since assumptions are free, let's assume it!
Az Ey Ax (x in y <---> Ew (w in z & x in w)) [union].
Now define
Uz = y <---> Ax (x in y <---> Ew (w in z & x in w)) [defn U].
As usual, we must establish existence and uniquenss before using this definition in a proof. Existence is immediate by the axiom. I leave uniqueness to you.
Exercise 2: prove the uniqueness claim for union.
Exercise 3: Suppose x, y exist. Do we now know that x U y exists? Prove it.
So we now have lots of sets. In fact, we have each of the natural numbers
Note: each natural number is the set of all its predecessors, starting with the empty set.
Indeed, we have the successor operation on the natural numbers:
s(x) = x U {x}
We also have ordered pairs of natural numbers. But we don't have the set of all natural numbers. That's another matter entirely. It is a "completed" rather than a "potential" infinity.
Function symbols are not the only extra notation we need. It is also convenient to add new relations. This is easier, because we don't have to establish uniqueness and existence. Every formula of set theory expresses a definable relation.
y subseteq z <---> (Ax x in y ---> x in z) [defn subseteq]
y subset z <---> y subseteq z & not y = z [defn subset].
Also, we can define the ordering relation for natural numbers
x lesseq y <---> x in y [defn lesseq].
x less y <---> x lesseq y & not x = y [defn less].
We can also define interesting properties. Each natural number set defind above has the following property
transitive(y) <---> Ax (x in y ---> x subseteq y)
Defined vocabulary can be used to state new axioms in a more succinct manner
This is one of the most useful axioms, since it yields the cartesian product function and hence relations and functions on a given domain. It falls short, however, of establishing the set of all functions on a given domain. That requires the power set axiom. Each time we get new objects, the set of all those objects becomes a new question requiring more assumptions.
The replacement schema says that if we can define a function symbol in set theory, then the image of any set under the function is also a set. The motivation is the same as in the union case: the image can't be any "bigger" than the original set (because of uniqueness), so such an axiom can't take us up to "scary", huge things like Russell's set.
Let f be an introduced function symbol. Then the following is an axiom:
Ay Ez Ax (Ew (w in y & f(w) = x) ---> x in z) [replacement].
We can use replacement to define a function taking each y to the image of y under defined function f:
Imagef(y) = z <---> Ax (x in z <---> Ew w in y & f(w) = x) [defn image].
Exercise 4: Prove existence and uniqueness to justify the definition.
Then we can introduce the following, more familiar notation
{f(x): x in y} = Imagef(y).
This isn't the notation justified by separation (why not?). Don't confuse the two.
We can use replacement twice and union to define the familiar cartesian product operation a X b.
{y} X z = {<y, w>: w in z}
w X z = U{{y} X z: y in w}
We have seen how to add new function symbols and predicates to L by way of definitions. But we can also view sets as relations and functions.
r is a relation <---> Ey Ez (r is a subset of (y X z)).
Then define the special conventional notation:
r(x, y) <---> <x, y> in r.
Now you can define reflexivity, symmetry, transitivity, partial order, simple order, and equivalence relations as it is usually done in modern math textbooks.
We can't define the domain of x using the separation schema as it is usually done in elementary textbooks:
dom(r) = {y: Ez <y, z> in r}. Why not?
The right way to do it is to define the projection functions for ordered pairs as follows, establishing existence and uniqueness, as always:
p1(<x, y>) = x
p2(<x, y>) = y
Then use the replacement schema to define domain and range
dom(r) = {p1(<x, y>): <x, y> in r}.
rng(r) = {p2(<x, y>): <x, y> in r}.
Functions are now single-valued relations
r is a function <---> Ax Ay Az (<x, z> in r & <x, y> in r ---> z = y).
r is injective <---> Ax Ay Az ((<x, z> in r & <y, z> in r) ---> x = y).
(r: x ---> y) <---> r is a function & dom(r) = x & rng(r) is a subset of y.
r is onto y <---> rng(r) = y.
r is a bijection from x to y <---> r is a function & r is injective & r is onto y.
Introduce the conventional notation:
if f is a function and x in dom(r), then f(x) denotes the unique y such that <x, y> in f.
To show that a function f exists as a set , follow this procedure:
An important word of caution: the operations corresponding to introduced function symbols do not exist as sets.
Exercise 5: Show that the successor operation s does not exist as a set theoretic function. More precisely,
-Es s is a function & Ax, y, (<x, y> in s <---> y = x U {x}).
Why does it matter? I'll tell you...
We compare sizes of sets by associating each element of one set with a unique element of the other. Such an association is an injective function. If the function is also onto, then the sets have the same size or cardinality.
x = y <---> Ef (f is a bijection from x to y).
x < y <---> Ef (f: x ---> y is injective).
Notice that cardinality is defined with an existential quantifier. One must show the existence of f. Since quantifiers range over sets, that means that you must go through the above procedure to show that f exists as a function.
The power set axiom is as follows:
Ay Ez Ax (x subseteq y, y in z) [power set].
This axiom allows us to introduce a new squiggly bracket notation:
{y: y is a subset of x} = z <---> Ay (y subset x ---> y in z).
Notice that this is neither the replacement operation nor the separation operation. It requires the power set axiom to introduce. An alternate notation is:
P(x) = {y: y is a subset of x}.
The most basic result of set theory is that no set is the same size as its power set.
Ax (x < P(x)).
How do we prove this? It requires us to show that a function does not exist:
Make sure you can fill in the missing steps rigorously.
Some definitions:
x is linearly ordered by "in" <---> Ay, z (y in x & z in x ---> y in z or z in y).
x is least in y <---> x in y & Az (z in y & not z = x ---> x notin y).
x is well-ordered by "in" <---> Ay (not y = 0 ---> Ez (z is least in y)).
x is transitive <---> Ay (y in x ---> y subset x).
x is an ordinal number <---> x is linearly ordered & x is transitive & x is well-ordered.
x is a successor ordinal <---> Ey (y is an ordinal & x = s(y)).
x is a natural number <---> x is an ordinal number & Ay (y in x ---> y = 0 v y is a successor ordinal).
Thus
0, {0}, {0, {0}}, {0, {0}, {0, {0}}}, ...
are natural numbers.
{{0}, {0}}
is not a natural number.
We don't know that the set of all natural numbers exists yet. That is the job of the infinity axiom.
Recall that we don't yet have the set of all natural numbers, so we don't have relations or functions on the natural numbers either (although we do have finite functions defined on finite sets of natural numbers). How do we get the set of all natural numbers? Well, we assume that it exists.
En (0 in n & Ax x in n ---> s(x) in n) [infinity].
To get the natural numbers themselves, define
N = y <---> Ay (y in N <---> y is a natural number).
If you like, show existence and uniqueness using the infinity axiom and extensionality.
We can define addition and multiplication on the natural numbers recursively, using successor.
x + 0 = x.
x + n+1 = s(x + n).
[It must be shown in set theory that such recurrence equations define a unique operation on N. That is the first lapse of rigor in these notes.]
Then we can define the integers Z as follows:
(x, y) is integer-equivalent to (z, w) <---> x+w = y +z.
[(x, y)]Z = {(z, w) in N X N: (x, y) is integer-equivalent to (z, w)}.
Z = {[(x, y)]Z: (x, y) in N X N}. (is this separation or replacement?)
The rationals are obtained similarly. Define multiplication on the natural numbers as follows:
x0 = 0
x(n+1) = (xn) + n.
Then define the rationals Q as follows.
(x, y) is rational-equivalent to (z, w) <---> xw = yz.
[(x, y)]Q = {(z, w) in N X N: (x, y) is rational-equivalent to (z, w)}.
Q = {[(x, y)]Q: (z, w) in N X N}.
So far, we haven't had to use the power set axiom. We need it to get from the rationals to the reals because the set R of all real numbers will be represented as a set of infinite sequences of rationals.
A Dedekind cut is a set of rationals (an element of P(Q)) that is
R = {c in P(Q): c is a Dedekind cut}.