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
editAlthough 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 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
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
editContrary 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
editWe 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
editIn 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
editBefore 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
editIntersections 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.