#though it is really interesting how countable choice is sufficient to prove most of the non-constructive results in analysis

[bubbloquacious]

thoughts on the axiom of choice

sub question: countable choice or FULL GENERALITY

:3€

There's a quote that I'm sure many of you have heard that goes "the axiom of choice is obviously true, the well-ordering principle obviously false, and who knows about Zorn's lemma". It sums up my feelings about the axiom pretty well! In general, I think it's a bit silly to say that a mathematical object 'exists' if you can't explicitly point to it. I'm hesitant to say, for example, that the real numbers are well-orderable, or that there exists a Hamel basis of the reals over the rationals.

But to be honest, my issue isn't even really with the proper, full axiom of choice (concerning collections of arbitrary cardinalities), but rather the principle of finite choice: the statement that given a finite collection of non-empty sets we can form a set that contains exactly one element from each of the sets in the collection. This is not actually an axiom of ZF set theory; it follows instead from the underlying logical framework. The axiom of choice is taken as 'obviously true' by analogy to the principle of finite choice! The issue is that even finite choice is non-constructive in nature; it 'produces data' from nothing. Let's reduce to a single set. We assume that this set is not equal to the empty set ('non-empty'). How do we now get an element of this set? Well, we know it's non-empty, so just pick one of its elements! We know it has at least one by assumption. In general, though, this does not tell us which element we have. This is exactly the issue with the full axiom of choice (or countable choice lol)! It's non-constructive.

This is why constructive set theory distinguishes between a set that's 'non-empty', which is taken to mean that assuming the set is empty leads to a contradiction, and a set that's 'inhabited', which means that we can construct an element of the set. The axiom of choice (finite or infinite) is valid for collections of inhabited sets, but not for non-empty sets (compare this to the fact that, even in ZF, it is provable that the category of sets has all small products, even though AC is equivalent to the statement that any set-sized collection of sets has a non-empty Cartesian product). I'm not all that attached to the framework of intuitionistic logic that's employed for constructive mathematics (I'm currently in the process of being dialetheism-pilled by @apovivdic), but I think this is a good perspective on the axiom!

This whole thing makes the axiom of choice kind of a muddy concept, I think. It looks different from different perspectives. Of the three famous equivalent statements, I prefer giving Zorn's lemma the ontological primacy of being chosen as an axiom. It's a bit more esoteric to get used to, but I think that conceptually it's got the most power behind it, and is most closely attached to the idea of taking a process that you can continue as far as you want finitely (such as picking linearly independent vectors in a vector space, or partial choice functions, or well-orders of subsets) and then declaring 'do this infinitely' and you'll get the 'end product' of the iteration process.