Basic Concepts

Next: Sets Up: Sets Previous: Sets

## Basic Concepts

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

Next: Sets Up: Sets Previous: Sets

Vishal I. Sikka
Wed Dec 7 13:23:42 PST 1994