Nonnegative linear functionals over $l^\infty$ My purpose is a clarification of the role of the axiom of choice in constructing limits for bounded sequences. Namely, we want a linear functional of norm 1 defined on the space of all bounded complex sequences that takes nonnegative sequences to nonnegative numbers. We also want that it annihilate all sequences with finite number of nonzero elements, and that it take constant sequences to the same constant. It is well known that such functionals can be realized as limits along free ultrafilters, thus the axiom of choice is needed. I would like to understand if the construction can be simplified if, instead of the ultrafilters, we allow functionals with properties as described above. Here are my questions:
Does there exist an explicit construction of such a functional? 
If not, does this mean that there are formal reasons why the explicit construction cannot exist?
Is it possible to establish the fact that the functional exists without using the axiom of choice?
Update after discussion: It is important that there are different "levels" of the axiom of choice. If I felt this better when I wrote this posting, I would also add the following question answered below in the affirmative:
Is it possible to construct the functional as desired without ultrafilters, but with using only the Hahn-Banach theorem for the space $l^\infty$?
This question looks more natural and elementary than the list of my questions, but the path sometimes gives you more than the goal. Many thanks to you all for the very helphul and interesting discussion!
 A: Note first that a positive linear functional is continuous.
There are models of ZF in which both $\ell^1$ and $\ell^{\infty}$ are reflexive and thus $\ell^1$ is the dual space of $\ell^{\infty}$. Solovay's model, the famous one in which every set of reals is measurable, has this property (see Väth's article I mention below).
This means that it is impossible to construct a functional as you want it without resorting to some sort of choice, for obviously no functional on $\ell^{\infty}$ coming from $\ell^1$ does what you want.
Note however, that all the requirements you list are fulfilled by the Cesàro limit
$$\operatorname{c{-}lim} x_k = \lim_{n \to \infty} \frac{1}{n} \sum_{k=0}^{n-1}\phantom{|} x_k$$
up to the fact that it isn't defined on all of $\ell^{\infty}$. These limits give what you want on the sequences you mention, i.e., if a sequence converges you get the usual limit (in particular it is zero for sequences of finite support and, of course, it is positive). You can consider the subspace $U$ of $\ell^{\infty}$ on which the Cesàro limit is defined. You should try and construct a bounded sequence for which the Cesàro limit doesn't exist.

As an accessible reference for constructive functional analysis I recommend E. Schechter's Handbook of analysis and its foundations. Academic Press, Inc., San Diego, CA, 1997. xxii+883 pp. ISBN: 0-12-622760-8. Don't be scared off by the somewhat uncharitable review on MathSciNet. Here's Schechter's homepage where you'll find lots of material on constructivism and the axiom of choice. 
In the paper by M. Väth, The dual space of $L^{\infty}$ is $L^{1}$, Indagationes Mathematicae
Volume 9, Issue 4, (1998), Pages 619-625, MR1691998 you'll find the justification of the second paragraph.
In Pincus, David, The strength of the Hahn-Banach theorem. Victoria Symposium on Nonstandard Analysis (Univ. Victoria, Victoria, B.C., 1972), pp. 203–248. Lecture Notes in Math., Vol. 369, Springer, Berlin, 1974. MR476512, you'll find a very detailed analysis of Hahn-Banach and its siblings. In particular it is established there that one can prove the first sentence of the second paragraph of this answer without resorting to Solovay's model and, even better, avoiding large cardinal assumptions (that are used for Solovay's model).
To answer your last question, yes you certainly don't need the full-blown axiom of choice for constructing such a linear functional, but you definitely need more than countable dependent choice and I seem to recall that the precise requirement you need is the Boolean prime ideal theorem, but I may be wrong. I'm sure that one of the competent set-theorists that are here occasionally can provide you with more information.
Edit: Here are two related MO-threads (thanks, Jonas):


*

*Explicit element of $(\ell^{\infty})^\ast - \ell^1$?

*What’s an example of a space that needs the Hahn-Banach Theorem?

Added:
Since you seem to be as interested in the existence of such a functional, you may want to visit Terence Tao's blog entry on Ultrafilters, nonstandard analysis, and epsilon management.
My favorite proof proceeds as follows:
Let $U$ be the subspace of $\ell^{\infty}$ consisting of sequences of the form $Tx - x$, where $T: \ell^{\infty} \to \ell^{\infty}$ is the shift operator $T(x_n) = (x_{n+1})$. Now prove:


*

*The constant function $1$ has distance $1$ from $U$.

*Prove that the sequences converging to zero are contained in the closure of $U$.

*By Hahn-Banach there exists a linear functional $l: \ell^{\infty} \to \mathbb{R}$ such that $l(u) = 0$ for all $u \in U$ and $l(1) = 1$.

*Prove that this implies that $l \geq 0$ and $l(Tx) = l(x)$ for all $x$ and $l(c) = \lim{c}$ for every convergent sequence $c$.


A second proof is to take $U$ be the subspace of sequences for which the Cesàro limit exists and to define $\tilde{l}: U \to \mathbb{R}$ by $l(x) = \operatorname{c{-}lim}{x}$. Now notice that $\tilde{l}{x} \leq \limsup{x_n}$ and apply Hahn-Banach to $\tilde{l}$ and the sublinear functional $\limsup$.
