Hilbert projection theorem without countable choice All the proofs of the Hilbert projection theorem, existence part, that I have seen so far use countable choice (usually implicitly). Is this necessary? It seems like you might be able to leverage the basic topological definition of closed, rather than the sequence convergence property used in the proof. Here's a proof sketch:
Theorem: In any complete normed vector space $V$, and given a closed subspace $A\subseteq V$ and $v\in V$, the infimum $\inf_{w\in A}|v-w|$ is attained by some $w\in A$.
Proof: Let $\delta=\inf_{w\in A}|v-w|$. Then for any $\delta'>\delta$ there is a $w\in A$ such that $|w-v|<\delta'$, so the sets $A_n=\{w\in A:|w-v|<\delta+\frac1n\}$ are nonempty. By CC, there is a sequence $(w_n)_{n\in\Bbb N}$ such that $w_n\in A_n$; then this sequence is Cauchy, and so converges to some $w\in A$ (because $A$ is closed). This point is in $\overline{A_n}$ for each $n$, and it is easy to see that $\overline{A_{n+1}}\subseteq A_n$; thus $w\in\bigcap_{n\in\Bbb N}A_n$, so $|w-v|=\delta$.
Here's an alternative proof that occurs to me, which still uses CC but for a very different reason. If $w$ is a minimizer, then $|w|\le|v|+|v-w|=|v|+\delta$, so all minimizers are in the ball of radius $|v|+\delta$ centered at the origin. Now consider the set $C=A\cap \bar B(0,|v|+\delta)$. This is a closed and (totally?) bounded subset, so by Heine-Borel (which needs CC) it is compact. The function $f:w\mapsto|v+w|$ is continuous, so the image 
$f(C)$ is also compact (as a subset of the reals). Thus it takes a minimum.
 A: It is possible to prove the Hilbert projection theorem without choice, if completeness is formulated appropriately. The usual definition of completeness in metric spaces is that every Cauchy sequence converges; but in more general settings (specifically, when the topology is not a sequential space) this does not appropriately characterize completeness, and is instead termed "sequential completeness". Since metric spaces are sequential spaces, assuming countable choice, this alternative definition reduces to the usual one under choice.
A filter $\scr F$ on $X$ is a nonempty collection of nonempty subsets of $X$ which is closed under finite intersection and superset. Given a metric $d$ on $X$, a Cauchy filter is a filter such that for all $\epsilon>0$, there is an $x$ with $B_\epsilon(x)\in\scr F$. Equivalently, for all $\epsilon>0$ there is an $A\in\scr F$ whose metric diameter is less than $\epsilon$. A filter is said to converge to $x$ if every neighborhood of $x$ is in $\scr F$.
A metric is said to be complete if every Cauchy filter converges. The following shows the relation between completeness and sequential completeness for metric spaces:
Theorem A complete metric is sequentially complete. Proof If $f:\Bbb N\to X$ is a Cauchy sequence, let $\scr F$ be the filter generated by the sets $\{f[\Bbb N^{\ge n}]:n\in \Bbb N\}$ (which is to say, the smallest filter containing the given sets). This is a proper base for a filter because it does not contain $\emptyset$ and it is closed under intersection. Since $f$ is a Cauchy sequence, for any $\epsilon$ there is an $n$ such that $d(f(i),f(j))<\epsilon$ for all $i,j\ge n$, which is to say $f[\Bbb N^{\ge n}]$ has diameter less than $\epsilon$, so $\scr F$ is Cauchy. Then if $\scr F$ converges to $x$ we have, for each neighborhood $U$ of $x$, some $n$ such that $f[\Bbb N^{\ge n}]\subseteq U$ by definition of $\scr F$, which implies that $f$ converges to $x$.
Theorem (CC) A sequentially complete metric is complete. Proof Given a Cauchy filter $\scr F$, let $(F_n)_{n\in\Bbb N}$ be a set of elements of $\scr F$ such that $|F_n|<1/n$ (where $|F_n|$ is the metric diameter of $F_n$). By taking $F_n'=\bigcap_{k\le n}F_n$ we can assume that the $(F_n)$ form a decreasing inclusion chain. Then picking $f(n)\in F_n$ for each $n$, we obtain a Cauchy sequence $f$, and any convergent point of $f$ is also a convergent point of $\scr F$. (We used CC twice in the proof, once to select $F_n$ and again to select $f(n)$.)
Turning now to the projection theorem:

Theorem In any complete normed vector space $V$, and given a closed subspace $A\subseteq V$ and $v\in V$, the infimum $\inf_{w\in A}|v-w|$ is attained by some $w\in A$.

Proof: Let $\delta=\inf_{w\in A}|v-w|$. Then for any $\delta'>\delta$ there is a $w\in A$ such that $|w-v|<\delta'$, so the sets $A_\epsilon=\{w\in A:|w-v|<\delta+\epsilon\}$ are nonempty. Let $\scr F$ be the filter generated by $\{A_\epsilon:\epsilon\in\Bbb R^+\}$. This is a Cauchy filter, so it converges to some $w\in A$ (because $A$ is closed). This point is in $\overline{A_\epsilon}$ for each $\epsilon$, and it is easy to see that $\epsilon>\epsilon'\to\overline{A_\epsilon}\subseteq A_{\epsilon'}$; thus $w\in\bigcap_{\epsilon\in\Bbb R^+}A_\epsilon$, so $|w-v|=\delta$.
This is clearly just a reformulation of the original proof; but the definition of a Cauchy filter allows us to skip all the choosing of points in the filter sets. It should be clear that joining the proof that sequentially complete implies complete with the proof of HBT for complete metrics essentially reproduces the original proof of HBT for a sequentially complete metric.
