Here is a usual proof of the statement above. (A family of elements of $X$ indexed by $I$ is a function from $I$ to $X$. Bases are families. $\operatorname{cl}(\bar{v})$ is the closure (hull) of the elements of a family $\bar{v}$.)
Theorem. Let $V$ be a linear space over a field $K$. For every family $\bar{v}$ of elements of $V$ indexed by a finite set $I$, there is a set $J\subseteq I$ such that $\bar{v} \mathbin{\upharpoonright} J$ is a basis of $\operatorname{cl}(\bar{v})$.
Proof. By induction on $I$. Let $\bar{v}$ be a family of elements of $V$ indexed by a finite set $I$. If $I$ is empty, $\bar{v} \mathbin{\upharpoonright} \emptyset$ is a basis of $\operatorname{cl}(\bar{v})$. Suppose that $I$ contains an element $i$. Define $I'$ as $I\setminus \\{i\\}$. By the induction hypothesis, there is $J\subseteq I'$ such that $\bar{v} \mathbin{\upharpoonright} J$ is a basis of $\operatorname{cl}(\bar{v} \mathbin{\upharpoonright} I')$. $\bar{v}(i)\in \operatorname{cl}(\bar{v} \mathbin{\upharpoonright} I')$ or not (non-constructive statement).
- Suppose $\bar{v}(i)\in \operatorname{cl}(\bar{v} \mathbin{\upharpoonright} I')$. Then $\bar{v} \mathbin{\upharpoonright} J$ is a basis of $\operatorname{cl}(\bar{v})$.
- Suppose $\bar{v}(i)\not\in \operatorname{cl}(\bar{v} \mathbin{\upharpoonright} I')$. Then $\bar{v} \mathbin{\upharpoonright} (J\cup \\{i\\})$ is a basis of $\operatorname{cl}(\bar{v})$. $\square$
I prove the non-constructive statement above by the axiom of excluded middle. Trying to prove the theorem constructively, I found these special cases when it can be proved constructively.
- The operations of $V$ and $K$ and the equality of elements of $V$ and $K$ are constructive, and $K$ is finite. We can check all linear combinations of $\bar{v}$.
- The operations of $V$ and $K$ and the equality of elements of $V$ and $K$ are constructive, and $V$ has a basis $\bar{w}$ such that the operation of expressing an element of $V$ in $\bar{w}$ is constructive. $\bar{v} \subseteq \operatorname{cl}(\bar{w} \mathbin{\upharpoonright} J)$ for a finite set $J$, and $\bar{w} \mathbin{\upharpoonright} J$ induces an isomorphism from $\operatorname{cl}(\bar{w} \mathbin{\upharpoonright} J)$ to the standard linear space $J\to K$. We can decide the non-constructive statement above by working in $J\to K$ and solving the corresponding system of linear algebraic equations induced by $\bar{v}$. By the way, solving this system of linear algebraic equations gives a set $I'\subseteq I$ such that $\bar{v} \mathbin{\upharpoonright} I'$ is a basis of $\operatorname{cl}(\bar{v})$ (namely, the set of linearly independent columns of the matrix induced by $\bar{v}$). Is the proof above useful at all?
Are there other cases where the theorem can be proved constructively? Can it be proved in the general case?
The question “Find a basis of a subspace constructively” is related to mine. I discuss a more general case. Does my question contain the answer to the linked question if real numbers are replaced with computable real numbers?