In KIF, a fundamental distinction is drawn between *individuals* and
*sets*. A set is a collection of objects. An individual is any object that
is not a set.

A distinction is also drawn between objects that are *bounded* and those
that are *unbounded*. This distinction is orthogonal to the distinction
between individuals and sets. There are bounded individuals and unbounded
individuals. There are bounded sets and unbounded sets.

The fundamental relationship among these various types of entities is that
of membership. Sets can have members, but individuals cannot. Bounded objects can
*be* members of sets, but unbounded objects cannot. (It is this condition that
allows us to avoid the traditional paradoxes of set theory.)

In KIF, we use the unary relation constants `individual` and `set`, `bounded` and `unbounded` to make these distinctions; and we
use the binary relation constant `member` to talk about membership.

The sentence `(individual )` is true if and only if the object
denoted by is an individual. The sentence `(set )` is
true if and only if the object denoted by is a set. As just
described, individuals and sets are exhaustive and mutually disjoint.

`(or (set ?x) (individual ?x))`

`(or (not (set ?x)) (not (individual ?x)))`

The sentence `(bounded )` is true if and only if the object denoted
by is bounded. The sentence `(unbounded )` is true if
and only if the object denoted by is unbounded. Boundedness and
unboundedness are exhaustive and mutually disjoint.

`(or (bounded ?x) (unbounded ?x))`

`(or (not (bounded ?x)) (not (unbounded ?x)))`

The sentence `(member )` is true if and only if the
object denoted by is contained in the set denoted by .
As mentioned above, an object can be a member of another object if and only
if the former is bounded and the latter is a set.

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

` (bounded ?x))`

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

` (set ?x))`

An important property shared by all sets is the extensionality property. Two sets are identical if and only if they have the same members.

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

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

` (= ?s1 ?s2)))`

Wed Dec 7 13:23:42 PST 1994