The presence of sets in our universe of discourse does not in itself
lead to paradoxes. The paradoxes appear only when we try to define
set primitives that are too powerful. We have defined the sentence `(member )` to be true in exactly those cases when the object
denoted by is a member of the set denoted by , and we might
consider defining the term `(setofall )` to mean simply the
set of all objects denoted by for any assignment of the free
variables of that satisfies . Unfortunately, these two
definitions quickly lead to paradoxes.

Let be the result of substituting term for
all free occurrences of in sentence . Provided that
is a term not containing any free variables captured in
, then the following schema follows from our informal
definition. This schema is called the *principle of unrestricted
set abstraction*.

`(<=> (member (setofall )) )`

Now, let us substitute the variable `?x` for , the sentence
`(not (member ?x ?x))` for , and the term `(setofall
?x (not (member ?x ?x)))` for . The resulting instance of
the principle of unrestricted set abstraction follows.

(<=> (member (setofall ?x (not (member ?x ?x))) (setofall ?x (not (member ?x ?x)))) (not (member (setofall ?x (not (member ?x ?x)))) (setofall ?x (not (member ?x ?x)))))

This sentence has the form `(<=> (not ))`, which
cannot be true in any interpretation. This is Russell's paradox, only
one of a family of familiar absurdities following from the principle of
unrestricted set abstraction.

It is crucial that the paradoxes of set theory be avoided. One of the goals in the design of KIF is that it have a clearly specified model-theoretic semantics in terms of which the concepts of entailment, equivalence, consistency, soundness and completeness can be defined. If the paradoxes are allowed to persist in principle, even if they are easy to avoid in practice, the consequence would be that no KIF theory would be true in any model. Definitions couched in terms of models would be trivialized, becoming useless. All sentences would be entailed by any theory, any two theories would be equivalent, no theory would be consistent, every possible inference rule would be sound, and so on.

In the von-Neuman-Gödel-Bernays version of set theory, these paradoxes
are avoided by replacing the principle of unrestricted set abstraction with
the *principle of restricted set abstraction* given above.

`(<=> (member (setofall ))`` (and (bounded ) ))`

With this principle, there are two reasons why something may be
excluded from a set `(setofall )`. It may fail to be a
member because it does not satisfy the defining condition , or it
may be excluded because it is an unbounded object.
Conditioning the membership of objects in this set on their boundedness effectively
eliminates the paradoxes.

Wed Dec 7 13:23:42 PST 1994