From: zuhair on

This theory might look like Ackermanns' but yet it differ from
Ackermann in that it doesn't require the second completeness axiom for
V to work in.

Language: FOL with the following primitives:

Identity "="
Epsilon membership "e"
the primitive constant V.

Define: x is a set <-> x e V
Define: x subclass y <-> for all z ( z e x -> z e y )

Axioms:

Extensionality: for all z ( z e x <-> z e y ) ->x=y

Transitive: for all x,y ( x e y & y e V -> x e V )

Class comprehension: if phi is a formula in which at least y
is free, that do not use V, and in
which x is
not free, then all closures of:

Exist x for all y ( y e x <-> ( y e
V & phi ) )

are axioms

Define: x={y|phi} <-> for all y ( y e x <-> ( y e V & phi ) )

Define: y transitional of x <-> ( x subclass y & y is transitive )

Define: z=Tc(x) <-> ( z transitional of x &
for all y ( y transitional of x ->
z subclass y ) )

"Tc" stands for "Transitive Closure".


Set comprehension: if phi is a formula in which at least y or z are
are free, with parameters x1,...xn, that
do not
use V, and in which c is not free, then
all
closures of

x1 e V & ...& xn e V &
for all c,z ((c= {y|phi} & c subclass Tc
(z)) ->
~phi(z))
->
Exist a set c for all y ( y e c <-> phi )

are axioms.


Theory definition finished/

For the purposes of this theory, I shall define "nice set" in the
following manner:

x is a nice set <-> ( x e V & for all y ( y e Tc(x) -> ~ y e Tc(y) ) )

So there is no circular membership of nice sets.

Now if we restrict ourselves to nice sets then we can easily derive
theorems of pairing,union,power,infinity,separation and Replacement of
nice sets, thus rendering ZF minus Regularity interpreted as a sub-
theory of this theory.

There is no need for the axiom of second completeness for V of
Ackermanns' in this theory, which is

For all x,y ( x subclass y & y e V -> x e V )

This is axiomatized by Ackermann to prove power, but this is not
needed here when working with nice sets.

Zuhair