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.

  • 6
    $\begingroup$ All these answers seem well thought out and interesting. I don't yet follow the details of each of these discussions so I don't really know which should be accepted. I'm going to try to parse them carefully over the next few days and hopefully come to some sort of conclusion. $\endgroup$
    – jodag
    Jul 26 '20 at 20:11
  • 1
    $\begingroup$ The existence of such a non-linear additive function does not in itself imply the Axiom of Choice in its full generality. So, strictly speaking, it is not true that you need the Axiom of Choice. What is true is that $ZF$, that is Zermelo-Fraenkel without the Axiom of Choice, is not sufficient to guarantee the existence of such a function. But $ZF$ together with some weaker version of $AC$ would also be sufficient. $\endgroup$
    – TonyK
    Jul 27 '20 at 14:45
  • $\begingroup$ I upvoted this question because I had already before thought of the idea of a function from R to R that distributes over addition but isn't linear. $\endgroup$
    – Timothy
    Jul 27 '20 at 17:20
  • $\begingroup$ Sometimes mathematicians will say the axiom of choice is necessary to prove a particular proposition when they mean that if that axiom is dropped entirely from one's theory of sets, then one cannot prove the proposition. But in some cases one can prove it with one of various weakened versions of the axiom of choice. (Right now I don't know which this is.) $\endgroup$ Jul 27 '20 at 20:15
  • $\begingroup$ @MichaelHardy: Dependent choice is enough for almost all measure theory except pathologies. Countable choice is enough for almost all real analysis including soft real analysis, such as equivalence of continuity and sequential continuity at a single point. $\endgroup$
    – user21820
    Jul 28 '20 at 8:07

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.

  • $\begingroup$ It's worth noting that this answer gives a way to know that a theorem needs some form of choice, whereas other answers (particularly, ones requiring the theorem to be equivalent to choice in ZF) give a way to know that a theorem needs the full axiom of choice. $\endgroup$
    – mudri
    Jul 28 '20 at 12:20

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.

  • 1
    $\begingroup$ Forcing can be developed entirely syntactically; you don't need to use models at all. As I recall, Cohen's original development was entirely syntactic. This syntactic approach (and a similar one for $\mathsf{V=L}$), avoiding the use of models, is how one would show, for instance, that $\mathsf{PA}$ proves the statements $\mathsf{Con}(\mathsf{ZF})\implies \mathsf{Con}(\mathsf{ZF}+\mathsf{AC})$ and $\mathsf{Con}(\mathsf{ZF})\implies \mathsf{Con}(\mathsf{ZF}+\neg\mathsf{AC}).$ $\endgroup$ Jul 26 '20 at 22:53
  • $\begingroup$ @MitchellSpector: Do you mean by your comment that you consider Cohen's proof of independence of AC over ZF to be a proof-theoretic one? $\endgroup$
    – user21820
    Jul 27 '20 at 13:35
  • 1
    $\begingroup$ @MitchellSpector: So is your answer to my question "yes"? I ask because Noah wrote "we're nowhere near a proof-theoretic argument that AC cannot be proved in ZF", and so I don't know whether both of you have differing notions of "proof-theoretic". $\endgroup$
    – user21820
    Jul 27 '20 at 18:05
  • 1
    $\begingroup$ @MitchellSpector: I'm not sure how ordinal analysis can be relevant here, because ZFC is equiconsistent with ZF and the p.t.o of ZF would be the same as that of ZFC. $\endgroup$
    – user21820
    Jul 27 '20 at 18:14
  • 1
    $\begingroup$ @user21820 I agree -- I only mentioned that because that's what proof theory often refers to, in my experience. $\endgroup$ Jul 27 '20 at 18:20

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.

  • 1
    $\begingroup$ Thank you, this is very interesting. The first paragraph makes sense to me but could you clarify something? So I accept that the additive non-linear proof uses every vector space has a basis and I'm willing to accept that its proven that this is equivalent to AC, but do we know that it was necessary to use the fact that every vector space has a basis in order to provide an example of a additive non-linear function? $\endgroup$
    – jodag
    Jul 25 '20 at 23:10
  • $\begingroup$ @jodag: I'm not sure what exactly you are asking in your comment, but as per my answer to construct an additive non-linear function on the reals you only need a Hamel basis, so of course you don't need every vector space to have a basis. $\endgroup$
    – user21820
    Jul 26 '20 at 11:10

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.

  • 3
    $\begingroup$ Isn't assuming Well-Ordering more or less assuming choice by the Well-Ordering theorem? Of course, given a well-ordered vector space we can prove that it has a basis but behind the scenes of 'every vector space has basis' we just use the equivalence of choice and well-ordering. I think the sentence we never in practice need the full axiom of choice is slightly misleading then, unless I'm missing something crucial. $\endgroup$
    – mrtaurho
    Jul 26 '20 at 11:33
  • 3
    $\begingroup$ @mrtaurho: The well-ordering theorem says "every set can be well-ordered". In practice we are dealing with some specific sets and so we do not need the full well-ordering theorem. In fact, all known real-world applications of mathematics do not require AC, because either they involve countable sets or they involve the real numbers for which we do not need AC to obtain an algebraic closure. $\endgroup$
    – user21820
    Jul 26 '20 at 11:38
  • 1
    $\begingroup$ Ah, I see where I was on the wrong track then. Thank you! $\endgroup$
    – mrtaurho
    Jul 26 '20 at 11:53
  • $\begingroup$ Isn't the full axiom of choice used to prove that the product of an arbitrary family of compact topological spaces is compact? $\endgroup$ Jul 28 '20 at 18:13
  • $\begingroup$ @MichaelHardy: I thought my last point in my post ("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") was clear enough. Just because you use AC in a proof does not mean you need it to hold for every set; AC can still fail for some obscure sets that are not relevant to what you need. All concrete applied mathematics that we know of so far can be derived from theorems provable without AC, for whatever reason. $\endgroup$
    – user21820
    Jul 28 '20 at 19:27

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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