In terms of purely set theory, the axiom of choice says that for any set $A$, its power set (with empty set removed) has a choice function, i.e. there exists a function $f\colon \mathcal{P}^*(A)\rightarrow A$ such that for any subset $S$ of $A$, $f(S)\in S.$ Is this correct?
My question then is about proving this fact, so that we do not need to put it as an axiom. Now as per the research done on this single object- Axiom of Choice, I believe here that there should be some falsity in my argument. I do not find the mistake.
For any $S\in \mathcal{P}^*(A)$, since $S\neq \emptyset$, $\exists s\in S$. Define $f(S)=s$. Then $f$ is a choice function.
This was showing me that the axiom of choice is proved, but then why it had been put as an axiom? For example, in this book, the author asserts that
It is a metatheorem of mathematical logic that it is impossible to specify the function that assigns to each non-empty subset of $\mathbb{R}$, an element of itself.
There are several notes and books on axiom of choice, but here I am trying to understand through doing some argument for some problem, where problem actually arises.
Best Answer
When you move from $\exists s\in S$, to specifying "Let $s$ be an element of $S$" you are using what is known as existential instantiation. This is an inference rule of the underlying logic, stating that if there are objects satisfying some property, we can add a new symbol to the language with the statement that this symbol satisfies our property.
So you can apply it once, or twice, or thrice, and if you live long enough and all you do is apply it, then maybe even a few trillion times. Sure, all that is fun and games. But how can you apply it to each and every set of real numbers?
You simply can't.
So what you did there, really, was to say that you have a function mapping $S$ to an element of itself, and that this was your uniform existential instantiation. But why would such a function exist? Well, the answer is that without postulating its existence, it is possible that no such function exists. So you need to have the axiom of choice to assert the existence of such a function, which happens to be exactly what the axiom of choice is doing: it allows you to take all those sets, and get existential instantiation for all of them for the price of one; namely, you only need to instantiate the quantifier stating "There exists a choice function" once, and the rest is given.
Let me add two remarks here.
Zermelo, historically, treated the axiom of choice as a principle of logic, rather than an axiom of set theory. Probably to do exactly what you did there.
Many modern proof assistants prove the axiom of choice, by exactly the same argument as this. When you eliminate existential quantifiers like this uniformly, you simply get a choice function. This is not a bug per se, it's more of a consequence of the design features.