B2. TRADITIONAL SET THEORY
In this chapter we set out axioms and definitions from traditional set
theory. What we present is a notational variant of standard
Zermelo-Fraenkel set theory (e.g., Cohen, 1966), without the Axiom of
Infinity. We are simply silent on whether entities of infinite
cardinality exist. We will have no occasion in this book to use them.
Sets will be treated as first-class individuals in the logic. They
are viewed as entities in the world that can be referred to by
constants and variables in the logic. To assert that something is a
set, we use the predication "(set s)". The fundamental relation
between sets and their members will be expressed with the predication
"(member x s)". A set is completely defined by its members.
(forall (s1 s2) (1)
(if (set s1)
(iff (equal s1 s2)
(and (set s2)
(forall (x)
(iff (member x s1)(member x s2))))))
That is, sets can only be equal to other sets, and they are equal
when they contain exactly the same members.
The second argument of the predicate "member" is necessarily a set.
There are no constraints on the first argument.
(forall (x s) (2)
(if (member x s)(set s)))
This is the first use we have seen of the predicate "equal". It will
be applied to a number of other kinds of entities as well as we go
along. Its principal properties are the familiar reflexivity,
symmetricity and transitivity.
(forall (x) (equal x x)) (3)
(forall (x y) (iff (equal x y)(equal y x))) (4)
(forall (x y z) (if (and (equal x y)(equal y z)) (5)
(equal x z)))
It is easily verified that equal sets satisfy these properties.
We will use the predicate "nequal" for pairs of entities that are not
equal.
(forall (x y)(iff (nequal x y)(not (equal x y)))) (6)
The null set is the set with no members.
(forall (s) (7)
(iff (null s)
(and (set s)(forall (x)(not (member x s))))))
Sets can be constructed recursively by adding one element at a time.
We will use the predicate "addElt" for this concept.
(forall (s s1 x) (8)
(iff (addElt s s1 x)
(and (set s)(set s1)
(forall (y)
(iff (member y s)
(or (equal y x)(member y s1))))))
This says that s is constructed by adding the element x to s1 exactly
when the members of s are the members of s1, together with x. It is
possible that x is already in s1, in which case s and s1 are equal.
A singleton set consisting of an entity x is defined as follows:
(forall (s x) (9)
(iff (singleton s x)
(exists (s1)
(and (addElt s s1 x)(null s1)))))
This is equivalent to saying that x is the only member of s.
We will also have frequent occasions to refer to sets with exactly two
members, so for this we will introduce a parallel term.
(forall (s x) (10)
(iff (doubleton s x y)
(exists (s1)
(and (nequal x y)(addElt s s1 x)
(singleton s1 y)))))
This is equivalent to saying that x and y are the only members of s.
The predication "(deleteElt s s1 x)" says that the set s is obtained
from set s1 by deleting an element x.
(forall (s s1 x) (11)
(iff (deleteElt s s1 x)
(and (set s)(set s1)
(forall (y)
(iff (member y s)
(and (member y s1)(nequal y x)))))))
That is, the members of s are those members of s1 not equal to x.
Note that we do not require x to be a member of s1. If it is not, s
and s1 will be equal.
The predication "(replaceElt s s1 x y)" says that set s is obtained
from set s1 by replacing element x with element y.
(forall (s s1 x y) (12)
(iff (replaceElt s s1 x y)
(exists (s2)
(and (deleteElt s2 s1 x)
(addElt s s2 y)))))
That is, to get s, we delete x from s1 and add y to the result. If x
is not a member of s1, replaceElt amounts to adding y. If y is
already in s1, replaceElt amounts to deleting x.
The union of two sets is defined in the standard way.
(forall (s s1 s2) (13)
(iff (union s s1 s2)
(and (set s)(set s1)(set s2)
(forall (x)
(iff (member x s)
(or (member x s1)(member x s2)))))))
That is, set s is the union of sets s1 and s2 if its members are
members of either s1 or s2.
We will often have occasion to take the union of three sets, so we
define a predicate for this.
(forall (s s1 s2 s3) (14)
(iff (union3 s s1 s2 s3)
(exists (s4)
(and (union s s1 s4)(union s4 s2 s3)))))
That is, we perform two unions.
Set difference is defined similarly to union.
(forall (s s1 s2) (15)
(iff (setdiff s s1 s2)
(and (set s)(set s1)(set s2)
(forall (x)
(iff (member x s)
(and (member x s1)
(not (member x s2))))))))
Set s is the set difference between s1 and s2 exactly when the members
of s are the members of s1 less the members of s2.
The definition of the "subset" relation is as follows:
(forall (s1 s2) (16)
(iff (subset s1 s2)
(and (set s1)(set s2)
(forall (x)(if (member x s1)(member x s2)))))
A proper subset is a subset which is not equal.
(forall (s1 s2) (17)
(iff (properSubset s1 s2)
(and (subset s1 s2)(nequal s1 s2))))
Two sets are disjoint if they have no members in common.
(forall (s1 s2) (18)
(if (and (set s1)(set s2))
(iff (disjoint s1 s2)
(not (exists (x)
(and (member x s1)(member x s2)))))))
We have conditioned this definition on the arguments being sets
because in Chapter B8 we will extend it to cover scales as well.
The power set of a set is the set of all its subsets.
(forall (s0 s) (19)
(iff (powerSet s0 s)
(forall (s1)(iff (member s1 s0)(subset s1 s)))))
Finally, we define cardinality recursively with the set construction
predicate "addElt". We assume addition of integers; "(sum n n1 n2)"
means that n is the sum of n1 and n2. In addition, we assume the
numbers 0 and 1 and the predicate "nonNegInteger".
(forall (n s) (20)
(iff (card n s)
(and (nonNegInteger n)(set s)
(or (and (null s)(equal n 0))
(and (exists (s1 x m)
(and (addElt s s1 x)
(not (member x s1))
(card m s1)
(sum n m 1))))))))
That is, the cardinality of the null set is zero. The cardinality
of a set s obtained by adding a new element x to a set s1 is one more
than the cardinality of s1.
It will occasionally be useful to talk about sets of eventualities.
(forall (s) (21)
(iff (eventualties s)
(and (set s)
(forall (e)
(if (member e s)(eventuality e))))))
The predicate "eventualities" is true of sets all of whose members are
eventualities.
Predicates Introduced in this Chapter
(set s): s is a set.
(member x s): x is a member of s.
(equal x y): x is equal to y.
(nequal x y): x is not equal to y.
(null s): s is the null set or empty set.
(addElt s s1 x): s is obtained from s1 by adding x.
(singleton s x): s consists of the single element x.
(doubleton s x y): s consists of the two elements x and y.
(deleteElt s s1 x): s is obtained from s1 by deleting x.
(replaceElt s s1 x y): s is obtained from s1 by replacing x with y.
(union s s1 s2): s is the union of s1 and s2.
(union3 s s1 s2 s3): s is the union of s1, s2 and s3.
(setdiff s s1 s2): s is the set difference of s1 and s2.
(subset s1 s2): s1 is a subset of s2.
(properSubset s1 s2): s1 is a proper subset of s2.
(disjoint s1 s2): s1 and s2 are disjoint.
(powerSet s0 s): s0 is the set of all of s's subsets.
(card n s): n is the cardinality of s.
(eventualities s): s is a set of eventualties.
In addition, we used the predicates "sum" and "nonNegInteger" and the
constants 0 and 1, which will be discussed in Chapter B9.
References:
Cohen, Paul J., 1966. {\it Set Theory and the Continuum Hypothesis},
W. A. Benjamin, Inc., New York.