# Are there amenable groups without explicit Folner sets?

This is essentially a follow-up to this previous discussion on how, in the absence of choice, the "invariant mean" and "Folner set" characterizations of amenability are no longer equivalent. Recently I've been wondering about, essentially, the opposite direction of the one in the link.

It's well known that, given an invariant mean on a group, one can deduce the existence of Folner sets. But the only proof of this that I know invokes the Hahn-Banach theorem or something similar.

This suggests that there might be groups where choice principles at least as strong as the Hahn-Banach theorem can prove that they have Folner sets, but for which one cannot prove the existence of Folner sets otherwise. In other words, groups which are support an invariant mean but for which we cannot give an explicit Folner set construction. This would be in stark contrast to the situation with, say, $\mathbb{Z}$, which has many very explicit Folner sequences but which, again, does not support an invariant mean in ZF.

Does anyone know if this can ever happen? I've tagged reverse mathematics because this seems like the sort of question its tools might be able to answer, even though it's outside of my expertise.

EDIT: as YCor points out, it obviously makes no sense without some choice to define amenable groups to be groups which support an invariant mean. "Do there exist groups with solvable word problem which support an invariant mean without a computable Folner sequence" would certainly be a good specification of my question.

• Without choice, defining amenable groups as groups with an invariant mean is ridiculous. A mean is a typically "choice" object, never explicit. Existence of Følner approximations, or their $\ell^p$-analogues (more robust) are reasonable definitions. – YCor Apr 3 '18 at 16:41
• Anyway there's a reasonable interpretation of the question, unrelated to AC. Namely given say a finitely generated group, say with solvable word problem (if infinite, this means we consider $\mathbf{N}$ with a computable group law), if amenable does there exist an computable Følner sequence? – YCor Apr 3 '18 at 16:43
• @BigM No they're well-known (and easy to construct) for $ax+b$ (and for all connected amenable Lie groups), although balls are not Følner. In coordinates $\mathbf{R}\rtimes\mathbf{R}$, something such as $\{(x,t):|x|\le 2^n:|t|\le n\}$ works. – YCor Apr 3 '18 at 17:05
• @YemonChoi there's something trivial, namely that groups of subexponential growth have some extracted sequence of balls that are Følner. I don't know more on this and specialists have thought about the question; I can't say more. – YCor Apr 3 '18 at 20:19
• Actually the specification has a negative answer (I found this while googling so as to find a counterexample- I actually knew this paper...): see arxiv.org/abs/1703.04133 by Matteo Cavaleri: f.g. amenable groups with solvable word problem have a computable Følner sequence. – YCor Apr 3 '18 at 21:59