Consider a First order (FO) formula $\phi = \exists^*\forall^*\exists^* \psi$ where $\psi$ is quantifier free and function free (No n-ary functions, $n \geq 1$) matrix. I am searching for a formula (Example) in the above FO form such that the right most $\exists^*$ cannot be pulled out to the front of the given first oder formula $\phi$. In other words, there is no choice to pull the right most existential quantifier so that that the new formula be in the form of $\phi' = \exists^*\forall^*\psi$.

Consider a formula $\phi = \exists x \forall y \forall z \exists t, P(x,t) \rightarrow Q(y,z)$ and let us pull the right most $\exists t$. So, $\phi' = \exists x \exists t \forall y \forall z , P(x,t) \rightarrow Q(y,z)$. The question is whether $\phi $ and $\phi'$ equivalent? If Yes/No, then why ? What are the conditions in which we can pull the right most existential/universal quantifier so that get aligned in $\exists^*\forall^*\psi$ or $\forall^*\exists^*\psi $ form?

  • 1
    $\begingroup$ Not very clear... Forgetting about the initial $\exists$, we can consider $\forall x \exists y (x=y)$. It is clearly not equiv to $\exists y \forall x (x=y)$. $\endgroup$ Oct 3 '18 at 13:15
  • $\begingroup$ @MauroALLEGRANZA Thankyou for the response. For two quantifiers, it is intuitive and simple. But are there any rule for the pull and push of the n quantifiers. I have edited the question, as it was not clear. $\endgroup$ Oct 3 '18 at 18:17
  • $\begingroup$ @RiturajSinghRathore Just have the additional quantifiers be dummy quantifiers. Adding more quantifiers is never going to make things simpler ... $\endgroup$ Oct 3 '18 at 18:30

There are rules used to put a formula in prenex normal form that have to do with pulling out quantifiers. For example, $g \rightarrow (\forall x ~.~ f)$ is rewritten as $\forall x ~.~ g \rightarrow f$ and $(\forall x ~.~ f) \rightarrow g$ is rewritten as $\exists x ~.~ f \rightarrow g$.

(Correctness of these transformations depends on variable renaming, which is carried out before their application to guarantee that $x$ does not appear in $g$.)

The order in which the rewriting rules are applied is not fixed, so that expressions in prenex normal form with different prefixes may be derived from the same formula. These different expressions are equivalent, but some are more convenient than others when it comes to reasoning about them. (As a rule of thumb, you try to pull the existential quantifiers out first, so that your Skolem functions may be just Skolem constants.)

Consider, for example,

$$ \phi'' = (\forall x \forall t ~.~ P(x,t))) \rightarrow (\forall y \forall z ~.~ Q(y,z)) \enspace. $$

Using the two rewriting rules mentioned above, you can derive both your $\phi$ and your $\phi'$, which are therefore equivalent.


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.