I am unsure what the difference in proof by resolution is in the following two scenarios, one being an implies, the other being an entails:
$(\exists y\forall x P(x, y)) \to (\forall x\exists y P(x, y))$
$(\exists y\forall x P(x, y)) \vdash (\forall x\exists y P(x, y))$
Do you follow the same procedure in both to prove the validity i.e negating the RHS and treat the skolemisation procedures seperately?
Thanks!
First of all, there will be a difference in the starting point. In the first case, you negate the whole conditional, while in the second case, you assert the premise and negate the conclusion.
Second, other differences may occur after that, but exactly what kind of differences will depend on the order of the steps you use to generate the clauses. For example, once you have negated the conditional in the first case:
$$\neg (\exists y \forall x \ P(x,y) \rightarrow \forall x \exists y \ P(x,y))$$
you can rewrite that as a conjunction:
$$\exists y \forall x \ P(x,y) \land \neg (\forall x \exists y \ P(x,y))$$
and now the 'smart' (and pefectly legal) move would be to simply drop the $\land$ and continue with the process with what turn out to be the same two statements that you get at the start of the second case: $\exists y \forall x \ P(x,y)$ and $\neg \forall x \exists y \ P(x,y)$
However, instead of dropping the $\land$, you can also (in fact, some algorithms at this point dictate this) pull out the quantifiers ... which involves renaming the variables ... which could (depending on the order in which you pull outthe quantifiers) end up with:
$$\exists y \forall x \exists x' \forall y' (P(x,y) \land \neg P(x',y'))$$
... and now you need to use a function $f(x)$ when skolemizing the $\exists x'$, something that could have been avoided.
Long answer short: the difference between the two cases could be trivial, but it could also be more substantial .... It depends on the order of the steps taken to generate the eventual clauses.