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
-
1No, you don’t need AC: you can always pick a single element from a non-empty set. – 2012-09-19
-
0Could you please explain why. I understand that there obviously exists an element in A, but why do I not need the axiom of choice to choose such an element? – 2012-09-19
-
3It follows from [one of the rules of first-order logic](http://en.wikipedia.org/wiki/Existential_instantiation). Informally, that rule says that from $\exists x~\varphi(x)$ one may infer $\varphi(c)$, where $c$ is a new name created specifically for the purpose of naming something that has the property $\varphi$. – 2012-09-19
-
0Very interesting. Thank you for this! – 2012-09-19
-
2@BrianM.Scott Mmmm, a bit misleading, methinks. Take an ND system. Given $\exists x\varphi(x)$, you make the (temporary) new assumption $\varphi(c)$, deduce something $\psi$ that doesn't depend on $c$, and discharge the assumption and conclude $\psi$ by $\exists$-elimination. But at no point do you *infer* something like $\varphi(c)$. – 2012-09-19
-
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