How does the axiom of choice relate to logic?

Question

The axiom of choice is (so I'm told) often necessary to perform certain proofs.

It is a kind of "meta-mathematical" axiom it seems to me, in the sense that it doesn't relate to any specific mathematical theory (such as groups or topologies), but is kind of "assumed in the background". In this sense, it is similar to logical axioms, like LEM (law of excluded middle).

But the axiom of choice is an axiom of set theory, not of logic, so I am confused by the relation between logical axioms such as LEM, and the axiom of choice. So how does the axiom of choice relate to logic? Is there a sense in which the axiom of choice is a "logical axiom"? Or am I thinking in the wrong direction?

EDIT: Response to some comments: I know that the axiom of choice is an axiom in set theory (though it can also be stated in type theory), and that set theory is a foundation of math. I however am still confused. It seems that we need the axiom of choice to prove certain theorems within a theory $T$, even when the axiom of choice is not part of the axioms of that theory $T$.

For example, take the theory $T$ of groups (i.e. $T$ consists of the group axioms). Then as far as I know, all we need is the logical axioms (e.g. the standard axioms of first order logic), and the group axioms in $T$. Yet somehow we sometimes still in addition need the axiom of choice. How is this possible, given that the axiom of choice is not part of our logical axioms nor the axioms in $T$?

Answer 1

The axiom of choice, as far as 2019, and as far as "standard foundations" go, is an axiom of set theory, which is a foundation of mathematics.

You could argue that the power set axiom "just sits there in the background, lurking about, doing nothing but scaring those poor predicativists", because you use it to prove that uncountable sets exist.

Historically, however, Zermelo is known to have viewed choice as a logical principle. It can be seen as an inference rule, and this is how some second-order set theoretic proof assistant will prove choice in that sort of manner.

Regardless, progression in mathematics since 1904 moved the axiom of choice from an inference rule to a set theoretic axiom.

---

To the edit about group theory. Let's review for a moment where we actually need the axiom of choice in group theoretic proofs.

Since the axioms of a group cannot even decide if a model has some finite number of element, there are infinite models of any size. The axiom of choice comes in when we want to say something like "Every set carries a group structure" (which is equivalent to the axiom of choice). But this is not a statement in the language of groups, it's not even a statement about groups. It's a statement about sets.

Okay, so maybe the axiom of choice enters when we want to say that every divisible abelian group is injective, or every free abelian group is projective. Those are each equivalent to the axiom of choice. But again, these is not a statement in the language of groups. This is a "meta-theorem" about groups. The properties of projectivity and injectivity are not first-order anymore, they quantify over other groups and group homomorphisms. So this is really not something where choice enters "in the logic", but rather that the statement "exceeds the logic".

So what about this, and about all those rings and vector spaces and whatnot? Well. As with many cases, the axiom of choice is needed to produce some coherent choices. If we restrict all our attention to countable groups (i.e., define "countably injective groups" as those satisfying injectivity when all the groups involved are countable, etc.) then the axiom of choice will not be necessary anymore.

Choice, as I often said, is used to make our statement neat. Even if we mostly (or only) care about countable objects, or countably generated objects, choice makes mathematics simpler. It lets us generalize things to "all infinite objects", rather than "all countable objects" or "all well-ordered objects".

Despite all that, it's still a set theoretic axiom, and it comes into action when you move from the first-order theory of something to statements which actively involve quantifying over all possible models of a theory.

Answer 2

The axiom of choice is an extra-logicical axiom, while LEM is a logical axiom. The logical axioms apply no matter what subject you are studying. If you are studying group theory you have the extra-logical axioms of identity, associativity, and so on. If you are studying set theory you have a set of axioms for the set theory you are working in. If it is ZFC, the axiom of choice is one of them. If it is ZF, it is not. You can't prove as much in ZF as you can in ZFC because you don't have the axiom of choice available.