Can't find the prenex-normalform of a logical sentence

Question

My goal is to prenex-normalize the following sentence:

$(\exists{z} : S(z)) \wedge \exists{x} :\forall{y} : [\forall{z}: S(z) \Rightarrow P(y,z)] \Rightarrow R(x,y)$

I tried many times but none of the things that I try seem to work. I can't wrap my mind around the part between the []-brackets.

This is an exercise in a course that I take and we have a tool to check the correctness of a solution, most other exercises were no problem for me but I really struggle with this one.

Answer 1

I assume you were given the rules for pulling out the quantifiers?

In particular, the ones to pay attention to are:

$$\forall x \ \phi(x) \rightarrow \psi \Leftrightarrow \exists x (\phi(x) \rightarrow \psi)$$

$$\exists x \ \phi(x) \rightarrow \psi \Leftrightarrow \forall x (\phi(x) \rightarrow \psi)$$

In other words, when you pull a quantifier out side a conditional and where that quantifier was the antecedent of that conditional, the quantifier changes its sign.

Applied to your statement (and please allow me to add a few parentheses to make the diferent scopes a bit more clear):

$\exists z : S(z) \land \exists x : \forall y : ([\forall z : (S(z) \rightarrow P(y,z))] \rightarrow R(x,y)) \Leftrightarrow$

$\exists z : S(z) \land \exists x : \forall y : \exists z : ((S(z) \rightarrow P(y,z)) \rightarrow R(x,y)) \Leftrightarrow$

$\exists x : \forall y : \exists w : (\exists z : S(z) \land ((S(w) \rightarrow P(y,w)) \rightarrow R(x,y)) \Leftrightarrow$

$\exists x : \forall y : \exists w : \exists z :(S(z) \land ((S(w) \rightarrow P(y,w)) \rightarrow R(x,y))$

If the body needs to be put in CNF ... I assume you can do that youršelf.

Answer 2

$$\exists_1 z~ Sz \land \exists_2 x ~ \forall_3 y ~(\forall_4 z ~ Sz \to Pyz) \to Rxy$$

The fast way to do prenex: for each quantifier, Q: for every premise of a $\to$ it is in, flip it to the other quantifier type. For every $\lnot$ it is inside of, flip it to the other type.

$\exists_1$ isn't inside any $\lnot$ or $\to$, so leave it alone.

$\exists_2$ and $\forall_3$ are in the premise of the rightmost $\to$, so they get flipped.

$\forall_4$ is inside both the premise of the first $\to$ and the second $\to$, so it gets flipped twice (left alone that is).

So the result is:

$$\exists_1 z~ \forall_2 x~ \exists_3 y ~ \forall_4 z ~ \bigg(Sz \land (Sz \to Pyz) \to Rxy\bigg)$$

Note this only works when your equations are only composed of $\forall, \exists, \land, \lor, \to, \lnot$. If your equation has $\iff$ then you have to remove those first.

Answer 3

$(\exists{z} : S(z)) \wedge \exists{x} :\forall{y} : [\forall{z}: S(z) \to P(y,z)] \to R(x,y)$

The first issue is that you have two bindings for the token "$z$". Alpha replace one to a new token so that their scopes don't clash when transformed to prenex form. This is an imperative!

$(\underline{\exists{w} : S(w)}) \wedge \underline{\exists{x} :\underline{\forall{y} : [\underline{\forall{z}: S(z) \to P(y,z)}] \to R(x,y)}}$

For clarity I have underlined the nested scopes of each bound variable.   Thus making it clearer that the scope for $\forall z$ occurs as an antecedent for an implication within the scope for $\forall y$, and so we are obliged to apply the $[Q c: f(c)] \to p \iff [\overline Q c: f(c)\to p]$ rule.

$(\underline{\exists{w} : S(w)}) \wedge \underline{\exists{x} :\underline{\forall{y} : \underline{\exists{z}: [S(z) \to P(y,z)] \to R(x,y)}}}$

The relevant scopes all now contain implications but are not themselves antecedents, so now we may safely apply the $[Q_1 a:f(a)]\wedge[Q_2 b:g(b)] \iff [Q_1 a ~Q_2 b:f(a)\wedge g(b)]$ rule as often as needed. Thrice.

$\underline{\exists{w}~\underline{\exists{x}~\underline{\forall y~\underline{\exists{z} : S(w) \wedge [(S(z) \to P(y,z)) \to R(x,y)]}}}}$

And we are done.$${\exists{w}~{\exists{x}~{\forall y~{\exists{z} : S(w) \wedge \Big(\big(S(z) \to P(y,z)\big) \to R(x,y)\Big)}}}}$$