Existence of a basis in constructive vector spaces As I was trying to review forgotten knowledge on Vector Spaces in
wikipedia, I read that the existence of a basis follows from Zorn
lemma, hence equivalently from the axiom of choice. Actually, the
answer to another question shows that all three are equivalent.
However, my current (amateur) interest in mathematics is oriented
towards constructive mathematics (though I could hardly say I have much
competence for it). The axiom of choice is not constructive, though
I understand that weaker versions of it, such as those proposed in
intuitionistic theories, are constructive. So I assume the same holds for other equivalent statements.
So my question is: what are constructive versions of the existence of a
basis for Vector Spaces?
To make my question more precise, following the first comments, there
could be constraints that are specifically related to the fact that
everything must be computable anyway in a constructive context.
The fact that no one has yet found a basis for the vector space of
continuous functions from $[0,1]\rightarrow \mathbb R$ does not worry
me too much, and I would not mind if existence of a basis for such a
vector space were not considered by the replacement axiom.
But I am more concerned if you consider the
same, but restricted to continuous computable function over computable
reals from $[0,1]_C\rightarrow \mathbb R_C$ (the subscript $C$ is
intended to indicate that only computable numbers are to be considered.
(though I am afraid the situation may be as bad in the computable
case). Computable reals are denumerable. And, as I understand it,
computable mathematics will have to deal only with denumerable sets.
 A: I suspect that only finite dimensional - or even just finite - vector spaces may have a fully constructive proof of existence of a basis. However in discussing "Constructive Mathematics" in general it is worth noting that there are several versions of constructive mathematics, each with different views as to what strength of axioms is supported.
In dealing with this kind of question I think that it might be useful to consider the related results in Reverse Mathematics. Now Reverse Mathematics is an explicitly classical framework, but it is based around expressing mathematical theorems using recursive functions, and higher degree recursive functions (ie Oracles) and so provides a general point of contact with questions on Constructiveness and non-Constructiveness, even although that is not its primary purpose.
Reverse Mathematics groups theorems into several increasing classes of increasing non-constructive strength. Three levels commonly encountered are $RCA_{0} < WKL_{0} < ACA_{0}$. The theorems provable in the $RCA_{0}$ class are generally constructive. Theorems provable at higher levels correspond to theorems which constructive logic would only prove under extra non-constructive assumptions. The $ACA_{0}$ class is essentially equivalent to assuming that the Halting problem can be solved. 
The theorems provable in Reverse Mathematics are theorems only stated for countable sets and languages, but the theorems provable at the $ACA_{0}$ level correspond sometimes to theorems which - stated in full ZF- generality - require the axiom of choice. An example is the following collection of theorems related to this question:
Theorem III.4.3 $ACA_{0}$ is equivalent to "Every countable vector space over a countable field has a basis".
Theorem III.4.4 $ACA_{0}$ is equivalent to "Every infinite countable vector space is either finite dimensional or contains an infinite linearly independent set".
To understand the distinction between these two theorems we note that a basis is a subset $E$ of the vector space such that each vector can be expressed as a sum of a finite subset $E_{0} \subset E$. In Set theory this would be known as a Hamel basis.
An infinite linearly independent set sometimes shortened to "basis" in the general case.
It is interesting that both forms of this this theorem have exactly the same proof strength, which is non-constructive to the same degree.
(The above theorems are from "Subsystems of second Order Arithmetic" Second Edition, by S.Simpson 2010.)
