42
$\begingroup$

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.

|cite|improve this question
$\endgroup$
  • 5
    $\begingroup$ The intuitive idea is that when you say "since $S \neq \emptyset, \exists s \in S -$ Define $f(S)=s$" you are fixing $S$. If you want to do this for all $S \in \mathcal{P}^*(A)$, you must simultaneously do this for all of them, not fixing one at a time, otherwise you may be doing infinite things simultaneously, which the other axioms and the standard rules do not allow. Of course, this is a naive approach, and someone with real knowledge will appear soon, but this interpretation may help for now. $\endgroup$ – Aloizio Macedo♦ Jun 26 '16 at 5:33
  • 2
    $\begingroup$ No. Think about it as a computer program. We can estabilish a program to associate a natural number to two times itself. This is a finite program, so this is allowed, even though it results in a function defined on a infinite set. It defines a "uniform" rule. The problem is that your process (in your question and suggested proof) may not be finite, since you are fixing an element every time to define the process. How will you "uniformly" glue everything in a finite way? $\endgroup$ – Aloizio Macedo♦ Jun 26 '16 at 5:42
  • 3
    $\begingroup$ @Jyrki: Allow me to play the devil's advocate, I mean, the axiom of choice advocate (aren't those two the same?) and answer your point. We are not making infinitely many choices. We are making one choice, the choice of enumeration. From there everything is firmly unique: the diagonal values, the diagonally-produced real, and the proof it is not on the list. (Your last comment reminds me of a recent paper I wrote for an analysis course---to be posted online sometime in the future---where I claim that the work about analysis in non-choice context is meant as proof by intimidation to accept AC.) $\endgroup$ – Asaf Karagila♦ Jun 26 '16 at 6:28
  • 2
    $\begingroup$ @JyrkiLahtonen: To clarify further, the construction of a real number not on your list proceeds via unique definable choices at each step, and by induction we can construct a sequence $(x_n)_{n\in\mathbb{N}}$ of compatible digit sequences, namely that $x_n$ is a prefix of $x_{n+1}$ for every $n\in\mathbb{N}$, and then we can by suitable use of axiom of union construct the limit, which is an infinite sequence compatible with every $x_n$, and that limit is what we seek. $\endgroup$ – user21820 Jun 26 '16 at 16:10
  • 2
    $\begingroup$ @immibis: The point is that when you only choose finitely many points, you can delegate this to existential instantiation and induction. Problems begin with you can't describe something with a single formula, whose length is finite. You can argue that the choice is not necessarily well-defined, but if you apply the instantiation on the set of all objects with exactly the properties you need, it won't matter either (it will just be a fixed, but arbitrary selection for the remainder of your proof). $\endgroup$ – Asaf Karagila♦ Jun 27 '16 at 10:48
52
$\begingroup$

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.

  1. 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.

  2. 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.

|cite|improve this answer
$\endgroup$
  • 3
    $\begingroup$ Good explanation. I like the way your answer actually gets into the formal systems side of things, while magically not getting too bogged down in technical nonsense. Impressive! $\endgroup$ – goblin Jun 26 '16 at 6:02
  • 7
    $\begingroup$ Practice makes perfect... it ain't my first rodeo. :-P $\endgroup$ – Asaf Karagila♦ Jun 26 '16 at 6:03
  • $\begingroup$ The last remark is interesting; could you elaborate? (Also, it might be worthwhile to explain how "uniform" is being used here.) $\endgroup$ – joriki Jun 26 '16 at 6:11
  • 1
    $\begingroup$ @joriki: I just know this from a talk I heard by Peter Koepke about his project NAPROCHE. If I remember correctly, the point is that the system does this uniform existential instantiation. Similar to how some constructive systems prove the axiom of choice: if you could have proved that all the sets are non-empty, you could only do it by essentially being able to uniformly exhibit elements of those sets, which is your choice function. $\endgroup$ – Asaf Karagila♦ Jun 26 '16 at 6:20
  • 10
    $\begingroup$ The reason for the last part is that many proof assistants are based on constructive logic, in which the proof of existence of $s$ is exactly the choice function required, according to the Curry-Howard correspondence. However, this form of AC doesn't have the same far-reaching consequences as in classical set theory, though stronger formulations exist which are more analogous. $\endgroup$ – Lily Chung Jun 26 '16 at 8:18
19
$\begingroup$

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 ...

|cite|improve this answer
$\endgroup$
  • $\begingroup$ Excellent answer, +1! $\endgroup$ – joriki Jun 27 '16 at 14:31
  • $\begingroup$ @Henning: much clear explanation. $\endgroup$ – p Groups Jun 28 '16 at 3:14
  • $\begingroup$ This is lovely, +1. It's worth mentioning in this vein that the axiom of determinacy, which contradicts choice, also corresponds to a "higher deduction principle" - roughly, it lets us apply De Morgan's laws to infinite sequences of quantifiers over $\mathbb{N}$. $\endgroup$ – Noah Schweber Aug 29 '17 at 0:36
  • $\begingroup$ This is a good answer so I upvoted it. Just because you can't prove a statement in a system does not mean it's not provable. I don't find the axiom of choice obviously true myself. However, there are systems of pure number theory that you can prove that everything they prove is true and from that prove that a specific statement the system describes is both true and unprovable in the system. $\endgroup$ – Timothy Apr 6 '18 at 18:56
  • $\begingroup$ I figured out another reason I like this answer. For super intelligent people, they probably don't feel the need for any answer to this question but if they feel the need for some answer, that's probably because they don't know how to write a formal proof in ZF so this will probably be the only answer they feel is helpful to them. For those superintelligent people who know how to write a formal proof in ZF, Asaf Karagila's answer is probably not helpful because they can think of their own proof that no formal proof of the axiom of choice in ZF exists. $\endgroup$ – Timothy Apr 6 '18 at 21:25
15
$\begingroup$

This is a misunderstanding about the essence of axiomatic set theory. In axiomatic set theory, you don't assume that a set exists because you can think of it; in a sense, the entire point of axiomatic set theory is not to do that, to decouple the notion of existence of sets from such pre-existing (pun intended) notions.

When you say "Define $f(S)=s$", you're already assuming that $f$ exists. The point of the axiom of choice is to allow you to deduce the existence of $f$ from the axioms. If this seems unnecessarily formal, consider that before the advent of axiomatic set theory it probably seemed unnecessarily formal to ask whether the set of all sets that don't contain themselves exists. What do you mean, does it exist? Just define $A=\{x\mid x\text{ is a set that doesn't contain itself}\}$!

|cite|improve this answer
$\endgroup$
  • 2
    $\begingroup$ I downvoted, perhaps a little unfairly, because I disagree that the issue relates to the statement "in axiomatic set theory, you don't assume that a set exists because you can think of it" and because a good answer should attempt to show the issue with the OP's proof. And, you have a lot of Rep, you know, so I didn't feel too guilty :) haha. Have a nice day :) $\endgroup$ – goblin Jun 26 '16 at 5:55
  • 5
    $\begingroup$ @goblin: Thanks for the explanation! I'm not worried about my rep, I'm worried about my grasp of axiomatic set theory :-). I think our disagreement is basically the same as above with Aloizio Macedo; we have different impressions of where the OP stands and what their problem is; you're considering this as a flawed proof within axiomatic set theory, and I took it as an attempt to prove an axiom, not on the basis of other axioms, but on the basis of pre-existing notions of existence. Hopefully we'll hear from the OP which is closer to their thinking. $\endgroup$ – joriki Jun 26 '16 at 6:00
  • 3
    $\begingroup$ This is not a terrible answer. I don't know if it hits the nail on the head, or if it just touches a tangent issue which may or may not be the cause of confusion. But it certainly not something I'd consider worth downvoting beyond the first downvote. $\endgroup$ – Asaf Karagila♦ Jun 26 '16 at 6:03
  • 5
    $\begingroup$ @joriki: Wait another year, and it will be coming from the doctor! :D $\endgroup$ – Asaf Karagila♦ Jun 26 '16 at 6:29
  • 4
    $\begingroup$ Admittedly, after the recent meta thread about being nice to downvoters, this comment thread is a refreshing pace of discussion on the merits and problems of this answer. Good job everyone. $\endgroup$ – Asaf Karagila♦ Jun 26 '16 at 18:07
11
$\begingroup$

Good question!

This is really subtle stuff; its impossible to give a proper answer without picking an actual formal system for first-order logic and trying to formalize your argument inside. After a lot of struggle, you'll notice that it can't be done.

An informal explanation, however, is that you're implicitly using the "logicians" axiom of choice:

AC. For all sets $X$ and $Y$ and all predicates $P : X \times Y \rightarrow \rm\{True,False\}$, we have: $$(\forall x \in X)(\exists y \in Y)P(x,y) \rightarrow (\exists f : X \rightarrow Y)(\forall x\in X)P(x,f(x))$$

in going from

$$\forall S \in \mathcal{P}_{\neq 0}(A) \exists s \in A(s \in S),$$

which is provable in ZF, to

$$\exists s \in (\mathcal{P}_{\neq 0}(A) \rightarrow A)\forall S \in \mathcal{P}_{\neq 0}(A) (s(S) \in S),$$

which isn't provable.

You may be interested in this old question of mine.

|cite|improve this answer
$\endgroup$
  • $\begingroup$ Thanks for the link at the end. Yes, an interesting question. $\endgroup$ – almagest Jun 26 '16 at 19:19
  • $\begingroup$ @almagest, no worries. Thanks for your interest :) $\endgroup$ – goblin Jun 27 '16 at 10:40
  • $\begingroup$ Is it intentional that you use the letter $s$ for two very different things? I found this confusing. Why not call the second $s$ "$f$", as in the OP? $\endgroup$ – Torsten Schoeneberg Sep 8 '18 at 12:15
  • $\begingroup$ @TorstenSchoeneberg, I did it intentionally because I actually find this less confusing, but in light of your comment maybe this was a bad idea. But anyway, it's supposed to illustrate the relationship between notations like $y = x^2$ and the corresponding notation we sometimes see, namely $y(x) = x^2$. $\endgroup$ – goblin Sep 9 '18 at 1:44

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.