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.

Wed Dec 7 13:23:42 PST 1994