If we there is a free ultrafilter $\mathscr U$ on $\omega$ then $$\newcommand{\Ulim}{\operatorname{{\mathscr U}-lim}}f \colon x = (x_n) \mapsto \Ulim x_n$$ defines a functional belonging to $\ell_\infty^*\setminus\ell_1$. (See, for example, my answer here and other links given there.)
Unless I am mistaken, no use of AC is needed there. So in ZF we have that existence of an ultrafilter on $\omega$ implies that $\ell_\infty^*\setminus\ell_1\ne\emptyset$. And moreover, we have a functional which extends the usual limit. We could also impose some other reasonable properties - similar to the usual limit - on $f$.
Does either of the following imply existence of an ultrafilter on $\omega$?
- $\ell_\infty^*\setminus\ell_1\ne\emptyset$.
- There exists a functional $f\in\ell_\infty^*$ which extends the usual limit.
- There exists a Banach limit, i.e., we add positivity and shift-invariance to the above properties.
The answer seems to be most likely no, but I would like to have some reference for this. And of course, various further comments, insights, related results are welcome as well.
Perhaps it is worth mentioning that if we have $f\in\ell_\infty^*$ which is multiplicative, then we can get a free ultrafilter on $\omega$, see here: Every multiplicative linear functional on $\ell^{\infty}$ is the limit along an ultrafilter.
Notice that $\mathscr U$-limit is not a Banach limit, but we can get a Banach limit from ultralimit by putting $f(x)=\Ulim \frac{x_1+\dots+x_n}n$.
I tried to have a look at some to-go references for Axiom of Choice. In Herrlich's Axiom of Choice, existence of a free ultrafilter on $\omega$ is denoted by $\mathrm{WUF}(\mathbb N)$, see Definition 2.15.
According to Theorem 4.108 in presence of dependent chocie, $\mathrm{WUF}(\mathbb N)$ is equivalent to weak ultrafilter principe $\mathrm{WUF}$ saying that each infinite set has a free ultrafilter.
I tried searching also in Howard, Rubin: Consequences of the Axiom of Choice. This book also has an accompanying website here and here which makes searching for various forms and implications between them a bit easier. Existence of a not-trivial ultrafilter on $\omega$ is listed here as Form 70.
But I found in neither of the two books anything about nontrivial functionals from $\ell_\infty^*$ or functionals extending the usual limit. (Maybe I did not look carefully enough or perhaps I missed some simple reformulation of this.) The closest thing I found was Form 52H which deals with some kind of generalized limit, but on directed sets rather than on positive integers. So this corresponds to limits of nets, not to limits of sequences. (See also: Note 31.)
This was to some extent inspired by this comment by Joel David Hamkins: "Can we use the generalized limits of $0/1$-valued sequences to produce a nonprincipal ultrafilter on $\mathbb{N}$? If so, then the answer is yes, since if ZF is consistent, then there are models of ZF with no nonprincipal ultrafilters." This comment was posted under the question Generalized limits on $\ell^\infty(\mathbb{N})$. (Although the OP did not clearly say in the post what they mean by generalized limit.)
The answer to your questions is negative as shown by Solovay and Pincus in the following paper:
Specifically in the second section they show the existence of a model in which the Hahn–Banach theorem holds, but every ultrafilter is principal (everywhere). As the Hahn–Banach theorem implies the existence of non-trivial functionals on $\ell_\infty$, it means that indeed just the existence of functionals is not enough to prove the existence of a free ultrafilter (anywhere!).
Moreover, using the Hahn–Banach theorem we can extend the usual $\lim$ functional on $c$ to a functional on $\ell_\infty$ in a continuous way.
It might be interesting to note, however, that if one considers Banach limits, then the answer is somewhat open.
We know that in models where there are Banach limits there are sets without the property of Baire; however it is open whether or not the existence of a Banach limit implies the existence of a (Lebesgue) non-measurable set. As free ultrafilters imply the existence of non-measurable sets, a positive answer in the case of Banach limits would also solve this problem.