[FOM] ZFC with Classes (ZFCC?)
Victor Makarov
viktormakarov at hotmail.com
Tue May 18 23:47:27 EDT 2004
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
More information about the FOM
mailing list