# Is Scott's reduction sound for $\mathrm{FO}^2$ with equality?

As per this paper by Grädel, Kolaitis and Moshe Vardi, they discuss computational complexity of satisfiability problem in $$\mathrm{FO^2}$$, In order to do this they use Scott's reduction. Which is the fact that any sentence in $$\mathrm{FO^2}$$ can be reduced to Scott's Normal form in polynomial time. The Scott's Normal form is given as $$\forall x \forall y \alpha(x,y) \land \bigwedge_{i=1}^{m} \forall x \exists y \beta_{i}(x,y)$$ Now, they also say that proving decidability for scott's reduction only proves decidability for $$\mathrm{FO}^2$$, and then they discuss scott's class for $$\mathrm{FO}^2$$ with equality.

My question: Is Scott's reduction sound for $$\mathrm{FO}^2$$ with equality, i.e every sentence can be reduced to the form presented above, where $$\alpha$$ and $$\beta_i$$ are all binary predicates, it is not obvious to me from there discussion?

Yes. Just employ the formula $$\forall{x}\forall{y} \; R(x,y) \leftrightarrow (x=y)$$ (for a fresh binary predicate $$R$$), which allows you to "hide" the equality inside the $$\forall\forall$$-part of the Scott normal form. Then you proceed as usual.

EDIT: I've noticed that you wrote that $$\alpha$$ in $$\forall{x}\forall{y} \; \alpha$$ is a binary predicate. It is not true and obviously not all $$\textit{FO}^2$$ formulae are reducible to such a form. The aforementioned $$\alpha$$ should be a quantifier-free formula (line 13 of page 60 of the attached pdf). Maybe this is what made you problems while understanding the Scott reduction.

• Hey Bartosz, thanks for the great answer and added correction as well! Is it possible to have all $\beta_i$ such that they do not occur in $\alpha$ ? Aug 12 '20 at 11:38
• Of course, you can have such a form, e.g. \forall x \forall y (a(x) \lor b(y)) \land \forall x \exists y R(x,y) but not all FO2 formulae can be rewritten into this form (you somehow lack the ability to put any constraints on the binary relations). Aug 12 '20 at 14:40
• Writing a little bit more, in the form when betas do not appear in alpha you can always ignore them (e.g. if there is a model then there is also a model with the relations beta_i interpreted as self-loops (id relations)). Aug 12 '20 at 14:46