7
$\begingroup$

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

  • 0
    Of 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 1

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