[FOM] ZFC with Classes (ZFCC?)

[Victor Makarov]

Dear FOMers:

It seems, that set theories with classes are important

for practical formalization of mathematics (see,for example, the paper

"STMM: A Set Theory for Mechanized Mathematics" by William M. Farmer

published in the Journal of Automated Reasoning, 26:269–289, 2001.
(see also http://imps.mcmaster.ca/doc/stmm.pdf )

STMM is based on NBG.

But because ZFC is considered as "the gold standard",
it would be very desirable to suggest also something like "ZFC with Classes 
(ZFCC)"

- that is, a set theory with classes, as close as possible to ZFC
(at least, more close than the other set theories with classes).

My question is:  maybe someone did it?  Google search for "ZFCC"
returned nothing relevant. So below is a short description of the idea 
"ZFCC", as I understand it.

(the variables X,Y,Z are used for classes, x,y,z - for sets)

ZFCC is a first order theory with equality
(though  the equality is a defined symbol in ZFC,
it seems more practical to have it as a primitive symbol)

and with the following 2 relational symbols:

Set - of arity 1,  (Set(X) means "the class X is a set")
in  - of arity 2.  (X in Y is considered as a well-formed
                    only if Set(X) is a theorem and means "X is a member of 
Y")

There is also a new kind of terms -
abstraction terms of the form {x | Q(x)} where Q(x) is a formula.

Usual set-theoretic notations can be defined:

("A[x" means "for all x", "E[x" - "there exists such x, that", "==" - 
equivalence)

(X <= Y) := A[x, x in X -> x in Y];       (X is a subclass of Y)
Union(X) := {y | E[x, x in X & y in x]};  (the union of X)
P(X) := {x | x <= X};                         (the class of all subsets of X
{} := {x | x # x};                               (the empty class)
{x} := {z | z = x};                              (the singleton {x})
{x,y} := {z | z = x or x = y};               (the pair {x,y})
R[x:X,f(x)] := {y| E[x, x in X & y = f(x)]; (the range of f(x) on X)

The axioms of ZFCC are as follows :

0) z  in {x | Q(x)} == Q(z);     ( Axiom Schemata: defining axioms for {x|Q} 
);

1) X <= Y & Y <= X -> X = Y;    (Axiom of Extensionality)

2) Set({x, y});                       (Axiom of Pairing)

3) Set(X) -> Set(Union(X));     (Axiom of Union)

4) Set(X) -> Set(P(X));           (Axiom of Power-Set)

5) Set(X) -> Set({x:X | p});    (Axiom Schema of Subsets, p is any formula)

6) E[s,{} in s & A[x, x in s -> {x, {x}} in s]]; (Axiom of Infinity)

7) Set(X) -> Set(R[x:X, f(x)]);      (Axiom Schema of Replacement,
   f(x) is any set term possibly containing x).

The remaining 2 axioms (Axiom of Choice and Axiom of Foundation)
are essentially the same as the corresponding axioms in ZFC.

I would be very grateful for any comments and references.

Thanks in advance,

Victor Makarov

http://home.nyu.edu/~yvm204/vm/vm.htm