<p>One can prove in a quite straightforward manner an upper bound on the number of non-equivalent formulas with quantifier rank at most <span class="math-container">$q$</span> over a fixed finite relational vocabulary. I will sketch an argument here in the case where the vocabulary contains a single binary relation <span class="math-container">$R$</span> and we are allowed to use variables from the set <span class="math-container">$\{x_1,\dots,x_n\}$</span>.</p>
<p>Induction is done w.r.t. quantifier rank. In the case <span class="math-container">$q = 0$</span> we estimate the number of non-equivalent atomic formulas. Given our assumptions, the number of such formulas is bounded by <span class="math-container">$n^2$</span>. Suppose then that there are at most <span class="math-container">$k$</span> non-equivalent formulas of quantifier rank at most <span class="math-container">$q'$</span>. Now there are at most <span class="math-container">$2k$</span> non-equivalent formulas of the form <span class="math-container">$\exists x_i \psi$</span> and <span class="math-container">$\forall x_i \psi$</span>, where <span class="math-container">$\psi$</span> has quantifier rank <span class="math-container">$q'$</span>. Any formula of quantifier rank at most <span class="math-container">$q' + 1$</span> is a Boolean combination of such formulas and formulas of quantifier rank at most <span class="math-container">$q'$</span>. Up to logical equivalence, there are at most <span class="math-container">$2^{2^{2k + k}} = 2^{2^{3k}}$</span> such Boolean combinations (this is the number of distinct truth-tables when the number of propositional variables is <span class="math-container">$2k+k$</span>).</p>
<p>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 <span class="math-container">$q$</span>.</p>

CC BY-SA 4.0
2023-01-20T19:18:23.077Z
2023-01-20T19:18:23.077Z
Reijo Jaakkola
<p>In this <a href="https://arxiv.org/pdf/1701.05487.pdf" rel="nofollow noreferrer">paper</a> by Martin Grohe, in the first paragraph of section 4.1, it says:</p>
<p>&quot;because upto logical equivalence there only exist finitely many <span class="math-container">$FO[\rho]$</span> formulas of quantifier rank at most <span class="math-container">$q$</span> and with at most <span class="math-container">$k+l$</span> free variables.&quot;</p>
<p>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.</p>
<p>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?</p>
<p>A Specially interesting case would be FO<span class="math-container">$^2$</span>, for a given a FOL language, is it possible to write an algorithm that will generate all FO<span class="math-container">$^2$</span> formulas upto equivalence ?</p>

CC BY-SA 4.0
2023-01-20T18:57:47.880Z
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$.
Emil Jeřábek
<counting-complexity><first-order-logic>
Number of equivalent formulas in a function-free first order logic language?
SagarM
# Number of equivalent formulas in a function-free first order logic language?

(Asked by: username_0 on 2023-01-20)

In this [paper](https://arxiv.org/pdf/1701.05487.pdf) 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 ?

**Tags:** counting-complexity, first-order-logic
> **Comments:**
> **username_1**: 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$.  

---

## 1 answers

### Answer by username_2 on 2023-01-20. Score: 1 | Accepted answer

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


---

