Is there a constructive way to exhibit a basis for $\mathbb{R}^\mathbb{N}$?

Question

Assuming the Axiom of Choice, every vector space has a basis, though it can be troublesome to show one explicitly. Is there any constructive way to exhibit a basis for $\mathbb{R}^\mathbb{N}$, the vector space of real sequences?

Answer 1

"Constructively" "exhibiting" a basis for $\mathbb R^{\mathbb N}$ means "constructively" "exhibiting" a lot of linear functionals on $\mathbb R^{\mathbb N}$; one coordinate functional for each element of the basis. So, in particular, it would mean "constructively" "exhibiting" a linear functional on $\mathbb R^{\mathbb N}$ that is linearly independent of the point-evaluations. Can you "constructively" "exhibit" even one such functional? I think not.

Answer 2

This seems extremely unlikely, because if you could do this "constructively" enough to (obviously not countably) enumerate each member of the basis, you could use that enumeration to construct a well-ordering of $\mathbb{R}$ from this because we could then identify each $x \in \mathbb{R}$ with its unique final rational representation in terms of this basis.

While being able to well-order $\mathbb{R}$ is obviously a consequence of AoC, it is widely considered impossible to "constructively" give such a well-ordering.

All this is a consequence of the finiteness of our language and thus the inherent countability of everything we can describe precisely enough to "separate" each element of a set.

So the best you can get really is describing the basis as some structured collection of uncountable sets.

Edit to add that the second argument still holds if you're looking for an $\mathbb{R}$-basis, because this basis would need to be uncountable as well.

An easy way to see this is considering $\{(n^x)_{n \in \mathbb{N}}:x \in \mathbb{R}^+\}$ - this is an uncountable and $\mathbb{R}$-linearly independent set in $\mathbb{R}^\mathbb{N}$.

Answer 3

Assume that every set of real numbers has the Baire property, as well the axiom of dependent choice (it is true if we assume AD, or live in Solovay's model but we can get away with less than large cardinals too):

Since every set of $\mathbb R^\mathbb N$ has the Baire property, and $\mathbb R^\mathbb N$ is a Polish group, every homomorphism of it into itself is continuous [1, Th. 9.10].

Given a Hamel basis has to have cardinality $\frak c$, it defines $2^\frak c$ many endomorphisms of $\mathbb R^\mathbb N$.

Now, given that $\mathbb R^\mathbb N$ is a separable space (by rational sequences which are eventually zero) this means that a continuous function is defined uniquely on the countable dense set, in particular this implies that we can only have $\frak c$ many continuous functions from $\mathbb R^\mathbb N$ to itself.

Contradiction.

---

Bibliography:

1. Kechris, A. Classical Descriptive Set Theory. Springer-Verlag, 1994.