[FOM] Finite Axiomatization of Class Theory

[Harvey Friedman]

It appears that one can give simple finite axiomatizations for some major
f.o.m. systems.

It is well known that ZF is not finitely axiomatizable, but we can suitably
add a new sort for classes, and finitely axiomatized NBG (von Neumann
Bernays Godel). 

However, I have not seen any really simple finite axiomatization of NBG.

There is an obvious modification of NBG in which we add not classes of sets,
but rather binary relations on sets (these can be viewed as classes of
ordered pairs). 

Then we can give some very simple finite set of axioms for this system,
which is of course a conservative extension of ZF.

Again, this will be made into a numbered posting if it survives the scrutiny
of the FOM list. 

We start with a simple characterization of the binary relations on the
universe of sets (class relations) that are first order definable over the
universe of sets. 

THEOREM 1. The binary relations on the class V of all sets, that are
definable without parameters over (V,epsilon) forms the least family of
binary relations on V such that

i) the epsilon relation and the equality relation are in the family;
ii) the complement and the union of any relations in the family are again in
the family;
iii) the reverse (inverse) of any relation in the family is in the family;
iv) the composition of any two relations in the family is in the family.

Composition is defined as follows. Let R,S be binary relations. Then

T(x,y) if and only if (therexists z)(R(x,z) and S(z,y))

is the composition of R and S.

THEOREM 2. The binary relations on the class V of all sets, that are
definable with parameters over (V,epsilon) forms the least family of binary
relations on V such that

i) the epsilon relation and the equality relation are in the family;
ii) the complement and the union of any relations in the family are again in
the family;
iii) the reverse (inverse) of any relation in the family is in the family;
iv) the composition of any two relations in the family is in the family.
v) for every set b, the relation R(x,y) if and only if y = b is in the
family.

One can build a nice term calculus for designating first order binary
relations on sets, with these operations.

I know that Tarski and colleagues worked on various axiomatization issues
like this, in set theory and elsewhere. But I don't know if they looked at
things quite this way?

Here is the corresponding axiomatization of class theory. There are two
sorts: sets and binary relations on sets. We use lower case letters for set
variables, and upper case letters for class variables.

The atomic formulas are

1. x epsilon y.
2. x = y.
3. R(x,y).

The axioms are as follows.

1. Two sets are equal iff they have the same elements.
2. There is a set consisting of any two given sets.
3. There is a set consisting of the elements of elements of any given set.
4. There is a set consisting of the subsets (appropriately defined) of any
given set. 
5. There is a nonempty set with no epsilon maximal element.
6. Every nonempty set has an epsilon minimal element.
7. (forall x in y)(therexists unique z)(R(x,z)) implies (therexists
w)(forall z)(z in w iff (therexists x in y)(R(x,z))).
8. Every relation has a complement.
9. Any two relations have a union.
10. The epsilon relation on sets exists.
11. The equality relation on sets exists.
12. Every relation has a reverse (inverse).
13. Any two relations have a composition.

Harvey Friedman