0
$\begingroup$

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 ?

$\endgroup$
1
  • 1
    $\begingroup$ 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$. $\endgroup$ Jan 20, 2023 at 18:57

1 Answer 1

1
$\begingroup$

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

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.