Is the Axiom of Choice needed to choose a single element from an uncountable set?
I did a proof for a topology class regarding open covers which starts out like so:
Let C = {U_a : a in A} be an open cover for X. Pick some a_0 in A, and let x be in X-U_{a_0}…
Did I invoke the Axiom of Choice by saying “pick some a_0 in A”?
(Not homework–class is now over. Just curious)
Forgot to mention: This is assuming X is an infinite set, possibly uncountably infinite, and so the cover C and hence its index set A could be infinite as well.
No, the axiom of choice is never needed to choose a single element from a set which is known to contain at least one. It is only needed in order to make infinitely many simultaneous choices (e.g., “Assign to each nonempty set of reals a particular element from within it”), when there is no other clear means of doing so around (for example, you don’t need the axiom of choice to pick elements from every nonempty set of naturals, since you can use the rule of always picking the smallest one in the set, for example).
In general, yes. You need the axiom unless you can explicitly give an algorithm for picking an element out of your set.
I think you may have misread the OP; he is only making a single choice (one element selected from one set), not the sort of situation in which conventional mathematicians require the axiom of choice.
Apparently I misunderstand something. Given an uncountably infinite set X, how do you choose an element?
Well, there’s distinctions between different notions of what it means to “choose” an element, but the sort of thing the axiom of choice does for you is something you already can do without it in the case of making a single choice.
What kind of choice does the axiom of choice allow? Well, one common way to put it is this*: given a set of sets X = {A, B, C, …}, all of whose elements (A, B, C…) themselves have at least one element, then there is a function f on the domain X having the property that f(A) is an element of A, f(B) is an element of B, and so on. That is, the choice function f picks a particular element out of each thing in X; however many things are in X, f makes that many choices simultaneously. Without the axiom of choice, we still know, of course, that everything in X has at least one corresponding element; what the axiom of choice tells us is the additional fact that there’s actually a particular function carrying out the correspondence, so to speak.
The other axioms of set theory aren’t enough to always prove the existence of such an f, without the axiom of choice. However, if there’s only one thing in X (say, X = {A}), then you will be able to prove the existence of such an f without the axiom of choice; in this case, such an f just has to have the property that f(A) is an element of A. Well, by stipulation, A has at least one element. Therefore, there exists a constant function sending A to one of its elements, which suffices to be our f. [Or, as this last part is more likely to be written in normal mathematics, “A has at least one element. Let c be such an element of A. Define f as the constant function on the domain {A} sending its input to c.”]
You might object that I’ve snuck in a kind of choice there, that I went from “A has an element” to reasoning as though I had chosen a particular such element which I named c. But standard logic allows us to make this kind of move, from “There exists an x such that P(x)” to any conclusion derivable from “P©” which does not itself mention c, where c is a ‘fresh’ name. (This is the rule of existential elimination in first-order logic). Having this kind of reasoning available in our logic suffices for us to be able to prove a finite version of the axiom of choice; that is, to make finitely many choices. But one is unable to prove the full axiom of choice with just this kind of reasoning, which is why one must explicitly adopt it as an additional axiom to the others of one’s set theory if one intends to make use of it.
*: This is not my preferred way of formulating the Axiom of Choice, but it is a very common set-theoretical way of doing so, so I’ve used it for the sake of avoiding confusion. There are a million differing equivalent ways to state the Axiom of Choice; one which I like is as the statement that every surjection has a right inverse.
Came in to learn from some of the sharpest dopes around.
It is not often that Indistinguishible and ultrafilter have a difference of opinion like this one.
Looking forward to seeing how this plays out, but please use small words so that I can understand. 
I would also state that, regarding what’s generally required for proving the existence of functions/ways of making simultaneous choices, without using the axiom of choice, talk of algorithms is probably not the best way to put it, certainly not in the context of classical mathematics. Talk of “rules” strikes me as better. For example, without the axiom of choice, I can classically prove that there is a function which sends computer programs to either True or False according as to whether they halt or not; there is an obvious rule defining such a function, which I have just stated in its description. However, it would seem appropriate to say there is no algorithm defining such a function, thanks to the undecidability of the Halting Problem. Rules can be much more general than algorithms, at least on a conventional understanding of the terms.
Ah, yes, the Thrilla in Mozilla. Take a look at his status icon; I’d say I’ve knocked his lights out. 
Honestly, I was pretty surprised to see that he “disagreed”; as you say, he’s one of the sharpest dopers around. I’m sure it was just something like a brain fart or different interpretation of words.
Just waiting for you to let your guard down. Then POW! Straight to the moon!
Nah, it’s just been too long since I studied this stuff, and my grasp on it is more tenuous than it used to be. I will have to wait till tomorrow to look at your technical posts.
I think maybe I should clarify in smaller/newer words my point above:
If by “choose an element of non-empty set X”, you mean “Give me an actual description which isolates a single particular element from X”, then of course I can’t do that for you; you haven’t even told me what the set X is. But, then, the axiom of choice won’t help you here either; it just tells you that certain choice functions exist, without giving any description that actually singles them out. And, if all you want is an existence proof without a description, you won’t need to invoke the axiom of choice in this case; by stipulation, X is non-empty (i.e., there exists an element within it), so such a proof is trivial.
What the axiom of choice becomes necessary for is something like “Each of X_0, X_1, X_2, …, is non-empty. Thus, let us define a sequence of elements a_0 in X_0, a_1 in X_1, a_2 in X_2, …” In proposing the existence of such a sequence, we are asking not just to make one choice, but to make a whole bunch of them, simultaneously. I.e., we want a proof not just that there are elements in each X_i (which is trivial to show; it was our stipulation), but, furthermore, that there is actually a function selecting a particular such element a_i for each index i. Demonstrating the existence of such a function is tricky if one has no means at hand for giving an explicit rule defining a particular such function; the axiom of choice is the principle that guarantees the existence of such a function, absolving us of the need to think up such a rule to “manually” prove its existence.
Note, however, that if we only had to make finitely many choices, then we could prove the existence of such a function “manually” anyway. The easiest way to see this is by considering the case where we already know there exists a sequence a_0, …, a_n chosen from X_0, …, X_n, respectively, and want to extend this to a sequence chosen from X_0, …, X_{n+1}. By stipulation, we will take X_{n+1} to have at least one element; it follows that there is at least one way of extending the old sequence a_0, …, a_n to a new one a_0, …, a_{n+1} doing what we want (in fact, there will be one such way for each element of X_{n+1}), and so, of course, such a sequence exists. Arguing inductively using this result, we find, even without assuming the axiom of choice, that finite “choice sequences” always exist. The axiom of choice only becomes necessary when we want to make an infinity of choices.
Also, another note of clarification: Plenty of mathematicians, though (the convention or majority or some such term) are happy to use the axiom of choice liberally, seeing no particular need to give arguments which don’t assume it or even to pay attention to whether or not they are invoking it implicitly.
Er, locked out of the edit window on the last paragraph:
Also, another note of clarification: Plenty of mathematicians, though (the conventional ones or the majority or some such term) are happy to use the axiom of choice liberally, seeing no particular need to give arguments which don’t assume it or even to pay attention to whether or not they are invoking it implicitly. Which is fine; I wouldn’t propose to tell them what systems they should and shouldn’t be working in. But there are also fascinating reasons to occasionally pay more attention and work without assuming it; such results often have applicability in broader areas than otherwise (i.e., even if one is of the philosophy the “actual” universe satisfies the axiom of choice, one should accept that other domains of mathematical discourse are a lot like the “actual” universe but fail to; results proven without assuming the axiom of choice would manage to hold even in those).
Also, re: the OP:
You haven’t used the Axiom of Choice here, but you have implicitly assumed that A (the set indexing the open cover C) is non-empty. However, if X is empty, then it is possible for C, and thus A, to be empty as well, so your proof, judging from what has been shown, only applies when X is non-empty.
Hence why I made the clarification in Post #2 
But thank you for the lucid answer. Ignorance was fought.
Oh, sorry, I somehow glossed over that clarification.