In many applications, it is helpful to talk about sets of objects as objects in their own right, e.g. to specify their cardinality, to talk about subset relationships, and so forth.
The formalization of sets of simple objects is a simple matter; but, when we begin to talk about sets of sets, the job becomes difficult due to the threat of paradoxes (like Russell's hypothesized set of all sets that do not contain themselves).
Fortunately, there is no shortage of mathematical theories for our use in KIF - various higher order logics, Zermelo-Fraenkel set theory, von Neuman-Bernays-Gödel set theory, Quine's variants on the previous two approaches, the more recently elaborated proposals by Feferman and Aczel, and so forth. In KIF, we have adopted a version of the von Neumann-Bernays-Gödel set theory.
In our presentation here, we first discuss the basic concepts of this theory - the notions of set and membership. Next, we look at some terminology for describing the properties of sets. We then present the standard axioms of set theory. Finally, we discuss the threat of paradox and indicate how our use of the von Neumann-Bernays-Gödel set theory avoids this problem.
An important word of warning for mathematicians. In KIF, certain words are used nontraditionally. Specifically, the standard notion of class is here called a set; the standard notion of set is replaced by the notion of bounded set; and the standard notion of proper class is replaced by unbounded set.