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?
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).