next up previous
Next: Boundedness Up: Sets Previous: Basic Concepts


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.

next up previous
Next: Boundedness Up: Sets Previous: Basic Concepts

Vishal I. Sikka
Wed Dec 7 13:23:42 PST 1994