Transform a formula via prenex normal form to to Skolem normal form

first-order-logiclogicpredicate-logicproof-verification

I need to transform the expression $(\exists x \forall y \ r_1(x,g(y)) \lor \neg \forall x \ r_2(x,u))$ via prenex normal form to skolem normal form.

I have encountered prenex normal form on one occasion before, but skolem normal form is new. I will work with the definition that "In mathematical logic, a formula of first-order logic is in Skolem normal form if it is in prenex normal form with only universal first-order quantifiers."


progress so far:

\begin{align*}
&(\exists x \forall y \ r_1(x,g(y)) \lor \neg \forall x \ r_2(x,u)) & \text{(Given)}\\
\equiv \ &(\exists x \forall y \ r_1(x,g(y)) \lor \exists x \ \neg r_2(x,u)) & \text{(Negation of quantifier)} \\
\equiv \ & \exists x \ ( \forall y \ r_1(x,g(y)) \lor \neg r_2(x,u)) & \text{(a)} \\
\equiv \ & \forall y \exists x \ ( r_1(x,g(y)) \lor \neg r_2(x,u)) & \text{(b)}\\
\end{align*}

a = Since the quantifier $\exists x$ is common to all expressions, bring it to the front.

b = Since y is not a free variable in $r_2$, bring the quantifier $\forall y$ to the front

Up until now, I have tried to apply what I think I know about prenex normal form to this problem, but at this point I become quite uncertain. Could anyone help me fill in the gaps?

Best Answer

Two problems:

First, as Graham points out, going from

$$(\exists x \forall y \ r_1(x,g(y)) \lor \exists x \ \neg r_2(x,u))$$

to

$$\exists x \ ( \forall y \ r_1(x,g(y)) \lor \neg r_2(x,u))$$

is not an application of the Prenex laws

However, as it so happens, the existential does distribute over the disjunction, so you're lucky, and in fact this is a correct equivalence. But you'll have to justify it by 'Distribution of $\exists$ over $\lor$' rather than reference to Prenex laws. Or, as Graham suggests, first replace variables, and then use the Prenex Laws.

Second, going from

$$\exists x \ ( \forall y \ r_1(x,g(y)) \lor \neg r_2(x,u))$$

to

$$\forall y \exists x \ ( r_1(x,g(y)) \lor \neg r_2(x,u))$$

is a mistake. By the Prenex laws, the formula

$$\forall y \ r_1(x,g(y)) \lor \neg r_2(x,u)$$

is equivalent to:

$$\forall y ( r_1(x,g(y)) \lor \neg r_2(x,u))$$

and so, substituting that back, you get that:

$$\exists x \ ( \forall y \ r_1(x,g(y)) \lor \neg r_2(x,u))$$

is equivalent to

$$\exists x \ \forall y ( r_1(x,g(y)) \lor \neg r_2(x,u))$$

Related Question