```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 consistencyof ZFC.Language: FOL(=,in)Define: set(x) iff  Exist y. x in yAxioms: 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 min 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 asurjection.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 < yTC(x) is defined as:TC(x)=y iff [for all z. z in y iff (for all s. x subclass_of s & s istransitive -> 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 proveZFC, that of Unique Construction of classes, and Size criteria.Zuhair
```