What is the best known lower bound on the number of non-equivalent first-order logic formulas of rank k with no free variables? For concreteness, we can consider the vocabulary of finite graphs.
The upper bound by doing structural induction on the definition of quantifier rank gives a non-elementary function. Do we know a non-elementary lower bound?