fom
Posts:
1,968
Registered:
12/4/12


Re: Just another exposition of MK.
Posted:
Mar 17, 2013 2:30 AM


On 3/16/2013 1:08 PM, Zuhair wrote: > On Mar 16, 9:33 am, Zuhair <zaljo...@gmail.com> wrote: >> 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 > > Another reformulation along the same lines is: > > Define: Set(X) iff {X,..} exists. > > Extensionality: X C Y & Y C X > X=Y > Class comprehension: {xSet(x) phi} exists. > Pairing: X C {a,b} > Set(X) > Subsets: Set(X) & Y C X > Set(Y) > Size limitation: X<V > Set(H(TC(X))) > > C is sublcass relation. > TC(X) is the transitive closure of X. > H(X) is the Class of all sets hereditarily subnumerous to X. > > Possibly (I'm not sure) pairing is redundant. >
How does your pairing axiom assert the existence of pairs?
Are you assuming that the monadic Set() predicate is satisfied for every finite and transfinite enumeration?

