# 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$ ? – SagarM Aug 12 '20 at 11:38