To allow us to name specific sets, KIF provides the operators `setof` and `setofall`.

The term `(setof ... )` denotes the set consisting of
the objects denoted by , ..., that are bounded.

`(=> (item ?x (listof @items))`

` (bounded ?x)`

` (member ?x (setof @items)))`

`(=> (member ?x (setof @items))`

` (item ?x (listof @items)))`

Note that the cardinality of the set denoted by `(setof ...
)` can be less than . By definition, an object can appear in
a set only once. Consequently, if and (for different
and ) denote the same object, the resulting set must contain
fewer than members.

The operator `setofall` allows us to define sets in terms of their
properties. The term `(setofall )` denotes the set of
all bounded objects denoted by for any assignment of the free
variables in that satisfies .

`(<=> (member (setofall ))`` (and (bounded ) ))`

Note that the first argument to `setofall` must be a term,
not a list of variables as with `forall` and `exists`. The
term can be a single variable, a functional expression, or even a
quantified term. If the term contains no free variables, then the
set consists of either zero members or one member, depending on the
truth value of the embedded sentence.

The `empty` relation is true of the empty set but false of all other
objects.

`(defrelation empty (?x) := (= ?x (setof)))`

In KIF, the functions `union`, `intersection`, `difference`, and
`complement` are defined as follows.

`(deffunction union (@sets) :=`

` (if (forall (?s) (=> (item ?s (listof @sets)) (set ?s)))`

` (setofall ?x (exists (?s) (and (item ?s (listof @sets))`

` (member ?x ?s)))))`

`(deffunction intersection (@sets) :=`

` (if (forall (?s) (=> (item ?s (listof @sets)) (set ?s)))`

` (setofall ?x (forall (?s) (=> (item ?s (listof @sets))`

` (member ?x ?s)))))`

`(deffunction difference (?set @sets) :=`

` (if (and (set ?set)`

` (forall (?s) (=> (item ?s (listof @sets)) (set ?s))))`

` (setofall ?x`

` (and (member ?x ?set)`

` (forall (?s) (=> (item ?s (listof @sets))`

` (not (member ?x ?s))))))))`

`(deffunction complement (?s) :=`

` (if (set ?s)`

` (setofall ?x (not (member ?x ?s)))))`

The functions `generalized-union` and `generalized-intersection` allow us to
talk about the union and intersection of the sets in a set of sets.

`(deffunction generalized-union (?set) :=`

` (if (and (set ?set)`

` (forall (?s) (=> (member ?s ?set) (set ?s)))`

` (setofall ?x (exists (?s) (and (member ?s ?set) `

` (member ?x ?s))))))`

`(deffunction generalized-intersection (?set) :=`

` (if (and (set ?set)`

` (forall (?s) (=> (member ?s ?set) (set ?s)))`

` (setofall ?x (exists (?s) (=> (member ?s ?set) `

` (member ?x ?s))))))`

The sentence `(subset )` is true if
and only if and are sets and the objects in the set
denoted by are contained in the set denoted by .

`(defrelation subset (?s1 ?s2) :=`

` (and (set ?s1) (set ?s2)`

` (forall ?x (=> (member ?x ?s1) (member ?x ?s2)))))`

The sentence `(proper-subset )` is true if
the set denoted by is a subset of the set denoted by
but not vice-versa.

`(defrelation proper-subset (?s1 ?s2) :=`

` (and (subset ?s1 ?s2)`

` (not (subset ?s2 ?s1))))`

Two sets are disjoint if and only if there is no object that is a member of both sets. Sets are pairwise-disjoint if and only if every set is disjoint from every other set. Sets are mutually-disjoint if and only if there is no object that is a member of all of the sets. Note that mutually-disjoint sets need not be pairwise disjoint; in fact, every pair of sets might be overlapping. For example, the sets and and are mutually disjoint but not pairwise disjoint.

`(defrelation disjoint (?s1 ?s2) :=`

` (empty (intersection ?s1 ?s2)))`

`(defrelation pairwise-disjoint (@sets) :=`

` (forall (?s1 ?s2) (=> (item ?s1 (listof @sets))`

` (item ?s2 (listof @sets))`

` (or (= ?s1 ?s2) (disjoint ?s1 ?s2)))))`

`(defrelation mutually-disjoint (@sets) :=`

` (= (intersection @sets) (set)))`

`(defrelation set-partition (?s @sets) :=`

` (and (= ?s (union @sets))`

` (pairwise-disjoint @sets)))`

`(defrelation set-cover (?s @set) :=`

` (subset ?s (union @sets)))`

We close this section with two axioms that allow us to conclude that sets of
various sorts do, in fact, exist. The first is the *axiom of regularity*
- every non-empty set has an element with which it has no members in common.

`(forall (?s)`

` (=> (not (empty ?s))`

` (exists (?u) (and (member ?u ?s) (disjoint ?u ?s)))))`

This axiom is not absolutely essential for set theory. However, it makes many proofs a lot easier, and so it is commonly included among the axioms of set theory.

The second axiom is the *axiom of choice*. It asserts that there
is a set that associates every bounded set with a distinguished
element of that set. In effect, it *chooses* an element from
every bounded set.

`(exists (?s)`

` (and (set ?s)`

` (forall (?x) (=> (member ?x ?s) (double ?x)))`

` (forall (?x ?y ?z) (=> (and (member (listof ?x ?y) ?s)`

` (member (listof ?x ?z) ?s))`

` (= ?y ?z)))`

` (forall (?u)`

` (=> (and (bounded ?u) (not (empty ?u)))`

` (exists (?v) (and (member ?v ?u)`

` (member (listof ?u ?v) ?s))))))))`

Again, this axiom is not essential. In some versions of set theory, the axiom of choice is omitted. However, it is a highly desirable property and is included here for that reason.

Wed Dec 7 13:23:42 PST 1994