The following paper by Kurt Maes is focused on a version of the question at hand here, namely, finding an equivalent formulation of AC in the language of set theory using the fewest number of quantifiers, rather than merely the shortest length. In his main result, Maes finds a 5-quantifier assertion equivalent
to the axiom of choice. The statement is built on the same
statement as in François's answer, but modified to use fewer quantifiers (Maes has five, in comparison with ten for François; but of course François wasn't trying to minimize that quantity).
Maes's result refuted a conjecture of Harvey
Friedman, which in the introduction the author mentions was stated on F.O.M., that it
would not be possible to state a formulation of the axiom of
choice using only five quantifiers.
Please see Maes's solution in his paper.
When I first heard about the Maes result (August 2004, apparently
an earlier draft of his paper—I haven't checked the
differences), I naturally set myself the task of proving the main result
myself, without looking at Maes's argument. I would encourage the same of all of you---before reading further, try to express AC in the language of set theory using only five quantifiers! Here is what I had come up with (retrieved after digging around in my old computer files):
Theorem. AC is equivalent (in ZF) to the following assertion:
$$\forall A\exists B\forall a\in A\, \exists x\forall z$$
$$(x \in a \cap B) \wedge (z \in a \cap B \implies z=x) \wedge (a
\neq B)$$ $$\text{or }\quad(B \in x) \wedge (x \in A) \wedge (a
\neq x)$$ $$\text{or }\quad(B \in A) \wedge (z \notin B).$$
Proof. The point is that in order to get down to only five quantifiers, you have to essentially reuse the quantifiers to cover the various cases. The idea is that clause 1 expresses that $B$ is a selection
set
for $A$, when $A$ is a family of disjoint nonempty sets (plus something extra useful when $A$ is not like that). Clause 2
expresses that $A$ has elements that are not disjoint (at least two
contain $B$). Clause 3 expresses that $A$ contains the emptyset
($B=\emptyset$).
AC easily implies the assertion. If $A$ is a family of disjoint nonempty
sets, then we can let $B$ be a selection set for $A$, and verify clause 1. (note: in order to get $(a \neq B)$ in the case that $A$ is a singleton, we can freely add irrelevant elements to $B$ outside of $\bigcup A$.) If $A$ contains non-disjoint sets, we let $B$ be any element which is
in at least two elements of $A$, and then we can always be in clause 2,
since for any element of $A$ we can find another element of $A$ containing
$B$. Finally, if $A$ contains the empty set, we can set $B=\emptyset$, and
verify always clause 3.
Conversely, suppose that the stated principle holds. To prove AC, it
suffices to construct a selection set for a family $A$ of disjoint
non-empty sets. By replacing $A$ if necessary with the isomorphic copy
$\{\{w\}\times a\mid a \in A\}$, where $w$ has high rank (such as $w=A$ itself), we
may assume that every element of $\bigcup A$ has the same rank. Thus, every element of $A$ has rank one higher
than this, and every element of $\bigcup\bigcup A$ has rank lower than
this. It follows that no element of $\bigcup A$ is in $A$, and no element
of $\bigcup A$ has itself elements in $\bigcup A$.
For such an $A$, we get $B$ by the stated principle. Note now that Clause
2 implies $B \in\bigcup A$, and clause 3 implies $B \in A$. Meanwhile,
clause 1 implies both that $B$ has an element in $\bigcup A$ and also that
$B$ is not in $A$ (since it implies that $B\cap a$ is nonempty for
some other $a\in A$, while sets in $A$ are disjoint). By our assumptions
on $A$, these possibilities are mutually exclusive.
It follows that $B$ must always be in clause 1, or always in clause 2,
or always in clause 3, regardless of $a$, $x$, and $z$. If clause 3 always
occurs, then $\emptyset\in A$, a contradiction. If clause 2 always
occurs, then $B$ must be in more than one element of $A$, since otherwise
we could let $a$ be that element, and this would contradict the
disjointness of the elements of $A$. Thus, it must be that clause 1
always occurs. In this case, $B$ is a selection set, and so we have
established AC. QED
Although I am not aware of any utility flowing from the fact that AC can be expressed in this manner, it is nevertheless true that proof theory has sometimes made advances by investigating the resource-limited expressive powers of languages.
