Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

The problem is as follows: Given the premise ∀x(P (x) ∨ Q(x)) and ∀x((¬P (x) ∧ Q(x)) → R(x)) is true, use the rules of inference to show that ∀x(¬R(x) → P(x)) is also true. (The domains of all quantifiers are the same)

Now, I have a vague idea of how to do this and have the following work:

(1) ∀x(P (x) ∨ Q(x))

Premise # 1

(2) ∀x((¬P (x) ∧ Q(x)) → R(x))

Premise # 2

(3) P(a) ∨ Q(a)

Universal Instantiation on (1)

(4) ¬R(a)

(5) ¬(¬P(a) ∧ Q(a))

Universal Modus Tollens

(6) P(a) ∨¬Q(a)

Simplification of (5)

(7) P(a) ∨ P(a)

Resolution of (2) and (6)

(8) P(a)

Simplification of (7)

(9) ¬R(x) → P(x)

Assuming (4), it implies (8)

(10) ∀x(¬R(x) → P(x))

Universal Generalization of (9)

Now my main problem is how to deal with the Universal Modus Tollens in (4) and (5). Particularly how can I just say ¬R(a)? And then how do I get from ¬R(a) and P(a) to ¬R(x) → P(x)? What do I have to do to make this whole thing flow logically and correctly? Am I missing something?

share|cite|improve this question
You'll need to show the system of inference rules you're working with. – Henning Makholm Feb 4 '13 at 23:03
up vote 2 down vote accepted

I believe you'll need to use universal instantiation on $(2)$. As a universally quantified premise, you can instantiate with $\,a\,$, as you did with premise $(1)$, (since the domain of all the quantifiers is the same) then use modus tollens when you need it, applied to the instantiated statement and using the assumption $\lnot R$.

Also, as currently numbered, I think you need to justify resolution for line $(7)$ by citing $(3)$ and $(6)$ (I'm assuming you're referring to resolution to $\,P(a)\,$ given the statements $\,\left[P(a) \lor Q(a)\right]\;$ and $\left[P(a) \lor \lnot Q(a)\right].$

The key here is that you want your steps (currently numbered) $4 - 8$ indented (to designate a "sub-proof", where $(4)$ is stated as an "assumption", then $5$ follows from $(4)$ and the (soon to be) instantiated step resulting from $(2)$.

Line $(9)$ should still be a statement about the constant $a$, not $x$ as written, citing sub-proof, $(4 - 8)$ (by assuming (4), we obtain (8)), i.e. $(4)\rightarrow (8)$ given subproof $4-8$.

From $9$ to $10$ then, you are correct, as is your justification of universal generalization.

share|cite|improve this answer
Very nice indeed + 1! – Amzoti Apr 30 '13 at 1:01
You are wonderful Amy. Splendid answers are coming from all sides here. :-) I am going to be at uni. Have a nice day a head Amy. Miss you... – Babak S. Apr 30 '13 at 1:52
Hello, my friend. You are so busy, I miss you too! I hope I can catch you before you go!? (I've run out of wonderful answers from you that I can support, so I'll wait for more!) – amWhy Apr 30 '13 at 2:03

We can "streamline" a little bit the proof ...

First, forget about the quantifiers: all the premise are universally quantified and so the conclusion; thus we can remove them at the beginning (with UI) and add it at the end (with UG).

Thus, we want to prove :

$P ∨ Q, (¬P ∧ Q) → R \vdash ¬R → P$.

1) $P ∨ Q$ --- premise

2) $(¬P ∧ Q) → R$ --- premise

3) $\lnot R → \lnot (¬P ∧ Q)$ --- from 2) by Contraposition

4) $\lnot R$ --- assumed [a]

5) $\lnot (¬P ∧ Q)$ --- from 3) and 4) by Modus Ponens

6) $P \lor \lnot Q$ --- from 5) by De Morgan

7) $\lnot P$ --- assumed [b]

8) $Q$ --- from 7) and 1) by Disjunctive Syllogism

9) $\lnot Q$ --- from 7) and 6) by Disjunctive Syllogism

10) $P$ --- from 7)-9) by Negation Introduction and Double Negation, discharging [b]

11) $\lnot R \rightarrow P$ ---- from 4) and 10), discharging [a].

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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