2
$\begingroup$

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?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
5
$\begingroup$

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.

Improve this answer
$\endgroup$
3
  • $\begingroup$ 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$ ? $\endgroup$
    – SagarM
    Aug 12, 2020 at 11:38
  • 1
    $\begingroup$ 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). $\endgroup$
    – Bartosz Bednarczyk
    Aug 12, 2020 at 14:40
  • 1
    $\begingroup$ 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)). $\endgroup$
    – Bartosz Bednarczyk
    Aug 12, 2020 at 14:46

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.