Showing $\forall x(p(x) \land \lnot p(f(x)))$ is unsatisfiable

Question

Showing $\forall x(p(x) \land \lnot p(f(x)))$ is unsatisfiable.

So i want to use resolution . The clauses are $\{p(x)\}\ \{p(f(x))\}$ . Obviously i cannot use resolution because they use the same variable. So i have to swap out $x$ and turn it to $y$. Then i have the clauses

$\{p(y)\}\ \{p(x)\}\ \{p(f(x))\}$.

By resolving first and third clause with substitution $y/f(x)$ i get the empty clause and showed that it is unsatisfiable.

My question is, is what im saying correct and why am i allowed to swap the $x$ in $p(x)$ with a $y$. When finding the most general unifier this step is not allowed. Why is this allowed in resolution? Thanks in advance.

Answer 1

Remember that variables are just 'dummy' placeholders, and so can be replaced by any other variable, as you just did in your problem.

However, when unifying with a clause that contains multiple different variables, you don't want to replace those different variables with the same variable (e.g. you don't want to replace both $X$'s and $Y$'s with $Z$'s, or just replace the $X$'s with $Y$'s when you already have a bunch of $Y$'s), because now you are effectively saying that you need to use the same object for all those variables, and thereby unnecessarily restricting the possibilities .. meaning that you don't end up using the most general unifier.

But in your particular example you only have $1$ variable in your clause, and you can replace that $1$ variable with any other variable without losing any kind of generality.

Answer 2

If $\forall x~(p(x)\wedge\neg p(f(x))$, then $\forall x~p(x)$ and $\forall x~\neg p(f(x))$.

You express this as $\{p(x)\wedge\neg p(f(x))\}$ infers $\{p(x)\}, \{\neg p(f(x))\}$, for arbitrary values of $x$.

But if $\forall x~p(x)$ then $\forall x~p(f(x))$, which is to say: if the predicate holds for any value at all, then it holds for any value returned by the function.   So if $\{p(x)\}$ then $\{p(x)\}[x\backslash f(x)]$, or simply $\{p(f(x)\}$, holds.

So $\{p(x)\},\{\neg p(f(x))\}$ are contradictory, and we conclude that the statement cannot be satisfied.