Normal forms for counting quantifiers?

Question

In the paper by [Erich Grädel and Martin Otto], 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] 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?

Answer 1

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:

• Bartosz Bednarczyk, 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