[FOM] Re 196:Quantifier complexity in set theory

[Kurt Maes]

I think I have found and proven a 5-quantifier expression in "epsilon,="- 
notation that is equivalent to the axiom of choice in ZF-set-theory.
Currently my proof is still somewhat in a draft form, and I only have it 
.sxw-format ("open-office writer"-document).

The theorem in this document proofs the equivalence of the following 5 
sentences:
1) If x is a set of non-empty sets which are pairwise-disjoint, than x has 
a choice-set (I.e. the intersection of y with any non-empty element of x is 
a singleton.)
2) Same as one, but we do not demand the elements of x to be non-empty.
3) Same as two, but instead of stating the existence of a choice-set, we 
sate the existence of a choice-set which is not an element of x itself.
4) for every set x at least one of the following two conditions holds:
   a) there exists an element of x which does not contain any element not 
already contained in another element of x.
   b) x has a choice-set which is not an element of x itself.
5) forall x exists y forall z exists a forall u [y in x and A(x,y,z,a)] or 
[y not in x and B(x,y,z,a,u)].
   Here A(x,y,z,a) stands for z in y implies (a in x and a not equal y and 
z in a)
   and B(x,y,z,a,u) stands for z in x implies (u in z implies a in z and a 
in y) and (a in z and a in y implies (u in z and u in y implies u=a))

The equivalence of the first four sentences uses ZF.
The equivalence of 4(when rewriten in "epsilon,="-notation) and 5 uses only 
logic and nothing of ZF.
Since 1 is known form of the axiom of choice in ZF, 5 is a 5-quantifier 
"epsilon,="-expression that is ZF-equivalent with the axiom of choice.

PS.:
I'm currently looking for a Ph.d-stundent position and I have no experience 
in publishing work of my own. So, if anyone thinks this result is worth 
pubishing and willing to assist me in this, please contact me.
If anyone wants a copy of this theorem for proof-reading, please contact 
me. We can then see to a formatconversion of the document.