Among hundreds of equivalent definitions of amenability (for discrete, countable, groups), I would like to discuss two which are most common:

A1. A group $G$ is amenable if it admits a Folner sequence.

A2. A group $G$ is amenable if it admits an invariant mean.

(See e.g. http://en.wikipedia.org/wiki/Amenable_group or http://terrytao.wordpress.com/2009/04/14/some-notes-on-amenability/)

However, proofs of equivalence that I know (even for $G={\mathbb Z}$) require either axiom of choice or, at least, existence of a nonprincipal ultrafilter on ${\mathbb N}$.

Question: Is there a proof that A1 $\iff$ A2 which uses only ZF axioms? Or, maybe $A1\iff A2$ implies existence of nonprincipal ultrafilters, maybe in a weakened form?

This question was discussed a bit in Why are abelian groups amenable? and Why groups that admit Folner Sequences are amenable but not in the above form.

Note: I am not a logician, but a geometric group-theorist and I frequently use ultrafilters. As the result I am often asked if the results could be proven without ultrafilters. For most proofs my answer usually is: "Yes, if you work much harder and write ugly and long proofs." However, I do not know the answer in the context of amenable groups.