In this paper by Martin Grohe, in the first paragraph of section 4.1, it says:
"because upto logical equivalence there only exist finitely many $FO[\rho]$ formulas of quantifier rank at most $q$ and with at most $k+l$ free variables."
So in my understanding the sentence implies that given a function-free First order Logic language, with a given number of relational symbols (predicates) and a given number of variables. There are only finitely many equivalent formulas, with a fixed quantifier rank.
How can I prove this statement ? Is there constructive proof to this ? Is there a way to get an estimate of the number of formulas?
A Specially interesting case would be FO$^2$, for a given a FOL language, is it possible to write an algorithm that will generate all FO$^2$ formulas upto equivalence ?