
Re: A reformulation of MKFoundationChoice: Even more compact!
Posted:
Mar 23, 2013 2:36 PM


On Mar 23, 8:33 pm, Zuhair <zaljo...@gmail.com> wrote: > This is even more compact reformulation of MKFoundationChoice. > > Unique 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. > > Size limitation: Set({}) & [Set(x) & y =< H(TC(x)) > Set(y)] > / > > Def.) y C x iff for all z (z in y > z in x) > Def.) y =< x iff y C x Or Exist f (f:y>x & f is injective) > Def.) TC(x)= {y for all t. t is transitive & x C t > y in t} > Def.) t is transitive iff for all m,n(m in n & n in t > m in t) > Def.) H(x)={y for all z. z in TC(y) or z=y > z =< x} > > It is nice to see that only one axiom can prove the existence of all > sets in ZF. > So Pairing, Union, Power, Infinity, Separation and Replacement All are > provable over sets. Of course Foundation and Choice are interpretable > in this theory. > Con(ZFC) is actually Provable in this theory. > > Zuhair
Set(x) is defined as in MK, i.e. by being a member of a class.
Zuhair

