Would mathematics based on lists obviate the need for the axiom of choice?

Question

I'm trying to wrap my head around the axiom of choice and its equivalent well-ordering theorem. Imagine a mathematics founded on ordered lists rather than sets. So by construction, wouldn't every mathematical object would be well-ordered and thus wouldn't the axiom of choice merely be a theorem rather than an axiom? Would this "list theoretic" mathematics be less expressive than ZFC?

Answer 1

Maybe working in the constructible universe, or Gödel's model of ZF would be interesting for you. There we restrict our universe (to so-called constructible sets), so that Choice becomes a theorem and we also have a "constructive" well-order of the whole universe. It solves many independent questions in a definite way (GCH holds e.g., and there is a Suslin line and many more interesting objects).

Answer 2

Well, the question is what is a list. If a list is just a well ordered set, then in principle you are correct.

In some sense this is similar to working with Global Choice, where every set has a distinguished well ordering.

The problem is formalizing lists is somehow more elaborate than formalizing sets. Since lists have an inherent structure to them, you need to incorporate this into your language and into your semantics. It's not impossible, but what do you get that you can't do with ZFC, or ZF+Global Choice? Ultimately, not much.

Answer 3

The usual proof that well-ordering implies a choice function $f$ exists on $X\not\owns\emptyset$ notes that if $\le$ well-orders $\bigcup X$, any $x\in X$ has a $\le$-minimal element, say $y$, because $x\subseteq\bigcup X$; we can thus define $f(x):=y$.

This argument requires $\bigcup X$ to exist for each such $X$. In set theory, that's no problem; it's the axiom of union. For a theory of sorted lists to work the same way, we need the union to admit a specific ordering as well.

So if your universe of objects is well-ordered, every list can just be an ordered sample therein, in which case choice is trivial. But then you're basically studying, in a non-standard formalism, the subsets of some universe nowhere near as general as we like to consider in foundational mathematics.

For example, our ordered lists could be of ordinals, so $<=\in$. It's true we can construct an easy choice function on any set of nonempty sets of ordinals. But one cannot, for example, easily identify the real numbers (or which are less naturally ordered, the complex ones) with ordinals in a way that makes this useful.