Constructivist defininition of linear subspaces of $\mathbb{Q}^n$? Let me preface this by saying I'm not someone who has every studied mathematical logic or philosophy of math, so I may be mangling terminology here (and the title is a little tongue in cheek).
I (and probably most of us) would define a linear subspace, $W$ of $\mathbb{Q}^n$ to be a non-empty set of vectors that is closed under vector addition and scalar multiplication.  This definition has the ``drawback" of not having a constructive (as far as I can tell) way to choose a basis of $W$.  
Alternatively, one could define a subspace $W$, of $\mathbb{Q}^n$ to just be a set which is the span of some finite collection of vectors, i.e. $W=\mathrm{span}\{ w_1, \ldots, w_N\}$.  This is a much clunkier definition (in my opinion) but does have the advantage of allowing one to construct a basis by using Gaussian elimination.  It has the ``drawback" that showing that the kernel of a matrix is a subspace is slightly non-trivial (though still constructive).
Naively, the second definition defines a smaller set of objects than the first, but it seems that in most philosophies of math they actually define the same set of objects.  
My questions: 
1) Is the second definition actually how a constructivist would define subspace?
2) Are there any system of axioms where the two definitions are really different?
3) Are there any reasons to prefer the first definition to the second definition besides taste?
This question comes out of something that always bothers me when I teach the service course in Linear Algebra.  Namely, I usually define (as does the textbook) a subspace using the first definition, but in practice only ever have students consider subspaces that are defined by the second one (or equally concretely as kernels of matrices).  Pedagogically, I sometimes wonder how much is being gained by using this first definition (as it doesn't fit in with the extremely explicit nature of the rest of the course).
Edit: Following @darijgrinberg remarks I've changed $\mathbb{R}^n$ to $\mathbb{Q}^n$.
 A: To answer question 2 (although perhaps not under a “system of axioms”), here is a simpleminded example showing that if the definitions are equivalent (even just for $n=1$), then $p\lor\neg p$ is $\top$ for any truth value $p$, i.e. the Law of Excluded Middle holds.  Given a truth value $p$ consider the subspace $\mathscr{V} = \{r\in\mathbb{Q} : (r=0) \lor p \} = \{0\} \cup \{r\in\mathbb{Q} : p\}$. Clearly this contains zero and is closed under addition and multiplication by $\mathbb{Q}$. But if $\mathscr{V}$ is the span of of a finite family $r_1,\ldots,r_m$ of elements, using the fact that each element of $\mathbb{Q}$ satisfies $(r=0) \lor\neg (r=0)$ (and proceeding by induction on $m$), either every element of the family is zero (in which case $\neg p$) or there is one which is nonzero (in which case it is invertible so $\mathscr{V}$ contains $1$, so $p$ is true).  So we have $p\lor\neg p$.
To make this perhaps more transparent, here is a sheaf model of this situation: let $X$ be a topological space, $U \subseteq X$ be an open set such that the union of $U$ and of the largest open set $\neg U$ disjoint with $U$ is not $X$.  And consider the subsheaf $\mathscr{V}$ of the constant sheaf $\mathbb{Q}_X$ (sheaf of locally constant $\mathbb{Q}$-valued functions) consisting of those locally constant $r\colon W\to\mathbb{Q}$ (for varying open $W\subseteq X$) which are identically zero outside of $U$.  This is a $\mathbb{Q}_X$-module subsheaf of $\mathbb{Q}_X$ which cannot be spanned by global sections.
Note that while my example is not spanned by a finite set $r_1,\ldots,r_m$, there is a “subfinite”(?) set $\{1 : p\}$ (meaning $\{r\in\mathbb{Q} : (r=1) \land p\}$) which spans $\mathscr{V}$ (because each element of $\mathscr{V}$, either is zero in which case it is the linear combination of the empty set, or is not zero, in which case $p$, in which case the element is the linear combination of $1$ with itself as coefficient).  I guess this set is even a basis of $\mathscr{V}$, though I'm not sure there aren't many subtly inequivalent definitions.
A: Your question almost answers itself, but this may not be so obvious. So I will try to give a short and clear answer.
Regarding 1) of your question:
As a mathematician well-schooled in intuitionistic and constructive mathematics, I would always consider more than one constructive notion of 'linear subspace'.
Your first definition is definitely my favourite for the purest definition. So I would say: $(A,+,\cdot, k)$ is a linear subspace of $(V, +,\cdot, k)$ iff $A\subseteq V$ is closed under addition and scalar multiplication.  
Important extra features would be to say that $(A,+,\cdot, k)$ is a finitely generated linear subspace iff there are $a_1,\ldots,a_n$ in $A$ such that $A=\mathrm{span}\{a_1,\ldots,a_m\}$, and a finite-dimensional linear subspace iff there is a basis $(a_1,\ldots,a_m)$ of $A$. 
For $\mathbb{Q}^n$, any finitely generated linear subspace is a finite-dimensional linear subspace, since the equality of elements is decidable on $\mathbb{Q}^n$. But this does not hold for $\mathbb{R}^n$, and so for $\mathbb{R}^n$ we can have a finitely generated subspace which is not provably finite-dimensional. Brouwer gave many examples of such situations.
Regarding 2) of your question:
In intuitionistic mathematics one can easily prove that not all linear subspaces of $\mathbb{Q}^n$ are finitely generated.
Regarding 3) of your question:
Yes, there is a reason to favour your first definition over the second, because in many constructive situations we do not explicitly have a finite set of generators, and still we can do a lot of worthwhile stuff with an $A$ which is closed under addition and scalar multiplication.

[update to reflect the comments below:]
As an indication of constructive situations where linear subspaces of $\mathbb{Q}^2$ which are 'not' finitely generated occur, let me give the following example (a bit contrived to keep it simple, but in higher math these situations are commonplace).
For $\alpha$ in $\{0,1\}^{\mathbb{N}}$  define $V_{\alpha}=\{(0,0)\}\cup\{r\cdot (0,1)\mid r \in\mathbb{Q}\mid \exists n\in\mathbb{N}[\alpha(n)=1]\}$.
Now for an arbitrary $\alpha$ the assertion that $V_{\alpha}$ is finitely generated implies that $\alpha=\underline{0}$ or $\alpha\neq\underline{0}$. We cannot constructively assert the latter for all $\alpha$ in $\{0,1\}^{\mathbb{N}}$, so if we want to prove something for all $V_{\alpha}$ we are stuck with 'non-finitely generated' linear subspaces of $\mathbb{Q}^2$. And in many situations like this often only the closedness of $V_{\alpha}$ under addition and scalar multiplication is necessary to produce a nice general theorem.
