In discussing this answer, I noted that while the statement:
Any vector space has a basis
is equivalent to the axiom of choice, I wondered if the statement that:
Any vector space either has a finite basis or an infinite set of linear independent vectors
was weaker than the axiom of choice. It feels weaker – it feels like you can inductively define a countably infinite set of linearly independent vectors without full choice, but I'm not sure if that is possible with ZF alone, or requires all of the Axiom of Choice, or is weaker but requires some form of choice.
Best Answer
Yes. The axiom of choice is needed in order to show that every vector space which is not finitely generated contains an infinite linearly independent subset.
The original consistency proof due to Lauchli (1962) was to construct a model in which there is a vector space that is not spanned by any finite set, but every proper subspace is finite.
Namely every collection of linearly independent vectors is finite.
If you have the axiom of dependent choice then you can actually perform the induction which you suggest and have a countably infinite set of independent vectors. But this is quite far from the full axiom of choice.
If one tries real hard, one can get away with just countable choice (which is strictly weaker than dependent choice). The argument is as follows:
Interestingly, Lauchli's example was of a space that every endomorphism is a scalar multiplication and as the above indicates this construction also contradicted $\mathsf{DC}$. In my masters thesis I showed that you can have $\mathsf{DC}_\kappa$ and still have a vector space which has no endomorphisms except scalar multiplication - even if it has relatively large subspaces.