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

[Zuhair Abdul Ghafoor Al-Johar]

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))

/ 

Key to notations is found at: http://zaljohar.tripod.com/logic.txt

The exposition of this theory is rather simple, just from three very
basic themes that are so inherent to sets one can prove all axioms
of ZF and prove the consistency of ZF also. However it is worth
noticing that this theory proves about well founded elements
in it matters that ZF doesn't prove about its sets, for example
the set of all sets hereditarily subnumerous to an element
is an element here, where that is not obvious in ZF.

Best Regards

Zuhair Al-Johar