Why is Axiom of Choice "a convenient and safe labour-saving device"?

Question

In Terence Tao's Analysis, he states

The axiom is almost universally accepted by mathematicians. One reason for this confidence is a theorem due to the great logician Kurt Godel, who showed that a result proven using the axiom of choice will never contradict a result proven without the axiom of choice. More precisely, Godel demonstrated that the axiom of choice is undecidable; it can neither be proved nor disproved from the other axioms of set theory, so long as those axioms are themselves consistent.

Then he writes

In practice, this means that any “real-life” application of analysis (more precisely, any application involving only “decidable” questions) which can be rigorously supported using the axiom of choice, can also be rigorously supported without the axiom of choice, though in many cases it would take a much more complicated and lengthier argument to do so if one were not allowed to use the axiom of choice. Thus one can view the axiom of choice as a convenient and safe labour-saving device in analysis.

In ZF, if a proposition is "decidable", and if we prove the proposition in ZFC, then it is true in ZF. I understand it. If we prove sth is true in ZFC, then it is undecidable or true in ZF. but I think the hardest part is to demonstrate a proposition is "decidable". How can we do that? Is there anyway to prove a proposition "decidable"? So I think the axiom of choice is not safe. I don't understand Tao's words. Also, I don't understand why he asserts "real-life" application is always "decidable".

Answer 1

When you want to prove that a particular and very hard to define sequence converges, it is sometimes easier to just prove "Every monotone sequence with an upper bound is convergent."

Of course, that means you need to verify that your sequence is monotone and bounded from above. But the general theorem is simpler.

When you move forward in analysis, you run into all sort of things that have general theories. Measure, Baire category, to name two main examples.

These theories are sensitive to the axiom of choice being present or removed. For example, it could be that the real numbers are a countable union of countable sets, which would destroy all theory of measure. Or it could be that all sets are Lebesgue measurable, or have the Baire property, which again changes the way these theories behave.

All these theories, when you try to apply them to stuff that "normally comes up", you find out that they can be proved by hand in the usual cases. It requires you, however, to fuss about $\varepsilon$s and $\delta$s, or work harder and produce actual computations of things, whereas the general theories just guarantee you certain things exist.

This is why sometimes it is just easier to work with choice, when you want to talk about the theoretical parts. This is what Tao means.

But the axiom of choice comes with a terrible price of giving you all sort of weird sets, like Vitali sets, Bernstein sets, and so on. So some people would argue that this is a reason to reject choice. That it is inconsistent, or at least incompatible with our intuition. Gödel proved, however, that if the rest of $\sf ZF$ is consistent, then $\sf ZFC$ is also consistent. So adding the axiom of choice will not cause real contradictions, only odd paradoxes.

This means that accepted or rejecting the axiom of choice is not about consequences in reality, but about simplifying proofs.

---

Let me just point out that Gödel only proved that the axiom of choice cannot be disproved from $\sf ZF$. It was Cohen who later showed that it cannot be proved either.

Answer 2

There is Shoenfield's absoluteness theorem, which could be what Terence Tao is referring to. At a simpler level, observe the following:

As usual, we use the standard interpretation of arithmetical sentences in ZF (as sentences about $ω$). Then for every axiom $A$ of ZFC, we have that ZF proves that the constructible universe $L$ satisfies $A$. Now take any arithmetical sentence $Q$ such that ZFC proves $Q$. Then ZF proves that $L$ satisfies $Q$, and hence also that $Q$ is true (because $ω$ is the same in $L$). We can hence observe (in a suitable metasystem MS) that any proof of any arithmetical sentence $Q$ within ZFC can be transformed into a proof of $Q$ within ZF. This weaker absoluteness theorem can be summed up as:

If you can prove some arithmetical sentence within ZFC, you can prove it within ZF alone.

This already implies that any theorem of ZFC about just the natural numbers does not depend on the axiom of choice. This could also be what he means by "decidable" (and anyway he did put it in scare-quotes). We can state a precise version: For any sentence whose truth value can be decided by a program that uses some finite Turing jump, if it can be proven within ZFC then it can be proven within ZF.