1
$\begingroup$

Say I have a first-order logic formula given like this one:

$$ \forall x \exists y ( (\forall z \ P(x,z) \land Q(x,y) ) \lor (\exists g \ G( (f(x),g) )$$

Now I am interested in creating the prenex-form, which is just pulling the quantifiers from the "local scope" in to the "global scope".

Now to my problem: How do I pull out the quantifiers to the front.

In what order do I pull out the quantifiers and where do they go with respect to the existing quantifiers ?

My current understanding is that the quantifers get pushed to the right side of the preexisting quantifiers.

Also since the variables from the quantifiers are not free in any predicates I can write the above formula like this:

$$ \forall x \exists y \forall z \exists g( P(x,z) \land Q(x,y) ) \lor G( f(x),g) )$$

Is my undestanding correct ?

$\endgroup$
1
  • 1
    $\begingroup$ Start inside-out; in the formula $\forall x (\varphi(x) \lor \exists y \psi(x,y))$ the existential quant is part of the sub-formula that is the scope of the outer universal quant. Thus, in pulling it out, it must stay inside the scope of the universal quant : $\forall x \ \exists y \ (\varphi(x) \lor \psi(x,y))$. $\endgroup$
    – Mauro ALLEGRANZA
    Commented Mar 22, 2018 at 10:49

1 Answer 1

Reset to default
1
$\begingroup$

I don't understand what you mean by the quantifiers being 'pushed to the right side of the formula', but your result is indeed correct.

To clarify why this is correct:

If you have something like:

$$\forall x A(x) \lor \exists y B(y)$$

then, since $\exists y B(y)$ does not contain any free variable $x$, we can 'pull out' the $\forall x$, and thus get:

$$\forall x (A(x) \lor \exists y B(y))$$

Then, because there is no free variable $y$ in $A(x)$, we can pull out the $\exists y$ ... but where does it end up?

Well, the relevant equivalence is that where $\phi$ is some formula that does not have a free variable $v$, we have that ($Q$ is some quantifier, and $\psi$ some formula):

$$\phi \lor Qv \ \psi(v)\Leftrightarrow Qv(\phi \lor \psi(v))$$

So, applying this to the example, we have that:

$$A(x) \lor \exists y B(y) \Leftrightarrow \exists y (A(x) \lor B(y))$$

And applying this equivalence to the larger $\forall (A(x) \lor \exists y B(y))$, we thus get:

$$\forall x (A(x) \lor \exists y B(y)) \Leftrightarrow \forall x \exists y (A(x) \lor B(y))$$

$\endgroup$
4
  • $\begingroup$ I was just about to ask about the full formula but you already edited your post, confirming my assumptions. Thanks for taking the time to answer and explain. Btw I have edited my post to make more sense about pushing the quantifiers $\endgroup$
    – zython
    Commented Mar 22, 2018 at 11:49
  • $\begingroup$ @zython Ah, yes, your edit makes sense! Yes, that's exactly it. Glad I could help! :) $\endgroup$
    – Bram28
    Commented Mar 22, 2018 at 13:29
  • $\begingroup$ and ∀x∃y(A(x)∨B(y)) is equivalent to ∃y∀x(A(x)∨B(y)) since we could have first taken out the right side. $\endgroup$
    – user56834
    Commented Oct 3, 2018 at 15:14
  • $\begingroup$ and ∀x∃y(A(x)∨B(y)) is equivalent to ∃y∀x(A(x)∨B(y)) since we could have first taken out the right side. $\endgroup$
    – user56834
    Commented Oct 3, 2018 at 15:15

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .