# Use the rules of inference to show that if $\forall x(P(x) \lor Q(x))$ and $\forall x(\lnot P(x) \land Q(x) \to R(x))$ are true.

then $$\forall x (\lnot R(x) \to P(x))$$ is true where the domains of all quantifiers is the same.

I'm getting caught up on step 7 below.

1. $$\forall x (P(x) \lor Q(x)$$ (Premise)
2. $$P(c) \lor Q(c)$$ (Universal Instantiation from 1)
3. $$\forall x (\lnot P(x) \land Q(x) \to R(x)$$ (Premise)
4. $$\lnot P(c) \land Q(c) \to R(c)$$ (Universal Instantiation from 2)
5. $$\lnot(\lnot P(c) \land Q(c)) \lor R(c)$$ (Conditional Logical Equivalence)
6. $$P(c) \lor \lnot Q(c) \lor R(c)$$ (DeMorgan's Law)
7. $$\lnot P(c) \lor R(c)$$ (Resolution 2 and 6)

^^^ How can 7 be the results of the resolution of 2 and 6? When I try and work it out I'm left with the following:

2-a. $$Q(c) \lor P(c)$$ (Commutative Law)

6-a. $$\lnot Q(c) \lor P(c) \lor R(c)$$ (Commutative Law)

7-a. $$P(c) \lor P(c) \lor R(c)$$ (Resolution 2 and 6)

--- Continuing on can I apply the Idempotent law to 7-a?

1. $$R(c) \lor P(c)$$ (Idempotent and Commutative Laws)

2. $$\lnot R(c) \to P(c)$$ (Conditional Logical Equivalence)

3. $$\forall x (\lnot R(x) \to P(x))$$ Universal Generalization

QED.

Your reasoning in 2-a through 10 is correct.

Line 7 does not follow from 2 and 6. To see this, you can use a model theoretic approach to show that $$\neg P(c) \vee R(c)$$ is not a logical implication of $$P(c) \vee Q(c)$$ and $$P(c) \vee \neg Q(c) \vee R(c)$$.

For example, let $$$$P(c) = T\\ Q(c) = T\\ R(c) = F.$$$$ Then we have $$$$(P(c) \vee Q(c)) = T\\ (P(c) \vee \neg Q(c) \vee R(c)) = T\\ \neg P(c) \vee R(c) = F.$$$$ Thus, the conditional $$[(P(c) \vee Q(c)) \wedge (P(c) \vee \neg Q(c) \vee R(c))] \rightarrow (\neg P(c) \vee R(c))$$ is false in this model, which means that you cannot infer $$\neg P(c) \vee R(c)$$ from the other two propositions in a proof theoretic setting. Of course, this all presupposes that the logical system you are using is sound :).

You are correct, $$\lnot P(c)\lor R(c)$$ is not the result of resolution of those lines.   Fortunately it is also not what you want to obtain from the resolution.

$$\{\{p, q\},\{p,\lnot q,r\}\}$$ resolves to $$\{\{p,r\}\}$$ ...which is also $$\{\{p,\lnot\lnot r\}\}$$

Thusly, line 7 should be $$P(c)\lor R(c)$$, which is equivalent to $$P(c)\lor\lnot\lnot R(c)$$, and thus $$\lnot R(c)\to P(c)$$, as you require.

1. $$\forall x~(P(x) \lor Q(x))$$ (Premise I)
2. $$\forall x~((\lnot P(x) \land Q(x)) \to R(x)$$ (Premise II)
3. $$\quad P(c) \lor Q(c)$$ (Universal Instantiation from 1 to arbitrary $$c$$)
4. $$\quad (\lnot P(c) \land Q(c)) \to R(c)$$ (Universal Instantiation from 2)
5. $$\quad \lnot(\lnot P(c) \land Q(c)) \lor R(c)$$ (Conditional Logical Equivalence)
6. $$\quad P(c) \lor \lnot Q(c) \lor R(c)$$ (DeMorgan's Law)
7. $$\quad P(c) \lor R(c)$$ (Resolution 3 and 6)
8. $$\quad \lnot R(c)\to P(c)$$ (Conditional Logical Equivalence from 7)
9. $$\forall x~(\lnot R(x)\to P(x))$$ (Universal Generalisation, from 8 and arbitrary $$c$$)