<p>I believe that the formula with the quantifier prefix you want to achieve are strictly less expressive than the two-variable logic with counting quantifiers. So there is no hope that you can translate any C2 formuale into such a form.</p>
<p>Similar types of Scott-normal forms were obtained in:</p>
<ul>
<li>Bartosz Bednarczyk, Witold Charatonik: Modulo Counting on Words and Trees. FSTTCS 2017 [for modulo-counting quantifiers but without binary predicates]</li>
<li>Michael Benedikt, Egor V. Kostylev, Tony Tan:
Two Variable Logic with Ultimately Periodic Counting. ICALP 2020 [for ultimately-periodic counting]</li>
</ul>
<p>Moreover, note that the normal form by Ian is somehow more useful than the normal form by Graedel and Otto, since under the binary encoding of numbers in the thresholds it requires an exponential blow-up (while the Ian's version can be obtained in poly-time).</p>
<p>Edit: Extended description of the above paragraph. Consider a formula <span class="math-container">$\exists^{=c} \varphi$</span> with a threshold <span class="math-container">$c$</span> encoded in binary, i.e. it means that to encode the value 1000 we need approximately <span class="math-container">$log(1000)$</span> bits rather than 1000. Hence, the value of <span class="math-container">$c$</span> is exponential in <span class="math-container">$|\varphi|$</span> rather than polynomial. In Grädel&amp;Otto approach you need to introduce a fresh binary relation for each witness of <span class="math-container">$\varphi$</span>, which increase the size of the formula exponentially (by c). The translation into Ian's normal form increases the size of the formula only polynomially.</p>
<p>You might be also interested in Gaifman's normal forms for FO extended with various kinds of counting. Here is the most recent paper, but you might check other papers by Dietrich Kuske and his co-authors:
<a href="http://eiche.theoinf.tu-ilmenau.de/kuske/Accepted/HeiKS18.pdf" rel="nofollow noreferrer">http://eiche.theoinf.tu-ilmenau.de/kuske/Accepted/HeiKS18.pdf</a></p>

CC BY-SA 4.0
2020-08-03T08:36:16.947Z
Thanks alot for the answer, and thanks for the last explanation paragraph as well ! Although you have already answered what I asked for, can you please elaborate on the last paragraph ? Why exactly is Graedel and otto reduction exponential time and not the same for Ian's version ? What does it mean to binary encode numbers in the threshold ?
SagarM
CC BY-SA 4.0
2020-08-03T12:32:25.350Z
I updated my answer.
Bartosz Bednarczyk
CC BY-SA 4.0
2020-08-01T17:38:30.460Z
2020-08-03T12:45:35.293Z
2020-08-03T12:45:35.293Z
Bartosz Bednarczyk
<p>In the paper by <a href="https://www.sciencedirect.com/science/article/pii/S0304397598003089" rel="nofollow noreferrer">[Erich Grädel and Martin Otto]</a>, the authors state that any formula in First Order Logic with two variables with counting quantifiers can be reduced to a formula of the form
<span class="math-container">$$ \forall x \forall y \alpha(x,y)\land \bigwedge_{i=1}^{m} \forall x \exists! y\beta_i(x,y)$$</span></p>
<p>Another reduction mentioned by <a href="https://www.sciencedirect.com/science/article/pii/S0890540109000637" rel="nofollow noreferrer">[Ian Pratt-Hartmann]</a> as
<span class="math-container">$$\forall x \forall y (\alpha(x,y) \lor (x \approx y)) \land \bigwedge_{1\leq h \leq m}\forall x \exists_{=c_h}y f_h(x,y) \land (x\not\approx y) $$</span></p>
<p>I am interested in these normal forms, because the reductions preserve the use of two variables only.
I would like to know whether are there other such reductions.
In particular, are there such reductions that would allow only
quantifiers of the type <span class="math-container">$\displaystyle\exists^{c}\forall$</span>,
where <span class="math-container">$c$</span> is an arbitrary counting condition?</p>

<lo.logic><first-order-logic>
Normal forms for counting quantifiers?
SagarM
# Normal forms for counting quantifiers?

(Asked by: username_0 on 2020-08-01)

In the paper by [[Erich Grädel and Martin Otto]](https://www.sciencedirect.com/science/article/pii/S0304397598003089), the authors state that any formula in First Order Logic with two variables with counting quantifiers can be reduced to a formula of the form
$$ \forall x \forall y \alpha(x,y)\land \bigwedge\_{i=1}^{m} \forall x \exists! y\beta\_i(x,y)$$

Another reduction mentioned by [[Ian Pratt-Hartmann]](https://www.sciencedirect.com/science/article/pii/S0890540109000637) as
$$\forall x \forall y (\alpha(x,y) \lor (x \approx y)) \land \bigwedge\_{1\leq h \leq m}\forall x \exists\_{=c\_h}y f\_h(x,y) \land (x\not\approx y) $$

I am interested in these normal forms, because the reductions preserve the use of two variables only.
I would like to know whether are there other such reductions.
In particular, are there such reductions that would allow only
quantifiers of the type $\displaystyle\exists^{c}\forall$,
where $c$ is an arbitrary counting condition?

**Tags:** lo.logic, first-order-logic


---

## 1 answers

### Answer by username_1 on 2020-08-01. Score: 4 | Accepted answer

I believe that the formula with the quantifier prefix you want to achieve are strictly less expressive than the two-variable logic with counting quantifiers. So there is no hope that you can translate any C2 formuale into such a form.

Similar types of Scott-normal forms were obtained in:

* username_1, Witold Charatonik: Modulo Counting on Words and Trees. FSTTCS 2017 [for modulo-counting quantifiers but without binary predicates]
* Michael Benedikt, Egor V. Kostylev, Tony Tan:
  Two Variable Logic with Ultimately Periodic Counting. ICALP 2020 [for ultimately-periodic counting]

Moreover, note that the normal form by Ian is somehow more useful than the normal form by Graedel and Otto, since under the binary encoding of numbers in the thresholds it requires an exponential blow-up (while the Ian's version can be obtained in poly-time).

Edit: Extended description of the above paragraph. Consider a formula $\exists^{=c} \varphi$ with a threshold $c$ encoded in binary, i.e. it means that to encode the value 1000 we need approximately $log(1000)$ bits rather than 1000. Hence, the value of $c$ is exponential in $|\varphi|$ rather than polynomial. In Grädel&Otto approach you need to introduce a fresh binary relation for each witness of $\varphi$, which increase the size of the formula exponentially (by c). The translation into Ian's normal form increases the size of the formula only polynomially.

You might be also interested in Gaifman's normal forms for FO extended with various kinds of counting. Here is the most recent paper, but you might check other papers by Dietrich Kuske and his co-authors:
<http://eiche.theoinf.tu-ilmenau.de/kuske/Accepted/HeiKS18.pdf>

> **Comments:**
> **username_0**: Thanks alot for the answer, and thanks for the last explanation paragraph as well ! Although you have already answered what I asked for, can you please elaborate on the last paragraph ? Why exactly is Graedel and otto reduction exponential time and not the same for Ian's version ? What does it mean to binary encode numbers in the threshold ?  
> **username_1**: I updated my answer.  

---

