From: zuhair on
Phi is said to be a *self binary relation formula* if Phi has only one
free variable in it, and that variable appears twice in Phi.

Examples:y=y, y e y ,~ y e y ,
for all m,n ((m e n & n e y) -> m e y ),
Exist x ( x e y & ~ y e x ) ,
Exist z ( z e y & ~ Exist c ( c e z & c e y ) )

Phi is said to be a *self comparing formula* if a sub-formula of Phi
is a self
binary relation formula.

Example: any self binary relation formula.

Another example is the formula

For all x ( x subset of y -> Exist z ( z e x & ~ Exist c ( c e z & c e
x ) ) )

Phi is not a self comparing formula if all its sub-formulas are not
binary self
relation formulas.

Examples: "y=a or y e a" ,
for all z ( z e y -> z e a ),
~ y e a ,
~ a e y.


DEFINITION OF SET THEORY "T".

T is the set of all sentences entailed ( from FOL with identity '='
and
epsilon membership 'e' ) by the axiom schema outlined below the
following
definition:

Define (set):
x is a set iff for all y ( for all z ( z e y iff z e x) -> y=x )
or equivalently:
x is a set iff ~ exist y ( ~ y=x & for all z ( z e y iff z e x) )

Axiom Schema of Comprehension: If Phi is not a self comparing
formula; having at least y free, and in which x is not free, then
all closures of

Exist a set x for all y ( y e x iff Phi )

are axioms.

Theory definition finished/

Zuhair