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)))