# Mathematical Proof and the Principles of Mathematics/Sets/Classes

So far, the only set we've actually proved to exist is ∅. We'd like to continue on to build up more sets such as , etc., and define important set operations such as union and intersection. Informally, the way to do this is using formulas such as:
    $\{a\}=\{x:x=a\}$
    $\{a,b\}=\{x:x=a\operatorname {or} x=b\}$
    $a\cup b=\{x:x\in a\operatorname {or} x\in b\}$
The empty set can be made to fit this pattern using
    $\varnothing =\{x:False\}$
More generally, given a predicate P(x), we would like to use the formula
    $\{x:P(x)\}$
To mean the set containing those x for which P(x) is true. As seen in the history section though, using any predicate you want for this willy-nilly leads to paradoxes. So every time the formula is used there must be a theorem which states that there is such a set and a theorem that says that such as set is unique. We'll need some machinery to streamline this process.

## Classes

Although the notion of a class is not defined formally in Zermelo-Fraenkel set theory, it is worthwhile to define it informally since it is a useful concept. Specifically, if P(x) is a predicate, then define the class P to be
    $P=\{x:P(x)\}$
Logically, a class $P$ is just a predicate $P(x)$ for which $x\in P$ is shorthand for $P(x)$. We informally think of a class as the collection of all sets that satisfy its defining formula.
Much of what can be said about sets applies to classes as well, as long as you remember that restrictions apply. For one thing a class can only appear on the right side of the ∈ symbol. Also, since classes aren't objects in our universe of discourse, they can't be used in quantifiers. Finally, the = symbol is only defined between sets. We can make a similar definition which applies to classes:
    P=Q when for all x, P(x) iff Q(x)
But keep in mind that the Axiom of Substitution does not apply for this type of equality.
Example: If Q(x) denotes the predicate
    not $(x\in x)$
then Q is the "set" which causes the problem with Russel's paradox. The paradox is avoided because the statement Q∈Q, which puts Q to the left of the ∈ symbol, cannot even be formed legally.
If a is a fixed set, then we can define the predicate A(x) to be
    $x\in a$
Then the class A and the set a have the same elements, in other words:
    $(x\in A)\operatorname {iff} \ (x\in a)$
In some sense you could say that A=a, but we're stepping on shaky ground here because A and a are different types; a is a set while A is technically still a predicate.

## Collectivizing predicates

Contrary to what you might be thinking, this has nothing to do with early 20th century Soviet agriculture. A predicate $P(x)$ is called collectivizing when
    For some $y$, for all $x$, $x\in y$ iff $P(x)$.
(This is an example of a second order predicate, meaning a predicate which applies to predicates rather than objects. Such things don't exist in the logic we've been using so far, but you can think if it as just shorthand for the phrase above.) In less formal language, $P(x)$ is collectivizing when there is a set $y$ whose elements are the $x$ for which $P(x)$ is True.
For example the predicate
    For all $y$, not $y\in x$
is collectivizing since it holds for ∅. On the other hand
    Not $x\in x$
can't be collectivizing because it would allow Russell's paradox discussed in the introduction to this chapter.
To see how this is useful, define the predicate $Q(y)$ to mean
    For all $x$, $x\in y$ iff $P(x)$.
Then $P(x)$ is collectivizing is the same as the existence property for $Q(y)$. If, in addition, we have the uniqueness property then
    The $Y$ for which $Q(Y)$
is well defined. To prove the uniqueness property, we need
    For all $y$, $z$, $Q(y)$ and $Q(z)$ imply $y=z$.
Expanded, this is
    Theorem SO1: For all $y$, $z$, if for all $x$, $x\in y$ iff $P(x)$ and for all $x$, $x\in z$ iff $P(x)$, then $y=z$.
This may seem complicated, but proving it isn't hard. We'll start an outline and leave the details to the reader.
Choose arbitrary $b$ and $c$, we must now prove that if for all $x$, $x\in b$ iff $P(x)$ and for all $x$, $x\in c$ iff $P(x)$, then $b=c$. Assume for all $x$, $x\in b$ iff $P(x)$ and for all $x$, $x\in c$ iff $P(x)$. So the new goal is to prove $b=c$. Axiom S4 says we can do this by showing $b\subseteq c$ and $c\subseteq b$. To prove $b\subseteq c$ we need to prove that for all x, $x\in b$ implies $x\in c$. But for arbitrary $a$ we have $a\in b$ iff $P(a)$ and $P(a)$ iff $a\in c$ so $a\in b$ implies $a\in c$ by Prop. 9 in the Logical equivalence section.

## Defining sets by comprehension

We can now make the following definition:
    Definition SO2: If $P(x)$ is collectivizing, then define
       $\{x:P(x)\}$
    As the set for which
       For all $z$, $z\in \{x:P(x)\}$ iff $P(z)$.
The resulting set is said to be defined by comprehension. For the next few sections we'll follow the same plan; state an axiom or prove a theorem which makes a certain predicate collectivizing, then define notation for the corresponding set.
If $P(x)$ is not collectivizing, and that can happen as we've been stressing, then technically
    $\{x:P(x)\}$
is undefined. It's useful though to think if it as a set-like object called a class.

## Unions

In order to get from singletons and pairs to triples, we'll use a more general method of combining sets. It's usual to start by defining the union of two sets, but this is actually a special case of a more basic operation, namely the union over a set.
    Axiom SO3 (Axiom of unions): For all $z$, the predicate
       For some $y$, $x\in y$ and $y\in z$
    is collectivizing.
Less formally, this says that, given $z$, there is a set $u$ so that $x\in u$ iff $x$ is an element of some element of $z$.
This allows us to make the definition
    Definition SO7: $\bigcup z:=\{x:\operatorname {for\ some} y,x\in y\operatorname {and} y\in z\}$
The expression $\bigcup z$ is read "the union over $z$.
We leave the proofs of the following as exercises:
    Theorem SO8: For all $x$, $z$, $x\in z$ implies $x\subseteq \bigcup z$
    Theorem SO9: For all $x$, $y$, $z$, $(x\in z\operatorname {implies} x\subseteq y)\operatorname {implies} \bigcup z\subseteq y$
Informally, $\bigcup z$ contains every element of $z$ as a subset and is the smallest such set.
To get the usual union of two sets, combine this union with a pair:
    Definition SO10: $x\cup y:=\bigcup \{x,y\}$
We can then prove as a theorem the usual definition:
    Theorem SO11: For all $x$, $y$, $x\cup y=\{z:z\in x\operatorname {or} z\in y\}$
As usual, the proof is left as an exercise.
It's now possible to define triples, quadruples, etc. for as many elements as needed:
    Definition SO12: $\{x,y,z\}:=\{x,y\}\cup \{z\}$
    Definition SO13: $\{x,y,z,u\}:=\{x,y,z\}\cup \{u\}$
Etc.
The proofs of the following are left as exercises:
    Theorem SO14: $\bigcup \varnothing =\varnothing$
    Theorem SO15: For all $x$, $\bigcup \{x\}=x$
    Theorem SO16: For all $x$, $y$, $\bigcup (x\cup y)=(\bigcup x)\cup (\bigcup y)$
    Theorem SO17: For all $x$, $y$, $z$, $\{x,y,z\}=\{x,z,y\}=\{y,z,x\}$
Here, $x=y=z$ is shorthand for $x=y$ and $y=z$.

## Axiom of separation

Before going on to intersections, we need yet another axiom to guarantee they exist. This is a restricted version of comprehension, the idea that any predicate defines a set. This gives it its alternate name, the axiom of restricted comprehension. The unrestricted, and incorrect version says, using the language of classes, that any class is a set. The restricted version says, in effect, any subclass of a set is a set. Written out a bit more formally, this says that for predicates $P(x)$ and $Q(x)$, if for all $x$$P(x)$ implies $Q(x)$ and $Q(x)$ is collectivizing, then $P(x)$ is collectivizing. Yet more formally:
    Axiom SO18 (Separation): For all $z$, if for all x, $P(x)$ implies $x\in z$ then $P(x)$ is collectivizing.
If $R(x)$ is a predicate then $P(x)$ defined as $R(x)$ and $x\in z$ has the required property, so we can make the definition
    $\{x\in z:R(x)\}:=\{x:x\in z\operatorname {and} R(x)\}$
with no restriction on $R(x)$. The fact that any predicate can be used here makes the axiom very powerful, but not so powerful that is leads to a contradiction (at far as anyone knows anyway).
It may be helpful to attempt to use this axiom to reproduce Russell's paradox; presumably the attempt will fail since the idea to avoid contradictions. Let $c$ be a set and define
    $b:=\{x\in c:\operatorname {not} x\in x\}$
Now suppose $b\in b$. Then $b$ fails to meet the criterion not $b\in b$ and so not $b\in b$ a contradiction. Assume, on the other hand, not $b\in b$. Then one of $b\in c$ or not $b\in b$ must be false. The second possibility is true by assumption, so we have not $b\in c$. But this is far from a contradiction and there is no paradox this time.

## Intersections

Intersections are similar to unions except that the 'For some' is replaced by 'for all'. We define intersections following the same plan as for unions. In this case though, we can use the axiom of separation to prove a theorem which replaces the axiom of unions.
    Theorem SO19 (existence of intersections): For all $z$ not equal to ∅, the predicate
       For all $y$, $y\in z$ implies $x\in y$
    is collectivizing.
Less formally, this says that, given $z$, there is a set $n$ so that $x\in n$ iff $x$ is an element of every element of $z$. The assumption $z$ not equal to ∅ will be needed in the proof.
    Proof (outline): Let $Q(x)$ be the predicate
       For all $y$, $y\in z$ implies $x\in y$.
    From not $z=\varnothing$, theorem S8 on the previous page says there is some $w\in z$. Pick one, say $d\in z$. One can now prove that $Q(x)$ implies $x\in d$, and therefore by the axiom of separation, $Q(x)$ is collectivizing.
This allows us to make the definition when $z$ is not ∅:
    Definition SO20: $\bigcap z:=\{x:\operatorname {for\ all} y,y\in z\operatorname {implies} x\in y\}$
The expression $\bigcap z$ is read "the intersecion over $z$. $\bigcap \varnothing$ is left undefined.
To get the usual intersection of two sets, combine this intersection with a pair:
    Definition SO21: $x\cap y:=\bigcap \{x,y\}$
We can then prove as a theorem the usual definition:
    Theorem SO22: For all $x$, $y$, $x\cap y=\{z:z\in x\operatorname {and} z\in y\}$
with the proof is left as an exercise.
    Definition SO23: $x$ and $y$ are disjoint when $x\cap y=\varnothing$. A set $z$ (usually taken to be a set of other sets) is pairwise disjoint if for all $x$, $y$, $x\in z$ and $y\in z$ imply $x=y$ or $x$ and $y$ are disjoint.
In other words $x$ and $y$ are disjoint when they have no elements in common, and $z$ is pairwise disjoint if any two different elements are disjoint.