1
$\begingroup$

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$?

$\endgroup$
  • $\begingroup$ And what is LEM? $\endgroup$ – José Carlos Santos Apr 12 at 14:43
  • $\begingroup$ @JoséCarlosSantos Law of Excluded Middle, I assume. $\endgroup$ – kccu Apr 12 at 14:44
  • $\begingroup$ @JoséCarlosSantos, yes law of exluded middle (edited) $\endgroup$ – user56834 Apr 12 at 14:46
  • 2
    $\begingroup$ Just reading the Wikipedia page on Axiom of Choice ... this seems to be all about sets ... why do you think this is about 'pure' logic? $\endgroup$ – Bram28 Apr 12 at 14:47
  • $\begingroup$ Just a quick note that the full axiom of choice implies LEM, by Diaconescu's theorem, see e.g. Wikipedia. $\endgroup$ – Mark Kamsma Apr 12 at 14:47
9
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Thanks! This edit really clarifies things for me. I have not explicitly realized there is a distinction between such theorems "in group theory" and theorems "about groups". Do you know of some keywords I could google, or specific texts, for me to get a better understanding of this? $\endgroup$ – user56834 Apr 14 at 10:28
0
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Thank you for the answer. Note that I have edited the question in response. $\endgroup$ – user56834 Apr 13 at 15:43

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.