I'm familiar with the standard proof that there exists no $\mathbb{N}$-dimensional Banach space based on Baire: Let $\{ v_{K} : k \in \mathbb{N} \}$ be a normalized basis for $V$, and let $W_{\ell} = \mathbb{R} v_{1} + \cdots + \mathbb{R} v_{\ell}$. Then $V = \cup_{\ell \in \mathbb{N}} W_{\ell}$. Moreover, $W_{\ell}$ is closed, so $X_{\ell} = V \setminus W_{\ell}$ is open. Also, $X_{\ell}$ is dense. To show it's dense, let $v = \sum _{k = 1}^{m} r_{k} v_{k} \in V$, where $r_{m} \neq 0$. If $m > \ell$, then $v \in V \setminus W_{\ell}$. If not, let $\epsilon > 0$; then $v + \frac{\epsilon}{2} v_{\ell + 1} \in X_{\ell} \cap N(v, \epsilon)$. Baire tells us that $\cap_{\ell \in \mathbb{N}} X_{\ell}$ is dense, but it is in fact empty, a contradiction.
My question is: Can the argument be made constructively? Do we need BCT to show there exists no $\mathbb{N}$-dimensional Banach space? Can we instead make a diagonalization argument, i.e. construct a Cauchy sequence that doesn't converge in $\operatorname{span} \{ v_{k} : k \in \mathbb{N} \}$?
Perhaps further, is the result dependent on BCT? That is, does the result imply BCT?
Thanks in advance.
Pick $\epsilon = \frac1{10}$.
Pick $w_{k} \in W_{k}/W_{k-1}$ with quotient norm $\|w_k\| = 1$. Then there exists a representative $x_k \in W_k$ such that $x_k + W_{k-1} = w_k$, $\|x_k\| < 1+\epsilon$, and $\|x_k - y\| \ge 1$ for all $y \in W_{k-1}$.
Now consider $z = \sum_{k=1}^\infty 10^{-k} x_k$. We can easily show this series is Cauchy convergent, and hence converges in $X$.
In the quotient norm $X/W_n$, we get $$ \|z + W_n\| \ge 10^{-n-1} \|x_{n+1}+W_n\| - \sum_{k=n+2}^\infty 10^{-k} \|x_k+W_n\| \ge 10^{-n-1} - (1+\epsilon)10^{-n-1}/9 > 0 .$$
Hence $z \notin W_n$ for any $n \in \mathbb N$, and hence $z \notin V$.