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

• I suggest you replace $\mathbb R$ by $\mathbb Q$, since the problem of non-constructivity also appears in the latter case (while the former comes with its own set of worms, such as: which of the many definitions of $\mathbb R$ are you using, and does any of them make it a field?). Mar 24, 2019 at 17:45
• This said, I agree with your impression that subspaces (in the finite-dimensional case) are constructed as spans, kernels, intersections, sums and similar fairly algorithmizable constructions, and so it should be possible to treat them as discrete things rather than as types. Something similar is done for polyhedra (even in non-constructive mathematics): They can be defined either as convex hulls (+ cones) or as intersections of finitely many halfspaces, and these are the definitions people use, as opposed to "convex subset that happens to have a mostly flat boundary" or whatever. Mar 24, 2019 at 17:47
• @darijgrinberg Good point about using the rationals. Mar 24, 2019 at 18:44
• A subspace of $\mathbb{Q}^n$ is, even constructively, juste a subspace of $\mathbb{Q}^n$ stable under the usual operation. So your "first definition". Your second definition is the definition of a finite dimensional subspace. and what you are pointing out is that constructively a subspace of a finite dimensional subspace might fail to be finite dimensional. Mar 24, 2019 at 19:52
• @LSpice Yes it was suppose to mean that "...stable under the usual operation, as your first definition. While your second definition is..." Mar 25, 2019 at 18:02

Your question almost answers itself, but this may not be so obvious. So I will try to give a short and clear answer.

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.

In intuitionistic mathematics one can easily prove that not all linear subspaces of $$\mathbb{Q}^n$$ are finitely generated.

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.

• How about “subfinite” and “subfinitely generated” subspaces which have a basis or generating set which is a subset of a finite set? Is there some place where these different notions are discussed, with examples and counterexamples? It's hard for a classically trained mathematician to keep track of the myriad of constructive notions into which a single classical one splits… Mar 25, 2019 at 17:43
• @Gro-Tsen I expect that this is all clearly covered in A course in constructive algebra by Mines, Richman and Ruitenburg. I don't have a copy myself, but I remember it being very clear and extensive on both algebra and the constructive issues involved. Mar 25, 2019 at 18:40
• Regarding 3). Is it possible to give an interesting" example of subspace that is not finitely generated? While I think I understand the example of @Gro-Tsen, it sort of feels like it goes against the spirit of being constructive since (as far as I can tell) one can't actually produce any non-zero element in the space (though the fact that I take issue with this may be my own failure to understand the philosophy). Mar 25, 2019 at 19:49
• @RBega2 i updated to answer your question, cheers frank Mar 26, 2019 at 11:52
• @RBega2: The example by Gro-Tsen is in a long constructive tradition of Brouwerian counterexamples. The constructivist idea about existence you’re thinking of isn’t so much “one should always able to produce elements”, although it’s often sloppily stated that way, but more like “being able to produce elements should be distinguished from mere non-emptiness” — and distinguishing these requires admitting that there may be non-empty/non-trivial objects in which one can’t explicitly produce elements. Mar 26, 2019 at 13:00

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.

• Nice example — but may I point out you’ve fallen back on classical habits in the phrasing “suppose there is a truth value $p$ such that $p \vee \lnot p$ is not $\top$”? As you surely know, it’s constructively provable (with no assumptions) that there is no such truth value, i.e. that excluded middle can’t fail — so a “Brouewerian counterexample” like this really does need to be phrased as “if these definitions are equivalent, then excluded middle must hold” (as you do indeed prove), not as “suppose excluded middle fails; then these definitions are inequivalent” (as you initially set it up). Mar 24, 2019 at 20:48
• Though "$p \vee \neg p$ is not $\top$" makes sense as a meta-theoretical statement, which is I believe is what is meant here. Mar 25, 2019 at 16:46
• @PeterLeFanuLumsdaine You're absolutely right, of course. I have the hardest time thinking constructively, so what I do instead is think about models (like sheaf models) in a classical ambient universe (e.g., my intuition of truth values is as open sets): this sort of phrase betrays me. I think it helps people who think like me to imagine in advance what to expect of the truth value. But feel free to edit my answer to make it constructively halal. Mar 25, 2019 at 17:38