Date: Feb 8, 2013 7:27 AM
Author: Zaljohar@gmail.com
Subject: A natural theory proving Con(ZFC)

I see the following theory a natural one that proves the consistency
of ZFC.

Language: FOL(=,in)

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
surjection.

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.

Zuhair