I have the following formula: $\forall x \neg \forall y(p(x,y) \iff \neg \exists z(p(z,y) \land p(y,z)))$
I have to prove that it's tautology using resolution. I don't need a solution but a mere direction on how to proceed with the problem.
Thanks in advance!
First, you need to negate the statement. If you then put that into Prenex normal form and do Resolution n the clauses, and derive an mpty clause, then th statement is a tautology. Also, you can use $\neg (P \leftrightarrow Q) \equiv \neg P \leftrightarrow Q$ to work the quantifier inside.
At that point, you cannot take the $\exists z$ outside the biconditional, because you may know that if you take a quantifier outside a conditional, it changes whether the quantifier is in the antecedent or the consequent:
$P \to \forall x Q(x) \equiv \forall x (P \to Q(x))$ (quantifier in consequent: No change of quantifier)
$\forall x \ Q(x) \to P \equiv \exists x (Q(x) \to P)$ (quantifier in antecedent: Change of quantifier)
However, you can rewrite the biconditional as a conjunction of two conditionals, and then the simplest thing to do is to immediately separate the conjunction into two separate claims, and then use the Prenex laws on them. If you do keep it as 1 claim, you need to rename variables to get unique variables, for you get two quantifiers for the $z$