Prove an entailment is not true via resolution.

Question

Given an entailment $\Sigma ⊨ S$ that I want to prove is false, if I want to prove it with resolution, do I just prove $¬ (\Sigma \implies S)$ instead? If not, how can I do it, still using resolution refutation?

Answer 1

Careful!

$\Sigma$ is a set of statements ... it makes little sense to make that part of a logic statement.

Consider:

$\Sigma = \{ P \}$

$S = Q$

Then $\neg ( \Sigma \Rightarrow S)$ would be $\neg ( \{ P \} \Rightarrow S)$?!?

OK, but I assume that by '$\neg ( \Sigma \Rightarrow S)$' you mean the statement that you obtain by the negating the conditional, whose antecedent is the conjunction of all statements in $\Sigma$, and whose consequent is $S$. So, in this case that would be $\neg(P \Rightarrow Q)$

(BTW: I am assuming that you use the $\Rightarrow$ as the truth-functional operator called the material implication, rather than as the meta-logical symbol for logical implication ... for otherwise $\neg ( \Sigma \Rightarrow S)$ would already make little sense, as it would be trying to use a meta-logical operator inside a logic expression)

OK, but consider. Using the same $\Sigma$ and $S$ as defined:

It is clear that it is not the case that $\{ P \} \vDash Q$, and hence it is not true that $\Sigma \vDash S$

But it is also not the case that $\neg(P \Rightarrow Q)$, and hence it is not true that '$\neg ( \Sigma \Rightarrow S)$'

So no, you can't prove that some logical entailment does not hold by trying to prove the negation of its corresponding conditional.

Answer 2

To prove $\Sigma\vDash S$ by resolution, show that the CNF clausal form of $\Sigma\cup\{ \neg S\}$ can be resolved down to emptiness (ie, that the union cannot be satisfied).

Eg: $p, p\to (q\vee r), r\to q\vDash q$ is proven by resolving $$\{(p), (\neg p,q,r),(\neg r,q),(\neg q)\}\\\{(q,r),(\neg r,q),(\neg q)\}\\\{(q),(\neg q)\}\\\{\}$$