Do We Need the Axiom of Choice for Finite Sets? 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.
 A: The ability to give a name to some arbitrary element of a nonempty set is known as "existential instantiation". This is an inference rule of the underlying logic, not part of the theory, and so it is included not only in ZFC, but also in ZF, and in appropriate forms it is also included in PA and every other first-order theory. 
The intuition is that giving a name to an object does not really require "choosing" an object; if we know that there is an element in a set $A$, and we begin arguing about some "given" element $c \in A$, we do not have to actually make a choice, we can just reason hypothetically ("what if we knew an element $c$ of $A$?"). This reasoning will be sound because $A$ really is nonempty. However, because we don't know which element is chosen, the only properties we know it has are the ones we can prove every element of $A$ has. In particular, we cannot assume that the element we are given is equal to any other object we already have, unless we can prove they are equal. So we need to give a new name that we are not already using for any other object. 
The word "choose" is used in several ways in set theory, both in this way (existential instantiation), and in ways corresponding to the axiom of choice, and in ways where there is not really any choice, for example when we have a function $f$ and a set $x$ and we "choose" $y$ such that $f(x) = y$. You have to look at the context to tell what formal proof is being suggested by the informal proof that you read. 
You might be thinking that "choosing" a single element from a set would be an algorithmic operation, but this is just not the case. The nonconstructivity of existential instantiation is a direct consequence of the nonconstructive meaning of $\exists$ in classical logic. To get a system where you can effectively choose a witness to any true existential statement, you have to move to constructive mathematics, but then the meaning of $\exists$ changes as well. 
A: You do not need to "choose" $x$ (what do you mean by "choosing" $x$?) You only need to prove the at least one $x$ exists, which is actually your assumption (the set is nonempty), so there is nothing to prove.
The Axiom of Choice does not "choose" a choice function, it only says that at least one choice function exists. It can be stated in the following form:

The Cartesian product of a family of nonempty sets is nonempty.

For one set this is obvious.
A: If $S$ is non-empty and finite then, by definition, there exists a bijection $f$ with a non-empty initial prefix of the natural numbers.  Choose $f(1)$.
A: Saying S is not empty, therefore there is an x∈S, does not suffice.

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
Let x∈S
...
Therefore P

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).
A: There are two things. Let $(A_i)_{i\in I}$ be an arbitrary family of nonempty sets. One version of the axiom of choice says that $\prod_i A_i\neq\emptyset$. We cannot prove this without the axiom of choice if we know that for all $i\in I$ the set $A_i$ is finite. What we can show is that the product is nonempty if $I$ is finite!
The proof goes like this: We show that for each $n$, if $I$ has $n$ elements, then the product is nonempty. We do this by induction. Without loss of generality, we let $I=\{1,\ldots,n\}$. If $I$ contains a single element, showing that the product is nonempty amounts to finding an element in the single set $A_1$. That this can be done is simply the meaning of $A_1$ being nonempty. So suppose there exists a choice function $(a_1,\ldots,a_{n-1})$ defined on $I\backslash\{n\}=\{1,\ldots,n-1\}$. Since $A_n$ is nonempty, there is some $a_n\in A_n$. This gives a choice function for $I$ given by $(a_1,\ldots,a_{n-1},a_n)$. And for this, we don't need the axiom of choice.
A: The axiom of choice, as said, allows us to choose from infinitely many sets at once (sometimes even when these sets are finite!). If, however, one only wishes to choose from finitely many sets then this can be done without it. It does not even matter if the sets themselves are finite or not.
Choosing an element from $A$ means fixing a particular element from $A$. If we can name it ($0$, for example chosen from the real numbers) then it's fine. If we does not know the name of the element in advance then we have to assign it a name.
We do that using the infamous "let", and from that point we agree that the assigned name refers only to that particular element. e.g.

Let $r\in\mathbb R\setminus\mathbb Q$...

What happens is that since we assume that $A$ is not empty then the proposition $\exists x(x\in A)$ is true. Now writing the rest of the proof we can think of it as a list of formulas that $x$ is one of the free variables in those formulas, let us call them $\varphi_1(x,y_1),\ldots,\varphi_k(x,y_k)$.
When we choose an element from $A$ we say: $$\ldots\exists x(x\in A\land\varphi_1(x,y_1)\ldots\varphi_k(x,y_k))\ldots$$
So we have some previous proposition, some other variables assigned and we have the proof itself in the middle, and we assign it an arbitrary $x$.
(Note that if we require $x$ to have a certain property then we replace $A$ with a subset of $A$ of "all the elements that have the required property in $A$", of course we sometimes need to argue that this set is not-empty!)
If you understand this explanation it shouldn't be hard to see why we can choose finitely many elements from finitely many non-empty sets as well.
A: One reason AC is not needed for a finite number of arbitrary choices lies in formal logic. In his Introduction to Mathematical Logic, 4th ed., p. 81-83, E. Mendelson shows how a deduction using "Rule C", involving a finite number of arbitrary choices, can be reduced to a formal deduction without such choices. The mathematical practice of making choices is viewed as a shortcut for the formal deduction. Since deductions can only involve a finite number of choices, one needs a new axiom if one wants to make an infinite number of choices within the proof.
