2
$\begingroup$

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?

$\endgroup$
  • 2
    $\begingroup$ Resolution rule is simply a "generalization" of modus ponens : "from $p \to q$ and $p$, derive $q$". In classical logic, you can rewrite $p \to q$ as $\lnot p \lor q$. $\endgroup$ – Mauro ALLEGRANZA Jun 14 '18 at 17:55
  • $\begingroup$ Hint: Also, $((x\lor y)\land \neg x) \to y$ from the disjunctive syllogism. $\endgroup$ – Mr Pie Jun 15 '18 at 1:13
3
$\begingroup$

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$.

$\endgroup$
3
$\begingroup$

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.

$\endgroup$
2
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.