[FOM] Impredicative Set Theory.

[Zuhair Abdul Ghafoor Al-Johar]

Is there an obvious inconsistency with the following theory?

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