[FOM] Impredicative Set Theory.

Zuhair Abdul Ghafoor Al-Johar zaljohar at yahoo.com
Mon Dec 5 01:55:40 EST 2011

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.


More information about the FOM mailing list