# Axiom of Choice — Why is it an axiom and not a theorem?

My question is only indirectly about the axiom of choice, I just happened to come to the question via the axiom of choice and will use it to illustrate my problem.

So far I thought axioms were propositions that were a) asserted to be true and b) consistent with the remaining theory.

Now I read on the axiom of choice, and something feels strange about it. Isn't there a difference between an axioms such as

$$0 \textit{ is a number}$$

$$\textit{if n is a number then s(n) is a number}$$

on the one hand axioms such as

$$\textit{for any relation } R, \textit{ there exists a function } f \textit{ such that } f\subseteq R \land \operatorname{dom}(R) = \operatorname{dom}(f)$$

on the other? This sounds a lot more like a theorem than an axiom. I cannot quite put my finger on it, but something is different between this one and the first two examples.

So, how can this axiom specifically be an axiom and how generally speaking can axioms like this one, that feel more like theorems, be axioms? Why do such propositions not need to be proven and can be asserted axiomatically?

• Whether something is an axiom or a theorem has nothing to do with the complexity of the formulation. – Arthur Nov 11 '17 at 23:59
• It's not a theorem, as it is not a logical consequence of the remaining axioms of set theory. – Lord Shark the Unknown Nov 12 '17 at 0:01
• How do you feel about the (relatively complicated) parallel postulate being one of Euclid's axioms for Euclidean geometry? – Eric Towers Nov 12 '17 at 0:02
• @EricTowers That makes intuitive sense, but I feel the same way about it as the axiom of choice (which also makes intuitive sense, I guess). – user3578468 Nov 12 '17 at 0:04
• @user3578468 Yes - this was proved by Paul Cohen in 1963. – Noah Schweber Nov 12 '17 at 0:19

Another useful comparision that's often made is to group theory. The axioms of group theory say that there are elements and a binary operation between them that obey certain properties. We find many structures that obey the axioms of group theory... we call them groups. There are many statements that are independent of the axioms of group theory. For instance $$\forall (x,y)\; x\cdot y = y\cdot x$$ is independent of the axioms of group theory since there are both abelian and non-abelian groups.
Similarly the axioms of ZF are that there are some elements (called sets) and a binary relation between them $$\in$$ such that $$x\in y$$ is interpreted as "$$x$$ is an element of $$y$$." We call a structure that obeys ZF a "model of ZF" (doesn't have a snappy name like "group"). Cohen and Godel showed that the axiom choice is independent of the ZF axioms just like the "commutativity axiom" is independent of the axioms of group theory.