
Just another exposition of MK.
Posted:
Mar 16, 2013 2:33 AM


Define: Set(x) iff {x,..}
Extensionality: x C y & y C x > x=y
Comprehension: {x Set(x) & phi}
Pairing: x C {a,b} > Set(x)
Generation: Set(x) & y C H(x) > Set(y)
where H(x)={z m in TC({z}). m =< x}
Size: x < V > Set(U(x))
where TC, U stand for transitive closure, union respectively defined in the customary manner; C is subclass relation;   =<   and   <   relations are defined in the standard manner.
The theory above minus axiom of Size is sufficient to prove consistency of Z. With the axiom of Size it can prove the consistency of ZF+Global choice, and it is equiinterpretable with MK+Global choice.
Zuhair

