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):
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$.
Best Answer
Some choice is needed, since it is consistent with $\mathsf{ZF}$ to have a nontrivial vector space $V$ such that $V^\ast=\{0\}$, and I'm talking about the algebraic dual here.
With choice given $e\in V$ with $e\neq 0$ it's easy to come up with a functional which is not zero on $e$: extend $\{e\}$ to a basis $\{e\}\cup\{v_i\mid i<\kappa\}$ of $V$ and define $\phi:V\to\Bbb R$ by $\phi(e)=1$ and $\phi(v_i)=0$ for every $i$. Extend by linearity to the whole space.
Note that in the context of Banach spaces we can even come up with a continuous functional which is nonzero on $e$, by using Hahn-Banach to extend the functional $\phi\colon\langle e\rangle\to\Bbb R$ given by $\phi(ae)=a$ to a bounded functional on the whole space.