Sometimes — especially when dealing with classes that may not be models of some basic axioms, such as the separation axioms — one needs to cloister himself in the original language $L$ of set theory, that is the language generated by $\in$. If you have to relativise a form of AC in one of these classes, it is convenient to have it as short as possible.
We can define the length of a formula as the number of nodes in its tree structure. Abbreviations such as $∀x∈y\ F$ need to be expanded, while $\leftrightarrow$ can be used.
So far, the shortest form of AC (which ZF proves to be equivalent to AC) I've come across is a translation of $$\forall u \bigl(\varnothing ∉ u \land ∀x,y∈ u (x≠y \rightarrow x \cap y = \varnothing) \rightarrow ∃w∀x∈u∃y(x\cap w = \{y\})\bigr) $$ into $L$. I replaced
- $\varnothing ∈ u$ with $∀x(x∈u \rightarrow ∃y(y∈x))$ (11 nodes)
- $x≠y \rightarrow x \cap y = \varnothing$ with $∃z(z∈x\land z∈y) \rightarrow x=y$ (13 nodes)
- $x\cap w = \{y\}$ with $∀z(z∈x \land z∈w \leftrightarrow z=y)$ (13 nodes)
Summing all up, you get a total of 71 64 nodes. My question is, is there any known equivalent (in ZF) form of AC which is shorter than the one above (once translated into $L$)?
[Boring] bonus questions: what are the formulas in $L$ with the lowest number of nodes, which ZF proves to be equivalent to the Axiom of Choice? What if we drop some axioms from ZF?