Explaining the resolution rule.

Question

It is nice to have inference rules explained informally. For example, the rule of Disjunctive Syllogism $((x \lor y) \land \neg y)\rightarrow x$ can be explained as follows: since $x \lor y$ is true, so either $x$ or $y$ is true. But $y$ is false and so $x$ must be true.

I was trying to give a similar informal explanation of why the resolution rule is true but I could not come up with one: $$((x \lor y) \land (\neg x \lor z))\rightarrow (y \lor z)$$ Is there any such convincing argument?

Answer 1

One possible explanation:

Since $\neg x\vee z$ is true, so either $\neg x$ or $z$ is true.

If $z$ is true, then $y\vee z$ is true and we are done.

If not, then $\neg x$ must be true i.e., $x$ is false. But $x\vee y$ is also true and therefore it must be that $y$ is true hence again giving the truthness of $y\vee z$.

Answer 2

In classical logic, either $x$ is true or $x$ is false (tertium non datur).

In the first case, $\lnot x$ is false and hence from the hypothesis $\lnot x \lor z$ it follows that $z$ is true.

In the second case, $x$ is false and hence from the hypothesis $x \lor y$ it follows that $y$ is true.

Summing up, since one of the two cases ($x$ is true or $x$ is false) holds, then either $z$ is true or $y$ is true, i.e. $y \lor z$ is true.

Answer 3

This is vacuously true a lot, which is sort of unsatisfying. The contrapositive is tidier:

By contraposition, if both y and z are false, and since one of x, $\lnot$x is false, then the whole left hand side is false.