The main challenge here is explaining the precise set-theoretic statement which is meant by "we can make finitely many choices without the axiom of choice"; the proof is then relatively easy. I am going to write in a sort of semi-formal way, which I hope will be clear enough that you can see how to translate into statements of ZF.
By CHOICE, I mean the statement:
Let $X$ and $Y$ be sets, with a map $\pi: X \to Y$. Suppose that, for every $y \in Y$, there is an $x \in X$ with $\pi(x) = y$. Then there is a subset $K$ of $X$ such that, for every $y \in Y$, there is a unique $x \in K$ with $\pi(x) = y$
So $X$ is the set we are choosing from (the set of all socks in the universe), $Y$ is the number of choices we're making, and $K$ is the set of choices we make.
Now, I want to show that this statement is true if $Y$ is finite. So we must discuss the definition of finite.
For any set $Z$, define $s(Z) = Z \cup \{ Z \}$. A set $I$ is called inductive if $\emptyset \in I$ and if, for all $Z \in I$, we also have $s(Z) \in I$. One can show (see any intro set theory book) that there is a unique set $\mathbb{N}$ such that (1) $\mathbb{N}$ is inductive and (2) every inductive set contains $\mathbb{N}$. A set $Y$ is called finite if it can be put in bijection with some member of $\mathbb{N}$.
We have now finished the definitions, and can move to the proof. We are going to show that, if $A \in \mathbb{N}$, if there is a bijection $Y \to A$, and if we have any map $\pi: X \to Y$ satisfying the hypotheses of CHOICE, then the conclusion of CHOICE holds.
First of all, composing $\pi: X \to Y$ with the bijection $Y \to A$, we may assume that $Y$ is an element of $\mathbb{N}$. (Exercise!)
Let's say that "we may make $Y$ choices" if CHOICE is true for $Y$, for all $\pi$ and $X$. Let $T \subseteq \mathbb{N}$ be the set of those elements $Y$ of $\mathbb{N}$ for which we can make $Y$ choices. (Exercise: Actually write out the definition of $T$ set theory notation.) We will show that $T$ is inductive.
First of all, we can make $\emptyset$ choices. Take $K = \emptyset$.
Now, suppose that we can make $Z$ choices. We must show that we can make $s(Z)$ choices. Consider any map $\pi: X \to s(Z)$. Let $X' = \pi^{-1}(Z)$, using the inclusion $Z \subseteq s(Z)$. So, by hypothesis, there is a subset $K' \subseteq X'$ such that, for every $y \in Z$, there is a unique element $x \in K'$ with $\pi(x) = y$. Also, by the hypotheses of AC, there is an element $x \in X$ such that $\pi(x) = \{ Z \}$. Take $K = K' \cup \{ x \}$.
We have now shown that $T$ is inductive, so $\mathbb{N} \subseteq T$. But also $T \subseteq \mathbb{N}$, by construction. So $T = \mathbb{N}$. We have shown that we can make $Y$ choices for every $Y \in \mathbb{N}$, as desired.
By the way, you may notice that this proof looks a lot like a proof by induction. This is how you write a proof by induction in ZF. Set theorists writing for a more experienced audience would just say "do it by induction", without all the explanation I've given.
An interesting question, that would take many pages to begin to answer! We make a small disjointed series of comments.
In the last few years, there has been a systematic program, initiated by Friedman and usually called Reverse Mathematics, to discover precisely how much we need to prove various theorems. The rough answer is that for many important things, we need very much less than ZFC. For many things, full ZF is vast overkill. Small fragments of second-order arithmetic, together with very limited versions of AC, are often enough.
About the Axiom of Choice, for a fair bit of basic analysis, it is pleasant to have Countable Choice, or Dependent Choice, at least for some kinds of sets. We really want, for example, sequential continuity in the reals to be equivalent to continuity. One could do this without full DC, but DC sounds not unreasonable to many people who have some discomfort with the full AC. This was amusingly illustrated in the early $20$-th century. A number of mathematicians who had publicly objected to AC turned out to have unwittingly used some form of AC in their published work.
Next, bases. For finite dimensional vector spaces, there is no problem, we do not need any form of AC (though amusingly we do to prove that the Dedekind definition of finiteness is equivalent to the usual definition.)
For some infinite dimensional vector spaces, we cannot prove the existence of a basis in ZF (I guess I have to add the usual caveat "if ZF is consistent"). However, an algebraic basis is not usually what we need in analysis. For example, we often express nice functions as $\sum_0^\infty a_nx^n$. This is an infinite "sum." The same remark can be made about Fourier series. True, we would use an algebraic basis for $\mathbb{R}$ over $\mathbb{Q}$ to show that there are strange solutions to the functional equation $f(x+y)=f(x)+f(y)$. But are these strange solutions of any conceivable use in Physics?
Finally, why should the Banach-Tarski result be unacceptable to a physicist as physicist? It is easy to show that the sets in the decomposition cannot be all measurable. In mathematical models of physical situations, do non-measurable sets of points in $\mathbb{R}^3$ ever appear?
Best Answer
There is no "easy" way to get intuition. If you want to get better you need to solve exercises. Many of them.
Two wonderful sources for exercises are:
In addition you can also use the many answers on this site which contain somewhat deep explanations, and try to extract some semblance of intuition from them.
But the real truth is that choice is finicky. Choice is hard. Choice is confusing. Infinite sets are weeeeeeeeirrrrrdddddd.Even I don't have a very amazing intuition without choice, because there's always stuff you've never thought about, stuff that's confusing you, stuff that's surprising you. It never ends. And that's part of the fun!