Examples of theorems that haven't been proven without AC in practice but can be proven without it in principle

Question

It is possible to prove theorems of the form "if $\phi$ is provable in ZFC, then $\phi$ is provable in ZF". For example, let $\phi$ be a statement that is absolute between $V$ and $L$. If $\phi$ were not provable in ZF, then there would be a model $M$ in which it is false, which in turn implies that it is false in $L^M$, hence not provable in ZFC.

I was wondering whether there are natural such statements all known proofs of which involve axiom of choice (or whose proofs become substantially easier when AC is used).

Following Andres Caicedo's answer and comments here, it is possible to "cheat" and turn ZFC proofs into ZF proofs by carrying out the argument in L and then using absoluteness. What I had in mind was to see if there are examples where AC "takes care" of a procedure which in theory we could do without it.

Answer 1

Here is some general theorem that you can prove.$\newcommand{\Ord}{\mathsf{Ord}}$

We write $(\exists^{\Ord}x)\varphi$ and $(\forall^{\Ord}x)\varphi$ to mean that we are bounding the quantifier on $x$ as a set of tuples of ordinals. Meaning $x\subseteq\Ord^{<\omega}$, and $\varphi$ holds. (You can observe that this doesn't increase the complexity of the formula in the Levy hierarchy more than a usual quantifier would.)

If $\varphi(x)$ is a statement which is upwards absolute, then $(\forall^\Ord x)\varphi(x)$ is provable with the axiom of choice if and only if it is provable without the axiom of choice. The proof is almost trivial, given $x\subseteq \Ord^{<\omega}$, we can consider $L[x]$ as a model of choice, $\varphi(x)$ holds there, and it is upwards absolute, so it holds in $V$. $\qquad\square$

This gives an immediate plethora of examples in the sense of finite coloring theorems and properties, e.g. "every coloring of a subset of $[\kappa]^{<\omega}$ in $\lambda$ colors, has a subset of order type/cardinality $\alpha$ which is homogeneous/anti-homogeneous" are all statements of the form $\Pi_2$ whose universal quantifiers can be replaced by $\forall^\Ord$.

---

You can also take a look in Herrlich's book The Axiom of Choice which includes many examples of less set-theoretical nature.

Answer 2

If I understand the question, one example of a theorem that becomes substantially easier when the axiom of choice is used is Hindman's theorem.

This is a theorem of infinitary combinatorics:

Hindman's Theorem. If $k \in \mathbb{N}$ and $g\colon \mathbb{N} \to \{1, \ldots, k\}$, there is an infinite set $I \subseteq \mathbb{N}$ and a $c \leq k$ such that for all nonempty finite $F \subseteq I$, $g(\sum_{i \in F} i) = c$. In words, for every finite coloring of $\mathbb{N}$ there is an infinite set $I$ and a color $c$ such that the sum of any positive finite number of distinct elements of $I$ receives color $c$.

There are (essentially) three known proof methods for the theorem. One method uses a special kind of ultrafilter on $\mathbb{N}$, which is constructed by an application of Zorn's lemma. There is an exposition of this proof by Leo Goldmakher here; the construction is theorem 3.1. This method gives the "easiest" proof of the theorem.

The second method, due to Furstenberg and Weiss, uses methods of topological dynamics and ergodic theory. This proof also uses high powered techniques, although it does not directly use ultrafilters.

The third method is based on Hindman's original proof, which is much more difficult but which uses much more elementary methods. Hindman's original proof can be formalized in second-order arithmetic (as shown by Blass, Hirst, and Simpson 1987), so it does not have any essential uses of the axiom of choice. Simplified expositions of this method are given by Baumgartner (1974) and Towsner (2011), online here.