So I am relatively familiar with the Axiom of Choice and a few of its equivalent forms (Zorn's Lemma, Surjective implies right invertible, etc.) but I have never actually taken a set theory course.
I know there are times when an explicit way of choosing some elements may not be provided, and instead we call upon the Axiom of Choice to do it for us. But one thing has always bothered me.
I have heard that for a finite set we do not need the Axiom of Choice to choose an element. I find this a little confusing. How is choosing an element from a finite set any different than choosing from an infinite set? I have heard before "since the set it finite, there are finitely many orders, so order the set and choose the first element in the order." But how does one choose what order to use? This involves picking an element from a finite set, i.e. it presumes the conclusion.
I'm guessing there is a good reason why everyone keeps insisting that the Axiom of Choice in not needed to choose from finite sets, so could someone please explain it to me?
Edit: There seems to be confusion on what exactly I am asking. I know that we need the Axiom of Choice, sometimes, to make infinitely many choices, from finite or infinite sets. This is not what is confusing me. Allow me to be more precise:
Suppose $S$ is a nonempty finite set. I want to pick one element from $S$. Does choosing one element from $S$ require the Axiom of Choice? If not, how can the choice be made without the Axiom of Choice?
Saying $S$ is not empty, therefore there is an $x \in S$, does not suffice. How do I choose such an $x$? There is one, but how do I describe it without any information about the set, other than the fact that it nonempty and finite?
Another clarification: I am not asking about using "Let ... be given" as a proof technique.
Ah, but it does suffice! Knowing that $S$ is non-empty, there do exist such $x$, and so we can declare the symbol $x$ to denote an element of $S$, and the rest of our argument is then a function of $x$.
To put it more formally, a typical proof that chooses an element from $S$ has the form
and constitutes a proof of $\forall x: (x \in S \implies P)$, which in turn implies $P \vee (S = \emptyset)$.
Similarly, if you made two choices $x \in S, y \in T$, you typically prove a statement like $\forall x,y: \left( (x,y) \in S \times T\implies P \right) $.
This makes it clear how the axiom of choice enters the picture; a sequence of infinitely many choices indexed by $I$ of the form described above would be a proof of
$$ \forall x : \left(x \in \prod_{i \in I} S_i \implies P \right)$$
which implies
$$ P \vee \left(\prod_{i \in I} S_i = \emptyset \right) $$
i.e. a proof that $P$ is true or the family $S_i$ does not have a choice function (or both).