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.

  • 7
    $\begingroup$ Two definitions of global continuity are equivalent for real functions. See the answers on Mathematics: Continuity and the Axiom of Choice. This result is in the chapter named "Unnecessary Choice" in Herrlich's book - maybe some other results from that chapter might be interesting, too. It is mentioned in one of the answer here: Unnecessary uses of the axiom of choice. $\endgroup$ Jan 20 at 9:20
  • 3
    $\begingroup$ This similar question has a lot of answers that would apply here. $\endgroup$ Jan 20 at 18:58
  • 3
    $\begingroup$ @Steinberg Some answers in this other question are relevant but the answers given below to my question are also quite on topic. I am interested in examples of use of AC that simplify the proof. Useless does not necessarily means simpler. $\endgroup$
    – coudy
    Jan 21 at 17:13

8 Answers 8


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\}$.


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.

enter image description here

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.

  • 8
    $\begingroup$ One thing I quite like about this example is that the AC-proof is actually much harder, when fully unwound, than the AC-free proof: it relies on trichotomy of well-orderings, whereas the AC-free proof really is ust a quick stitching of maps and sets. It's only if we treat some basic well-ordering theory as a blackbox that the AC-proof is immediate. $\endgroup$ Jan 20 at 18:02
  • 1
    $\begingroup$ But trichotomy of ordinals is easy---you just define the isomorphism by recursion, and one side will run out first or they are isomorphic. Isn't that much simpler than the back-and-forth of CSB? $\endgroup$ Jan 20 at 18:04
  • 4
    $\begingroup$ I don't personally think so. The choice-free proof of CSB I have in mind (the "three types of $f\circ g$-block" argument) at least doesn't need transfinite recursion at all, while trichotomy of well-orderings does. $\endgroup$ Jan 20 at 18:05
  • 1
    $\begingroup$ I see, interesting. I think of the three-blocks etc proof (as in my figure) as fussy and detailed and complicated, whereas trichotomy is conceptually simple---just match them up until one runs out. $\endgroup$ Jan 20 at 18:26
  • 3
    $\begingroup$ Fair, I give higher weight to the complexity of trichotomy. Even granting that point, though, in the AC-proof we still need to get from AC itself to the well-ordering principle - which again isn't trivial. $\endgroup$ Jan 20 at 18:40

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:

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

  • $\begingroup$ Nice. I think I saw a similar problem in a book of Halmos, Problems for Mathematicians, Young and Old. $\endgroup$
    – coudy
    Jan 20 at 17:20
  • 2
    $\begingroup$ Just to clarify, speaking constructively, the complement of $\mathbb{R}^3$ and the union of the circles is empty – no point has been forgotten. The stronger statement, namely that the union equals $\mathbb{R}^3$ would constructively mean that there is a map that assigns to each point the circle it belongs to – and since that map is not continuous, we cannot show its existence constructively. $\endgroup$ Jan 22 at 8:36
  • $\begingroup$ Thanks, Andrej, that is helpful. (I guess you mean the complement in $\mathbb{R}^3$ of the union of the circles?) $\endgroup$ Jan 22 at 14:03

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.


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:




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.


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.

  • 3
    $\begingroup$ One could add though that for such applications, the spaces being separable, one can get away with DC instead of AC. $\endgroup$ Jan 20 at 15:11

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.


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


Not the answer you're looking for? Browse other questions tagged or ask your own question.