How to prove that an existence statement cannot be constructive Given the well known spaces of sequences:
 $$
l_\infty =\{(x_n), n\in \mathbb{N}, x_n \in \mathbb{R} : \sup_n |x_n|<\infty\}
$$
$$
l_1= \{(x_n), n\in \mathbb{N}, x_n \in \mathbb{R} : \sum_n |x_n|<\infty\}
$$
we can prove, by Hahn-Banach theorem, that $l_1\subsetneqq( l_\infty)^*$, where $( l_\infty)^*$ is the dual space of $ l_\infty$. But it seems that it's impossible to show explicitly an element of $( l_\infty)^*/l_1$. 
Here I found that "it is impossible for an explicit example to be constructed", but there is not a proof of this statement. 
I found the same statement also here, but again without proof.
I tried to find a proof but it's too hard for me. Someone can give me a sketch of the proof, or indicate an accessible source where I can find such proof?
I'm interested to this question because it's connected with that Do we really need reals?, being an example of a non constructive existence theorem with an explicit proof of the fact that a constructive approach is impossible. Some one know other similar results?
 A: The answer is given in both your sources, in the second one more explicitly. Shelah showed that, assuming ZF is consistent, ZF cannot prove that $(\ell^\infty)^\ast \neq \ell^1$. In particular, some non-constructive methods are needed to separate $(\ell^\infty)^\ast$ from $\ell^1$. Shelah's result is even stronger: even ZF+DC cannot prove that $(\ell^\infty)^\ast \neq \ell^1$ (Dependent Choice is a weak form of AC).
Here ZF is Zermelo–Fraenkel, the usual constructive set of axioms used for set theory. The non-constructive Axiom of Choice is also usually assumed, and it implies in particular the Hahn–Banach theorem, which in turn shows that $(\ell^\infty)^\ast \neq \ell^1$. Without AC, however, the Hahn–Banach theorem cannot be proved, as Shelah's result shows. Shelah proved his result by constructing a model of ZF+DC in which $(\ell^\infty)^\ast = \ell^1$. The exact paper of Shelah is probably referenced in Schechter's book Handbook of Analysis and its Foundations, but it might prove to be too technical for you (or me).
