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 &quot;hide&quot; 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.