<p>Yes. Just employ the formula <span class="math-container">$\forall{x}\forall{y} \; R(x,y) \leftrightarrow (x=y)$</span> (for a fresh binary predicate <span class="math-container">$R$</span>), which allows you to &quot;hide&quot; the equality inside the <span class="math-container">$\forall\forall$</span>-part of the Scott normal form. Then you proceed as usual.</p>
<p>EDIT: I've noticed that you wrote that <span class="math-container">$\alpha$</span> in <span class="math-container">$\forall{x}\forall{y} \; \alpha$</span> is a binary predicate. It is not true and obviously not all <span class="math-container">$\textit{FO}^2$</span> formulae are reducible to such a form. The aforementioned <span class="math-container">$\alpha$</span> 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.</p>

CC BY-SA 4.0
2020-08-12T11:38:32.200Z
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
CC BY-SA 4.0
2020-08-12T14:40:49.213Z
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).
Bartosz Bednarczyk
CC BY-SA 4.0
2020-08-12T14:46:11.487Z
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)).
Bartosz Bednarczyk
CC BY-SA 4.0
2020-08-09T07:14:19.697Z
2020-08-09T08:10:10.517Z
2020-08-09T08:10:10.517Z
Bartosz Bednarczyk
<p>As per this <a href="https://www.jstor.org/stable/421196?read-now=1&amp;seq=8#page_scan_tab_contents" rel="nofollow noreferrer">paper</a> by Grädel, Kolaitis and Moshe Vardi, they discuss computational complexity of satisfiability problem in <span class="math-container">$\mathrm{FO^2}$</span>, In order to do this they use Scott's reduction. Which is the fact that any sentence in <span class="math-container">$\mathrm{FO^2}$</span> can be reduced to Scott's Normal form in polynomial time. The Scott's Normal form is given as
<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>
Now, they also say that proving decidability for scott's reduction only proves decidability for <span class="math-container">$\mathrm{FO}^2$</span>, and then they discuss scott's class for <span class="math-container">$\mathrm{FO}^2$</span> <strong>with</strong> equality.</p>
<p>My question: Is Scott's reduction sound for <span class="math-container">$\mathrm{FO}^2$</span> <strong>with</strong> equality, i.e every sentence can be reduced to the form presented above, where <span class="math-container">$\alpha$</span> and <span class="math-container">$\beta_i$</span> are all binary predicates, it is not obvious to me from there discussion?</p>

<lo.logic><first-order-logic>
Is Scott's reduction sound for $\mathrm{FO}^2$ with equality?
SagarM
# Is Scott's reduction sound for $\mathrm{FO}^2$ with equality?

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

As per this [paper](https://www.jstor.org/stable/421196?read-now=1&seq=8#page_scan_tab_contents) 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?

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

---

## 1 answers

### Answer by username_1 on 2020-08-09. Score: 5 | Accepted answer

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.

> **Comments:**
> **username_0**: 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$ ?  
> **username_1**: 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).  
> **username_1**: 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)).  

---

