I recently read a proof that had the following in it: "since $A$ is non-empty, we can find an element $x$ in $A$." This proof did not mention the axiom of choice, but it seems to me that it would be required to make the proof formal. Would I not require a choice function to allow me to find/pick some element $x$ from $A$ after noting that A is non-empty? Thanks
Don't we need the axiom of choice to choose from a non-empty set?
7
$\begingroup$
elementary-set-theory
axiom-of-choice
-
0Of course, one could add a [choice operator](http://ncatlab.org/nlab/show/choice+operator) to the logical system, in which case one really can infer $\varphi (c)$ from $\exists x . \varphi (x)$, where $c = \tau_x \varphi (x)$... – 2012-09-19
1 Answers
8
The axiom of choice is needed when you need to make infinitely many arbitrary choices at once.
Recall that a set $A$ is not empty if and only if $\exists x. x\in A$, so assuming that $A$ is not empty we can provably pick such $x$.
-
0@Mahmud: Yes, that was Russell. – 2012-09-19