
Re: An equivalent of MKFoundationChoice
Posted:
Feb 21, 2013 7:39 AM


On Feb 21, 2:01 am, Zuhair <zaljo...@gmail.com> wrote: > 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. Size limitation > Set(x) <> Ey. y is set sized & Azex(Emey(z<<m)) > > where y is set sized iff Es. Set(s) & y =< s
An artificial fix is to define "set sized" in the following manner:
y is set sized iff [(E<3mey) or Es.Set(s)&y=<s]
where E<3mey means: there exist strictly less than 3 members in y.
[E<3mey] iff Ea,bAzey(z=a or z=b)
This obviates the need for axiomatizing pairing.
Anyhow this is just an artificial mix.
Zuhair

