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

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?

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))$$

• Thanks, that clarifies the part of my question regarding prenex normal form well. Regarding skolem normal form, I still have some uncertainty. According to my definition, only universal quantification is permissible in skolem normal form. Thus, the existence of the existential quantifier in $$\exists x \ \forall y ( r_1(x,g(y)) \lor \neg r_2(x,u))$$ would indicate that further steps must be taken. Would you mind providing me some hints/literature for how to do this? Commented Jul 10, 2018 at 17:54
• @Oscar You use Skolemization (look it up) to get rid of the existentials. With the existential in front, your sentence is easily skolemized: just drop the existential and replace the variable in the formula with a constant. So, you'd get $$\forall y ( r_1(c,g(y)) \lor \neg r_2(c,u))$$ In general, when you have multiple existential quantifiers, they all need their own 'witness', which is either a constant, or a function that is a function of all the variables used in any of the unversals occurring before the existential. Again, look up Skolemization; I am sure there are examples online. Commented Jul 10, 2018 at 19:13
• I apologize- that last step is clear. I just needed some time to think about it. Commented Jul 10, 2018 at 19:46

No.   The things that exist to satisfy the predicates don't have to be the same things .   The existential quantifier are are not "in common" to both phrases so you cannot "distribute out the common factor".

For example: "There exists a number less than seven, and there exists a number greater than nine," is true, but "There exists a number that is: less than seven and greater than nine," is false. $$(\exists x~(x<7))\wedge(\exists x~(x>9))~\not\equiv ~(\exists x ~(x<7)\wedge(x>9))$$

Rather, to make it prenex you are required to use alpha-substitution on one of the bound variables before distributing.

$$(\exists x~(x<7))\wedge(\exists x~(x>9))~\equiv ~(\exists w\exists x ~(w<7)\wedge(x>9))$$