Impredicative Set Theory "Imp.ST" is the collection of all sentences
entailed from FOL with equality and membership by the following non
logical axioms:

I. Extensionality: (z)(z e x <-> z e y) ->x=y

II. Transitive Closure: (x)[y](x c y & transitive(y) &
(z)(x c z & transitive(z) -> y c z))

where c is subset relation; and
transitive(y):= (m)(m e y -> m c y).

Define: y=TC(x):= (z)(z e y <-> (t)(x c t & transitive(t)-> z e t))


III. Impredicative Comprehension: if phi is a formula in which x is not
free, then ([x](y)(y e x <-> phi & ~x e TC(y) & ~y=x)) is an axiom.

Define: x is a {y|phi}:= (y)(y e x <-> phi & ~x e TC(y) & ~y=x)


IV. Size axioms: if phi is a formula, then the following are axioms:

([y](phi) ->(x)(x is a {m|phi} ->[z](z e x)))

([y..](phi) ->(x)(x is a {m|phi} ->[z..](z e x)))


V. Acyclicity: (x)(y)(y e TC(x) -> ~y e TC(y))

/

Notation:[x] stands for "there exist x"
[x..] stands for "there exist many x"
:= stands for "is defined as"

When I defined this theory I thought it might be obviously
inconsistent especially with axiom V in play, but I'm not
seeing a clear inconsistency with it yet.

Zuhair Al-Johar
5/12/2011