# first order logic to normal form order of operations

 ∃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?

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()).