Date: Feb 20, 2013 6:01 PM
Author: Zaljohar@gmail.com
Subject: An equivalent of MK-Foundation-Choice

This is just a cute result.

The following theory is equal to MK-Foundation-Choice

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. Size limitation
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