Search All of the Math Forum:
Views expressed in these public forums are not endorsed by
NCTM or The Math Forum.



An equivalent of MKFoundationChoice
Posted:
Feb 20, 2013 5:58 PM


This is just a cute result.
The following theory is equal to MKFoundationChoice
Language: FOL(=,e)
Define: Set(x) iff Ey. x e y
Axioms: ID axioms+
1.Extensionality: (Az. z e x <> z e y) > x=y
2. Construction: if phi is a formula in which x is not free, then (ExAy.y e x<>Set(y)&phi) is an axiom
3. Pairing: (Ay. y e x > y=a or y=b) > Set(x)
4. Set(x) <> Ey. y is set sized & Azex(Emey(z<<m))
where y is set sized iff Es. Set(s) & y =< s and z<<m iff z =<m & AneTC(z).n =<m
TC(z) stands for 'transitive closure of z' defined in the usual manner as the minimal transitive class having z as subclass of; transitive of course defined as a class having all its members as subsets of it.
y =< s iff Exist f. f:y>s & f is injective.
/
Of course this theory PROVES the consistency of ZFC. Proofs had all been worked up in detail. It is an enjoying experience to try figure them out.
Zuhair



