Is there a constructive (i.e., not using Axiom of choice, and at most Axiom of dependent choice) proof of the Banach-Alaoglu theorem in the case of separable Banach spaces? Even if it is needed assume that the dual is separable. Under even more assumptions - is there such a proof for infinite-dimensional Banach spaces.
We know such proof exists for Hahn-Banach in the separable case.
If $X$ is separable then the closed unit ball $B$ of $X^{*}$ is metrizable in the $weak^{*}$ topology. [ $d(f,g)=\sum\limits_{k=1}^{\infty} \frac 1 {2^{i}} \frac {|f(x_i)-g(x_i)|} {1+|f(x_i)-g(x_i)|}$ metrizes it if $\{x_i\}$ is dense in $X$]. Any sequence $\{f_n\}$ in $B$ has a subsequence $\{f_n'\}$ converging at each of the $x_j$'s (by a diagonal procedure). It is now fairly easy to see that if $\{x_{i_l}\}$ converges to some point $x$ then $f_n'(x_{i_l})$ is Cauchy. Call the limit $f(x)$. Obviously, $\|f\|\leq 1$. It follows that $f_n'(x_{i_l})$ converges in the weak* topology. Thus, $B$ is sequentially compact and metrizable, hence compact.