[FOM] Re 196:Quantifier complexity in set theory
maes.kurt at pandora.be
Mon Nov 10 10:23:36 EST 2003
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
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
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.
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.
More information about the FOM