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

Solution 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.

Solution 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.