# 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.

• There aren't any in general. For example $C[0,1]$ The set of continuous functions from $[0,1] \rightarrow R$ is a vector space that no one has yet found a basis for. – amcalde Sep 24 '14 at 22:13
• Otherwise, if you have a finite dimensional vector space and you have a list of vectors in said space, you can use Gram-Schmidt to determine a linearly independent subset, which if you have enough elements is a basis. – amcalde Sep 24 '14 at 22:14
• There are none, because "every vector space has a basis" implies Choice. See this pdf: math.lsa.umich.edu/~ablass/bases-AC.pdf – Henry Swanson Sep 24 '14 at 22:17
• @Henry: The OP says that they are aware of this fact. – Asaf Karagila Sep 24 '14 at 22:35
• Oh shoot, somehow I missed that sentence. The question wasn't "what's a constructive proof", it's "what's a similar but constructive statement"? Well, now I just feel silly. – Henry Swanson Sep 24 '14 at 22:55

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.)

• You're obviously citing these theorems. It might be a good habit to give an actual reference. – Asaf Karagila Feb 18 '19 at 15:17
• @ Asaf Karagila Done. – Roy Simpson Feb 18 '19 at 15:31