0
$\begingroup$

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?

$\endgroup$
0
$\begingroup$

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

$\endgroup$
  • $\begingroup$ 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? $\endgroup$ – Oscar Jul 10 '18 at 17:54
  • $\begingroup$ @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. $\endgroup$ – Bram28 Jul 10 '18 at 19:13
  • $\begingroup$ I apologize- that last step is clear. I just needed some time to think about it. $\endgroup$ – Oscar Jul 10 '18 at 19:46
0
$\begingroup$

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

$\endgroup$

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.