Axiom of Choice: Where does my argument for proving the axiom of choice fail? Help me understand why this is an axiom, and not a theorem.
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.
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.
This is a confusing matter, mainly because the kind of reasoning you use in your proof is usually taken to be valid.
However, in order to formalize that reasoning in axiomatic set theory, we need to reduce it to particular symbolic formulas in a formal logic system. And it turns out that the rules of symbolic logic and set theory that are sufficient to express most other kinds of generally accepted proofs can't by themselves express your reasoning.
We declare that this is not the fault of your reasoning, but of the limited logical rules we already have. Then we set out to fix our axiomatic set theory by adding a new rule stating that it's allowed to do what you do. This new rule is the axiom of choice.
So the problem with your proof is not that it doesn't work, from the perspective of ordinary mathematics -- but that what it does is not very interesting. It just says that if we accept this kind of reasoning, then we must conclude that this kind of reasoning works, which doesn't really tell us anything.
What a "proof of the axiom of choice" ought to be would be an argument that even if we don't extend our system with this new rule, we can still prove everything we can prove with the rule. But that means that the proof has to be done with fewer tools than we normally allow ourselves to use.
Otherwise, the end result would be something like claiming that you don't need to buy a hammer for your toolbox, because you can still drive in nails. How? Well, just hit the nail with a hammer ...