Let $E$ be a real vector space. If $E$ has finite dimension, then for any subspace $F\subset E$ there is always some subspace $G\subset E$ such that $$E = F \oplus G$$ In infinite dimension, I know that the axiom of choice allows to construct such a $G$ for any subspace $F\subset E$. Is it possible to do without the axiom of choice when $F$ (but not $E$) is of finite dimension?
I know it is when $E$ is Hilbert. In that case, any finite-dimensional subspace $F\subset E$ is closed, therefore $F\oplus F^\perp = E$. I am wondering if there are ways to do something like this when $F$ is "nice" (e.g., finite-dimensional) in spaces more general than Hilbert spaces.
No. You can't do it.
It is consistent that for any field $F$ there is a vector space $V$ such that no proper subspace of $V$ has a direct complement. In particular for $\Bbb R$. This is based on the work of Läuchli in
In which he showed (amongst other things) that it is possible to have a vector space (over a countable field) which is not finitely generated, but every proper subspace is finitely generated. In my masters thesis I "refreshed" the argument to a broader context:
Moreover, we can do this without changing the extensional definition of $F$, so in the case of the real numbers when moving from the one universe of set theory to the one witnessing the failure, we can do it in a way that no real numbers are added.
Taking any $\lambda>\aleph_0$ ensures, if so, that $\sf DC$ holds, and therefore countable choice as well. In my Ph.D. thesis I developed a framework for iterating these sort of failures, and in November 2019 I wrote a paper showing that Läuchli's result can be iterated in a very strong way to obtain the result mentioned at the start. The framework is still under work, and I hope to prove the necessary theorems for accommodating the preservation of $\sf DC_{<\lambda}$ soon enough, and obtain the most general result.
Even if the space is a Banach space, there might not be a direct complement. For example, it is consistent with $\sf ZF$ that $\ell^\infty/c_0$ does not have any linear functionals except $0$, continuous or otherwise. In that case, if $v$ is any non-zero vector, if $\operatorname{span}(\{v\})$ had a direct complement, the projection will naturally define a linear functional.
The models witnessing this fact are models where analysis "can be developed" which means $\sf ZF+DC$ holds there. The above is a consequence of statements such as "Every set of reals is Lebesgue measurable" or "Every set of reals has the Baire property", both have been shown to be consistent without the axiom of choice (with $\sf ZF+DC$, of course), although the former requires us to assume mild large cardinal axioms are consistent as well (the latter does not).