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

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 ?

• Even without a bound on the total number of distinct variables, this is a standard fact that you can find in any model theory textbook that treats Ehrenfeucht–Fraïssé games. You can prove it by induction in the quantifier rank, using the definition of rank: a formula of rank $q$ in free variables $x_0,\dots,x_{n-1}$ is a Boolean combination of formulas $\exists x_n\,\theta$ where $\theta$ is a formula of rank $q-1$ in free variables $x_0,\dots,x_n$. Jan 20 at 18:57

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$$.