Number of equivalent formulas in a function-free first order logic language?

Question

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 ?

Answer 1

One can prove in a quite straightforward manner an upper bound on the number of non-equivalent formulas with quantifier rank at most $q$ over a fixed finite relational vocabulary. I will sketch an argument here in the case where the vocabulary contains a single binary relation $R$ and we are allowed to use variables from the set $\{x_1,\dots,x_n\}$.

Induction is done w.r.t. quantifier rank. In the case $q = 0$ we estimate the number of non-equivalent atomic formulas. Given our assumptions, the number of such formulas is bounded by $n^2$. Suppose then that there are at most $k$ non-equivalent formulas of quantifier rank at most $q'$. Now there are at most $2k$ non-equivalent formulas of the form $\exists x_i \psi$ and $\forall x_i \psi$, where $\psi$ has quantifier rank $q'$. Any formula of quantifier rank at most $q' + 1$ is a Boolean combination of such formulas and formulas of quantifier rank at most $q'$. Up to logical equivalence, there are at most $2^{2^{2k + k}} = 2^{2^{3k}}$ such Boolean combinations (this is the number of distinct truth-tables when the number of propositional variables is $2k+k$).

This sort of calculation will give you a bound on the number of non-equivalent formulas which grows roughly like an exponential tower of height $q$.