Prove that the axiom of choice is necessary in order to prove something else.

Question

My mathematical background is perhaps a little lacking on this topic, but I've been searching and haven't come up with a satisfactory answer to this question. I have no idea how to approach the problem or if it has been answered.

I have seen numerous cases where it is asserted that "the axiom of choice is necessary" to complete a particular proof but I've yet to see a case where the necessity of the axiom of choice is actually itself proven.

For example consider the following question: Additive function $:\mathbb{R} \rightarrow \mathbb{R}$ that is not linear.

The answers and comments note that you can't construct such a function without the axiom of choice. Then it seems like this would imply, for example, that any function with a closed form which is additive is necessarily linear. Is this correct? How would one go about proving the necessity of the axiom of choice?

I apologize in advance that I don't have my own attempt to share since I'm not even sure how to approach such a proof.

Answer 1

Let's take the axioms of a group. We have a binary operator, $*$, and the axioms state that there is a neutral element, $e$, and that $*$ is associative, and for every $x$ there is $y$ such that $x*y=e$.

Question. Is it true that for every $x,y$ it holds that $x*y=y*x$?

Well, there are infinitely many proofs from these finitely many axioms. So how can we tell? Checking them one by one is futile.

The answer is that if this was provable, then every model of the axioms would also satisfy the above property. In other words, every group would be commutative. So if we can find a group which is not commutative, then we effectively proved that the axioms of a group are not sufficient for proving that for every $x$ and $y$, $x*y=y*x$.

And indeed, it is not hard to find non-commutative groups.

So, going back to $\sf ZF$ and $\Bbb Q$-linear operators on $\Bbb R$. How would you prove that $\sf ZF$ is not sufficient for proving the existence of such discontinuous operators? Well, you'd show that there are models of $\sf ZF$ in which there are no such operators.

Now we know that any $\Bbb Q$-linear operator which is also Baire measurable is continuous (one can also use Lebesgue measurability, for example). So if we can find a model of $\sf ZF$ in which every such linear function is Baire measurable, then every such function is also continuous.

And indeed, this was shown possible by Solovay, and later improved upon by Shelah. In other words, they exhibited models of $\sf ZF$ in which every function $f\colon\Bbb{R\to R}$ is Baire measurable, and in particular any $\Bbb Q$-linear operator. So every such operator is continuous.

These constructions are extremely technical utilising not only the technique of forcing, but also extended techniques of symmetric extensions, and often relying on theorems in analysis as well. But with time, one can learn them.

---

TL;DR: To prove that some axioms don't prove a statement, it is usually easier to prove that there is a model of the axioms where the statement is false. This is true for $\sf ZF$ as well.

To show that the axiom of choice is necessary for proving something we need to show that:

1. $\sf ZFC$ implies this something, and
2. there is a model of $\sf ZF$ where this something is false.

The difficult part—conceptually—is getting your head around models of $\sf ZF$, because it's the foundation of mathematics. But once you've gone through that step, the rest is just a technicality.

Answer 2

In order to show that proving $X$ requires the Axiom of Choice, it suffices to prove the Axiom of Choice from $X$ (and the remaining axioms). Well, not only that. In addition, you need to know that it has been shown that the $\mathsf{AC}$ to be independent of the other axioms (i.e., we can add either $\mathsf{AC}$ or $\neg \mathsf{AC}$ to them without one case being inconsistent (or more inconsistent than the other)

Actually, sometimes you can only show a weaker form of choice (Countable Choice, Dependent Choice, ...) from $X$ and vice versa only need that weaker form to show $X$. So one has to be careful. The impossibility of a constructive proof of $X$ need not mean that we need full-blown Choice. This is also the case here. After all, we only deal with small sets - such as $\Bbb R$ or perhaps the powerset of $\Bbb R$ or at most a handful of powersets further up, whereas the Axiom of Choice deals with arbitrarily large sets. Inded, we use "Every vector space has a basis" to arrive at our non-linear additive function, and that statement is indeed equivalent to $\mathsf{AC}$ - but to repeat: we use this only for a specific small-ish case.

I won't however go into details and try to fully expand how much choice we can get "back" from a nonlinear additive functoin.

Answer 3

Hagen von Eitzen's answer is correct, but it doesn't tell the whole story. In particular, even assuming that you can prove $\mathsf{AC}$ from $(*)$ together with the $\mathsf{ZF}$ axioms, this only tells you that $\mathsf{AC}$ is necessary for proving $(*)$ if you already know that $\mathsf{AC}$ itself can't be proved in $\mathsf{ZF}$. At some point in the story we have to have a general framework for establishing unprovability results: how do we show that a theory $T$ does not prove a sentence $\varphi$?

There are two ways one might approach this. The most obvious is to hope for a very detailed combinatorial analysis of all $T$-proofs, as purely syntactic objects, which would let us prove (e.g. by some sort of induction on complexity) that there is no $T$-proof of $\varphi$. This was basically Hilbert's goal with proof theory. As it turned out, it's not too successful - it can sometimes be done (e.g. in ordinal analysis, it's how we establish that the consistency of a theory follows from a certain transfinite induction principle which lets us "simplify" proofs to the point that we can actually rule out any possible proof of $0=1$ - but in general is rarely feasible. In particular, we're nowhere near a proof-theoretic argument that $\mathsf{AC}$ cannot be proved in $\mathsf{ZF}$.

The more flexible approach - which actually occurred much earlier, in the context of non-Euclidean geometries - is by exhibiting a model. Briefly, a theory which has a model has to be consistent (when made formal, this is the soundness theorem), and so if we can whip up a model of $T\cup\{\neg\varphi\}$ (that is, a model of $T$ in which $\varphi$ is false) we know that $T$ can't prove $\varphi$ since if it did $T\cup\{\neg\varphi\}$ would be inconsistent.

This model-theoretic approach is how we establish independence results over $\mathsf{ZF}$ or similar, most commonly$^1$ via forcing (perhaps plus additional bells and whistles - e.g. to show the unprovability of $\mathsf{AC}$ over $\mathsf{ZF}$, we need to also use the notion of symmetric submodels). However, models of $\mathsf{ZF}$ are necessarily extremely complicated objects, in contrast with for example models of Euclid's axioms with the parallel postulate replaced by its negation. Consequently forcing is an extremely complicated technique, and it has no simple description; for this reason results of this type are generally just stated without justification when not presupposing advanced set theory. (That said, see here.)

So unfortunately I kind of have to punt: the best I can do is mention the missing ingredient without telling you much about it. For what it's worth, though, forcing is an incredibly beautiful technique, and well worth the rather large amount of time required to master.

---

$^1$Of course, forcing and its elaborations are not the only techniques around. Indeed the $\mathsf{ZF}$-unprovability of $\neg\mathsf{AC}$ - or if you prefer, the consistency of $\mathsf{AC}$ with $\mathsf{ZF}$ - was proved a decade before the unprovability of $\mathsf{AC}$, by a simpler but more limited method: inner models.

It's also worth mentioning that all of these unprovability results are really relative unprovability results - e.g. what we really prove is "If $\mathsf{ZF}$ is consistent, then $\mathsf{ZF}$ doesn't prove $\mathsf{AC}$" and so forth. Since the theories at this level are so powerful, it's important to take seriously the possibility of inconsistency, although we often ignore it in practice.

Answer 4

Besides the other existing answers, I just want to add that we never in practice need the full axiom of choice. Rather, we typically need just a well-ordering of some relevant objects. For example, we can prove without using AC that every vector space whose vectors can be well-ordered has a basis. Applying that here, we only need a well-ordering of the reals in order to obtain without using AC an additive non-linear function on the reals. What does that mean? Well, to deny the existence of such a function implies denying the existence of a well-ordering of the reals. So if you want to prove that AC is necessary to prove the existence of such a function, you must at least be able to construct a model of ZF in which the reals cannot be well-ordered, under the assumption that ZF is consistent. That should give an idea of why it is unsurprisingly hard in the first place. (It is harder to construct a model of ZF where the reals cannot be well-ordered, than one where the reals are well-ordered.)

Similarly, we have (without AC):

• Every partial-order on a well-orderable set in which every chain has an upper bound has a maximal element. (The proof can be easily adapted from here by using the well-ordering to map each chain to a unique strict upper bound.)
• Every well-orderable field has an algebraic closure. (This applies to all countable fields, and curiously we do not need AC to that prove the complex numbers are algebraically closed.)

So it is sometimes interesting to note that although many theorems do rely on AC in full generality, when they are applied to specific sets it comes down to merely depending on a well-ordering of one specific set, far from full AC.