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.