In this paper Scott's reduction is discussed, which reduces any FO2 formula to Scott's Normal form. As far as I understand the reduction process explained in the paper can get you to formulas with only $\forall \forall$ and $\forall \exists$ quantification prefixes. Which has three possibilities of prefixes $\forall x \forall y $, $\forall x \exists y$ and $\exists y \forall x$. Now scott's normal form only admits $\forall x \forall y $ and $\forall x \exists y$ quantification. Then how is the explained process sound for a formula like $\exists x \forall y R(x,y) $ ?

In other words, what is the scott's reduction for $\Phi(x,y) = \exists x \forall y R(x,y)$.

My attempt on reduction according to the paper:

$ Sc( \Phi(x,y) )= \exists x P(x) \land \forall x \forall y (P(x) \leftrightarrow R(x,y)) $


Your solution is correct. It suffices to see that the formulae $\exists{y} P(y)$ and $\forall{x} \exists{y} P(y)$ are equi-satisfiable, which allows you to put your formulae in the desired form.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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