2
$\begingroup$
 ∃y∀x [A(x) ∧ B(y) -> C(x,y)]
 ∃y∀x [¬(A(x) ∧ B(y)) v C(x,y)]
 ∃y∀x [¬A(x) v ¬B(y) v C(x,y)]

I need to convert the above to conjunctive normal form. I'm a little confused about the order of operations in the case of both existential and universal quantifier and which part of the expression they apply to. From the last step, would I skolemize y across the entire expression meaning:

∀x [¬A(x) v ¬B(S(x)) v C(x,S(x)]

or do I take the universal quantifier first?

$\endgroup$
1
$\begingroup$

You always remove quantifiers in the order in which they appear in the prefix, from left to right, that is, you first eliminate $\exists y$ and then $\forall x$.

But the variables to apply the skolem function to are just the variables occurring free in the expression, no bound ones. Since $x$ is bound by $\forall x$, and $y$ is being skolemized away, the skolem function for $\exists y$ becomes a zero-place function symbol, or constant, S():

∃y∀x [¬A(x) v ¬B(y) v C(x,y)]
>>
∀x [¬A(x) v ¬B(S()) v C(x,S())]

In the next step, eliminate the the universal quantifier:

∀x [¬A(x) v ¬B(S()) v C(x,S())]
>>
¬A(x) v ¬B(S()) v C(x,S()).

$\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.