Date: Feb 8, 2013 7:27 AM
Subject: A natural theory proving Con(ZFC)
I see the following theory a natural one that proves the consistency
Define: set(x) iff Exist y. x in y
Axioms: Identity axioms +
(1) Extensionality: (for all z. z in x iff z in y) -> x=y
(2) Comprehension: if phi is a formula in which x is not free then
(Exist x. for all y. y in x iff set(y) & phi) is an axiom.
(3) Pairing: (for all y. y in x -> y=a or y=b) -> set(x)
(4) Hereditary size limitation: set(x) <-> Exist y. set(y) & for all m
in x (m << y)
(5) Simple size limitation: set(x) & y < x -> set(y)
where relations <, << are defined as:
x < y iff Exist z. z suclass_of y & Exist f. f:z --> x & f is a
where z subclass_of y iff for all m. m in z -> m in y.
x << y iff x < y & for all z in TC(x). z < y
TC(x) is defined as:
TC(x)=y iff [for all z. z in y iff (for all s. x subclass_of s & s is
transitive -> z in s)]
where transitive is defined as:
x is transitive iff (for all y,z. z in y & y in x -> z in x)
In nutshell there are mainly two scenarios here essential to prove
ZFC, that of Unique Construction of classes, and Size criteria.