How do we know we need the axiom of choice for some theorem?

Question

I have been working through Munkres Topology book and in an exercise he says that there was a theorem he proved in a previous section that relied on the axiom of choice and the task is to find it. I am fairly certain I found it (and judging by the the research for this question I did find a theorem that requires choice) and the theorem is:

$\bf{Theorem \; 1}:$ A countable union of countable sets is countable.

Anyways, I have been using the theorem quite a bit in exercises and I have been thinking about the theorem and the proof and deciding whether or not some variant of the theorem needs choice. I realized though that I don't know that choice is needed, I just know that the proof I know of is a proof that uses choice. This leads to my question(s):

How can we tell a theorem needs the axiom of choice (or some weaker version of choice) to be proven?

I suspect that there might be no good specific answer that would apply to all theorems that seem to need choice, so is there some general strategy that would work for theorems like $\bf{Theorem \; 1}$ or similar things that could pop up in Munkres?

It is worth pointing out that here that Arturo Magidin mentions that without choice it has been shown that it is consistent with ZF that $\bf{Theorem \; 1}$ is false. In my mind, I am thinking that a strategy would be to show that without choice the theorem doesn't need to be true. If that strategy is particularly effective is there some "canonical" (I can't quite think of a better word for what I am talking about) way to do this?

With my little experience with AC I guess a good heuristic would be if the theorem deals with infinite amount of arbitrary sets then AC would be needed, but I am sure that there are some theorems that look like AC would be needed, and is the obvious way to go about proving them, but there is actually some clever way around it. I guess this is where my questions are coming from.

Also, I am interested in learning more on similar things so references, books or articles, would be appreciated. Would Set Theory by Kunen be a good book for learning to answer questions like this?

Answer 1

How do we know that we need the axiom of choice for proving a particular theorem?

Well, the first thing we should do is to analyze the proof of the theorem and see if at some point we make an infinite number of arbitrary choices. This means that the axiom of choice was used. It might be possible to use some structural properties of our objects (e.g. order, countability, etc.) to avoid using it, in which case we can prove the theorem without the axiom of choice.

But in order to prove that a certain theorem cannot be proved without some form of the axiom of choice we can do one of two things:

1. We can construct a model of set theory in which the axiom of choice fails and the theorem also fails. For example, we can construct a universe of set theory in which there exists a certain countable collection of countable sets, whose union is not countable.

   If we want to show that the theorem is weaker than the axiom of choice then we also have to show that there is a model in which the theorem holds, but the axiom of choice still fails.

2. We can show that if we assume that the theorem holds, then we can prove another statement $\varphi$ that was already shown to be independent from $\sf ZF$. For example, if we assume the Hahn-Banach theorem then we can prove the Banach-Tarski paradox, and therefore the existence of non-measurable sets. Since we know that it is consistent that there are no non-measurable sets without the axiom of choice, this means that the Hahn-Banach theorem cannot be proved without using some axiom of choice.

   Of course, it is possible use this method in order to show that a certain theorem is equivalent to the axiom of choice. We know quite a few equivalents, and if we can prove that a theorem implies one of them, then it implies the axiom of choice (and so it is equivalent to it, or even stronger).

To your last question, in order to learn about ways of proving independence from the axiom of choice one has to learn quite a bit of set theory, then learn about forcing and symmetric extensions. There are also other methods, such as Krivine's work using proof theoretical tools for these constructions; topos and sheaves based constructions which are similar (and in some way extend) forcing; and there are permutation models of $\sf ZFA$, which is the usual axioms of set theory, but we also allow non-sets objects to exist. Historically permutation models are the first method of independence we had, and symmetric extensions are somewhat based on the same idea of permutations.

Kunen could be a reasonable book, I suppose. There are also Jech's book, and depending on your set theoretical background there could be other (perhaps better) books to work with as well.