Simpler proofs using the axiom of choice

Question

I am looking for examples of results which may be proven without resorting to the axiom of choice/Zorn lemma/transfinite induction but whose proof is quite simplified by the use of the axiom.

For example, in the Poincare-Bendixson theory, it is shown that any closed orbit of a planar vector field contains a fixed point. This is done first by showing that any closed orbit contains a closed orbit. Then it is straightforward to conclude using Zorn's lemma. The conclusion can be reached without resorting to Zorn's lemma, for example by looking at the area bound by a closed orbit. But this is not so straightforward. One has to give a meaning to such area and then show amongst other things that this area depends continuously on the orbit.

Answer 1

In Division by Three, Peter G. Doyle and John Horton Conway show, without invoking the Axiom of Choice, that for any sets $A$ and $B$, if there is a bijection between $3 \times A$ and $3 \times B$, then there is a bijection between $A$ and $B$, where $3$ is a set with 3 elements, say $\{0,1,2\}$.

Answer 2

Another classic example is the Schröder-Cantor-Bernstein theorem.

Theorem. If a set $A$ injects into $B$ and $B$ injects into $A$ then there is a bijection.

If AC holds, then this is nearly trivial, since if $A$ and $B$ are well orderable, then the minimal ordinals would have to be the same, giving a bijection.

But there is a more constructive proof (one not using AC), stitching together pieces of the injections as illustrated in the following figure.

Historically, the distinction between the proofs is important, and actually the history of the theorem and who proved what when is quite complicated. See the Wikipedia entry.

Answer 3

Here is a nice example.

Theorem. Space $\newcommand\R{\mathbb{R}}\R^3$ is the disjoint union of circles.

The AC proof is simply to enumerate all points in $\R^3$ in a well-ordered sequence in length continuum, and then attach a circle to each point along the way. If at stage $\alpha$ the $\alpha$th point is not yet occuring on a circle, then since we have chosen already only fewer than continuum many circles, there must be a plane through the point that is not coplanar with any of them. And since each circle already chosen intersects that plane in at most two points, there are fewer than continuum many forbidden points on the plane. And so we can find a circle through that point in that plane that avoids them.

Meanwhile, there is a constructive proof given as theorem 1.1 of

• M. Jonsson and J. Wästlund: Partition of R3 into curves, Mathematica Scandinavica 83 (1998) 192-204; JSTOR, author's website.

One places circles of radius 1 centered at (4k+1,0,0), and then considers spheres centered at the origin, which intersects that family always in exactly 2 points, and such a 2-punctured sphere can be partitioned by circles. (Note: the proof is constructive in the sense that it does not use AC, but it is not constructive in the sense of intuitionistic logic.)

Of course it is nice to have the specific construction, but to my way of thinking, the AC proof is far more flexible, and one can use to to construct many other kinds of partitions (into unit circles, shapes of other kinds etc etc), whereas specific constructions for many of these other instances remain as open questions.

Here is another similar instance:

Theorem. Space can be partitioned by skew lines.

The AC proof proceeds like the transfinite recursion above. Just add the next point on a line avoiding the previous lines and pointing in a totally different direction.

But there is a constructive proof also. Take one vertical line, and then a nested arrangement of hyperboloids, with gradually changing angles. Each of them is a union of straight lines, and these are all skew.

See these related MO questions:

• Covering space by disjoint unit circles
• Is it possible to partition $\R^3$ by disjoint unit circles?
• Foliating space by skew lines
• Concerning proofs from the axiom of choice that ℝ³ admits surprising geometrical decompositions: Can we prove there is no Borel decomposition?

The latter question can be seen as asking which of these AC arguments genuinely require something fundamentally nonconstructive.

Answer 4

There is an interesting class of problems that are provable in $ZF$ by "coincidence" in the sense that either (a fragment of) $AC$ holds and then it is provable from the proof in $ZFC$, or there specific instance of the failure of $AC$ implies the result.

The simplest example for such problem is: countable product of spaces with $2$ elements is compact.

If the product of our spaces is non-empty, we have fragment big enough of $AC$ to prove that the product is compact by following the proof in $ZFC$, otherwise the product is empty, but the empty space is compact, so we are done.

A more complicated example is: let $X$ be subspace of $ℝ$, then $X$ is compact if and only if $X$ is sequentially compact and Lindelöf.

If $CC(ℝ)$ holds then the usual proof works, on the other hand $¬CC(ℝ)$ is equivalent to "subspace of $ℝ$ is Lindelöf if and only if it is compact", so because $X⊆ℝ$ is Lindelöf, it is compact.

The result of $¬CC(ℝ)$ being equivalent to "Lindelöf ⇔ Compact" for subspaces of $ℝ$ don't, as far as I know, have a simple proof.

Herrlich, Horst, Products of Lindelöf (T_2)-spaces are Lindelöf – in some models of ZF., Commentat. Math. Univ. Carol. 43, No. 2, 319-333 (2002). ZBL1072.03029.

Answer 5

Many examples from set theory are known, but here is a very basic (third-order) theorem from most ordinary mathematics:

"A regulated$f:[0,1]\rightarrow \mathbb{R}$ is bounded", (&)

where 'regulated' means that the left and right limits $f(x-)$ and $f(x+) $ exist everywhere.

To prove (&) using (countable) Axiom of Choice and (basic) sequential compactness, suppose there is a regulated $f:[0,1]\rightarrow \mathbb{R}$ that is not bounded. Find a sequence $(x_n)_{n\in \mathbb{N}}$ in $[0,1]$ such that $f(x_n)>n$ for all natural numbers $n$. This sequence has a convergent sub-sequence, say with limit $y\in [0,1]$. Then either $f(y-)$ or $f(y+)$ does not exist, and we are done. This proof only uses countable choice for quantifier-free formulas (called QF-AC$^{0,1}$ by Kohlenbach) and arithmetical comprehension.

One can also prove (&) without using the Axiom of Choice, namely in Z$_2^\Omega\equiv$ RCA$_0^\omega+(\exists^3)$; here, RCA$_0^\omega$ is Kohlenbach's base theory from higher-order reverse mathematics and $(\exists^3)$ is Kleene's quantifier. The system Z$_2^\Omega$ is a conservative extension of Z$_2$ and a fragement of ZF. Intuitively, one cannot prove (&) in fragments of Z$_2^\Omega$. The proof of (&) in Z$_2^\Omega$ is fairly indirect and involved, via a supremum principle and the Heine-Borel theorem for uncountable coverings.

In conclusion, the Axiom of Choice makes (&) much easier to prove in a much weaker system.

Finally, the aforementioned negative results (and many more examples) can be found in:

https://arxiv.org/abs/1808.09783

https://arxiv.org/abs/1910.02489

https://arxiv.org/abs/2212.00489

A Platonist will appreciate the observation that a well-known phenomenon (AC simplifies proofs, even when not needed) from the foundations of mathematics is reflected in ordinary mathematics. Comparisons with Plato's cave are allowed.

Answer 6

Axiom of choice is frequently used in Analysis through the Hahn-Banach theorem. An example is the existence of solution of Dirichlet's problem (=balayage problem). This can be proved without an appeal to the axiom of choice, but using Hahn-Banach gives a few lines proof, see for example

N. Landkof, Foundations of modern potential theory, Chap. IV, section 1.

Answer 7

The following theorem, relating path-connectedness and arc-connectedness (arc := injective path):

"Every path-connected Hausdorff space is arc-connected"

can be proven both with the axiom of choice or without it. The proof given in [1] uses AC, with the specific goal in mind to avoid complexity induced by the avoidance of AC. Some proofs avoiding AC are referenced in the introduction, for comparison.

[1]: https://www.wcupa.edu/sciences-mathematics/mathematics/jBrazas/documents/Constructing_arcs_from_paths_9-9-21.pdf

Answer 8

For an orthomorphism $A$ in a (real or complex) Banach lattice $X$ the formula $\lvert A\rvert x=\lvert Ax\rvert$ for $x\ge0$ can be obtained relatively quickly if one uses the fact that $X$ is order isomorphic to a space of continuous functions (observing that $A$ corresponds to a multiplication operator in that space). However, the proof of the latter requires the maximal ideal theorem which cannot be shown in ZF or ZF+DC. In the lack of an order isomorphism, the only proof known to me makes use of (a real or complex form of) Freudenthal's spectral theorem.