[FOM] Con(ZF) proved from three basic themes

[Zuhair Abdul Ghafoor Al-Johar]

Dear FOMers,
Another shorter axiomatization of the theory quoted below is the present one. This Theory depends on two themes that of Construction
and Size. It interprets MK over the realm of well founded sets of it.

Def.) elm(x):= [y](x e y) 

I. Construction: if phi is a formula in which x is not free, then
([!x](y)(y e x <-> elm(y) & phi)) is an axiom. 

Def.) x < y:= [f](f:x-->y & f is an injection) 

Def.) x <" y:= x < y & (z)(z e TC(x) -> z < y) 

Def.) y << x:= [f](f:x-->y & (z)(z e y\rng(f) -> z <" U(x))) 

Def.) accessible(x):= [=<2y](y e x) ? [y](elm(y) & x << y) 

II. Size: (x)(accessible(x) -> elm(x)) 

/ 

Where [=<2y] stands for there exist at most two sets y; TC,\,rng and U
stand for Transitive Closure, exception, range and Union respectively
defined in the standard manner. 

Notation at: http://zaljohar.tripod.com/logic.txt

Best Regards
Zuhair Al-Johar


At Mon, 12 Dec 2011 03:12:42 -0800 (PST)
Zuhair Abdul Ghafoor Al-Johar <zaljohar at yahoo.com>
wrote:
> 
> Dear FoMers,
> 
>  The following theory of mine interpret ZF under
> the realm of well founded elements of it, it also
> proves the consistency of ZF by defining its model.
> 
> ONTOLOGY: every object this theory speaks about is
> termed as a "set", however there are two kinds of sets,
> those that are elements of sets, those are termed as
> "elements", and those that are not elements of any
> set, those are termed as "proper sets". This theory
> do not contain objects that are elements of sets but
> are themselves not sets (i.e. proper elements), so
> all elements here are sets, but not all sets are elements.
> So the term "set" here is used instead of the term "class"
> used in Morse-Kelley's; while the term "element" here is
> used instead of the term "set" used in Morse-Kelley's.
> 
> EXPOSITION:
> 
> T is a theory in FOL with identity and membership with the
> following axioms:
> 
> Def.) elm(x):=[y](x e y)
> 
> elm(x) is read as "x is an element".
> 
> I. Construction: if phi is a formula in which x is not
> free, then
> ([!x](y)(y e x <-> elm(y) & phi)) is an axiom.
> 
> Def.) trs(t):= (x)(x e t -> x c t)
> 
> Def.) TC(x)=y:= (z)(z e y <-> (t)(trs(t) & x c t
> ->z e t))
> 
> 
> II. Relations: (a)(b)(x)((y)(y e x -> y=a ? y=b) ->
> elm(x))
> 
> Def.) x < y:= [f](f:x-->y & f is injection)
> 
> Def.) x <" y:= x < y & (z)(z e TC(x) -> z <
> y)
> 
> 
> III. Size axioms:
> 
> (x)(y)(elm(x) & y < x -> elm(y))
> 
> (x)(y)(elm(x) & (z)(z e y ->[u](u e x & z <"
> u)) -> elm(y))
> 
> / 
>