0
$\begingroup$

In Predicate Logic, if you want to prove the logical consequence using the method of resolution, do you ALWAYS start off by negating the conclusion?

$\endgroup$
1
$\begingroup$

The method works in the same way as proofs by contradiction. Suppose you have a set of assumptions $A$ and you want to prove that formula $\phi$ is a logical consequence of the formulas in $A$. One of the ways to do this is as follows.

  1. Put the negation of $\phi$ in your assumptions. So, now $A' = A\cup\{\neg\phi\}$
  2. Show that $A'$ is inconsistent. Here, this means to consecutively apply the resolution step on (appropriately chosen) formulas of $A'$, until a contradiction $(T\to F)$ is reached.

Classical logic tells you that, if (a) the initial set of assumptions $A$ is consistent and (b) $A\cup\{\neg\phi\}$ is inconsistent, then $A\cup\{\phi\}$ is consistent and you can say that $\phi$ is a logical consequence of $A$. So, if steps (1) and (2) succeed, then $\phi$ is a logical consequence of $A$.

If you don't negate the goal when you put it in the set of assumptions and if you manage to show that $A\cup\{\phi\}$ is inconsistent, then $A\cup\{\neg\phi\}$ is consistent and therefore $\neg\phi$ is a logical consequence of $A$.

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