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:

The empty set can be made to fit this pattern using

More generally, given a predicate P(x), we would like to use the formula

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 edit

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

 

Logically, a class   is just a predicate   for which   is shorthand for  . 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  

then Q is the "set" which causes the problem with Russel's paradox. The paradox is avoided because the statement QQ, 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

 

Then the class A and the set a have the same elements, in other words:

 

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 edit

Contrary to what you might be thinking, this has nothing to do with early 20th century Soviet agriculture. A predicate   is called collectivizing when

For some  , for all  ,   iff  .

(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,   is collectivizing when there is a set   whose elements are the   for which   is True.

For example the predicate

For all  , not  

is collectivizing since it holds for ∅. On the other hand

Not  

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   to mean

For all  ,   iff  .

Then   is collectivizing is the same as the existence property for  . If, in addition, we have the uniqueness property then

The   for which  

is well defined. To prove the uniqueness property, we need

For all  ,  ,   and   imply  .

Expanded, this is

Theorem SO1: For all  ,  , if for all  ,   iff   and for all  ,   iff  , then  .

This may seem complicated, but proving it isn't hard. We'll start an outline and leave the details to the reader.

Choose arbitrary   and  , we must now prove that if for all  ,   iff   and for all  ,   iff  , then  . Assume for all  ,   iff   and for all  ,   iff  . So the new goal is to prove  . Axiom S4 says we can do this by showing   and  . To prove   we need to prove that for all x,   implies  . But for arbitrary   we have   iff   and   iff   so   implies   by Prop. 9 in the Logical equivalence section.

Defining sets by comprehension edit

We can now make the following definition:

Definition SO2: If   is collectivizing, then define
 
As the set for which
For all  ,   iff  .

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   is not collectivizing, and that can happen as we've been stressing, then technically

 

is undefined. It's useful though to think if it as a set-like object called a class.

Unions edit

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  , the predicate
For some  ,   and  
is collectivizing.

Less formally, this says that, given  , there is a set   so that   iff   is an element of some element of  .

This allows us to make the definition

Definition SO7:  

The expression   is read "the union over  .

We leave the proofs of the following as exercises:

Theorem SO8: For all  ,  ,   implies  
Theorem SO9: For all  ,  ,  ,  

Informally,   contains every element of   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:  

We can then prove as a theorem the usual definition:

Theorem SO11: For all  ,  ,  

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:  
Definition SO13:  

Etc.

The proofs of the following are left as exercises:

Theorem SO14:  
Theorem SO15: For all  ,  
Theorem SO16: For all  ,  ,  
Theorem SO17: For all  ,  ,  ,  

Here,   is shorthand for   and  .

Axiom of separation edit

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   and  , if for all    implies   and   is collectivizing, then   is collectivizing. Yet more formally:

Axiom SO18 (Separation): For all  , if for all x,   implies   then   is collectivizing.

If   is a predicate then   defined as   and   has the required property, so we can make the definition

 

with no restriction on  . 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   be a set and define

 

Now suppose  . Then   fails to meet the criterion not   and so not   a contradiction. Assume, on the other hand, not  . Then one of   or not   must be false. The second possibility is true by assumption, so we have not  . But this is far from a contradiction and there is no paradox this time.

Intersections edit

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   not equal to ∅, the predicate
For all  ,   implies  
is collectivizing.

Less formally, this says that, given  , there is a set   so that   iff   is an element of every element of  . The assumption   not equal to ∅ will be needed in the proof.

Proof (outline): Let   be the predicate
For all  ,   implies  .
From not  , theorem S8 on the previous page says there is some  . Pick one, say  . One can now prove that   implies  , and therefore by the axiom of separation,   is collectivizing.

This allows us to make the definition when   is not ∅:

Definition SO20:  

The expression   is read "the intersecion over  .   is left undefined.

To get the usual intersection of two sets, combine this intersection with a pair:

Definition SO21:  

We can then prove as a theorem the usual definition:

Theorem SO22: For all  ,  ,  

with the proof is left as an exercise.

Definition SO23:   and   are disjoint when  . A set   (usually taken to be a set of other sets) is pairwise disjoint if for all  ,  ,   and   imply   or   and   are disjoint.

In other words   and   are disjoint when they have no elements in common, and   is pairwise disjoint if any two different elements are disjoint.