I'm given this proof and am told to prove by deduction: $(p∨(q∧r))→(((q∧r)→p)→p)$

I have the following rules that I can use:

  • ∧ introductions and eliminations
  • ∨ introductions
  • ∨ eliminations (a case analysis where I prove each case)
  • → introductions
  • Modus Ponens
  • Modus Tollens

My issue is that I do not know what I can assume as true/where to begin assuming which parts of the proof are true.

How do I know what assumptions I can make in a given proof? Is there a procedural way to determine what is safe to assume?

  • 2
    $\begingroup$ Here's a MathJax tutorial :) $\endgroup$
    – Shaun
    Commented Sep 10, 2023 at 21:40
  • 2
    $\begingroup$ Try this. $\endgroup$
    – Shaun
    Commented Sep 10, 2023 at 21:42
  • 3
    $\begingroup$ You could use this as a guide. $\endgroup$
    – Shaun
    Commented Sep 10, 2023 at 21:44
  • 1
    $\begingroup$ Thank you @Shaun! The second link was very helpful! $\endgroup$ Commented Sep 10, 2023 at 23:32
  • 6
    $\begingroup$ Work backwards from the result you want. You want to prove something of the form $A\to B$, so your last step could be a $\to$ introduction. This means you'll have a sub-proof that assumes $A$ and proves $B$. $\endgroup$
    – Karl
    Commented Sep 10, 2023 at 23:33

2 Answers 2


Overall, this is a $ \rightarrow $ statement; that's the last operation outside of parentheses. So for a direct proof, the last step would be $ \rightarrow $ introduction. To do $ \rightarrow $ introduction, you assume $ P $ and try to derive $ Q $; if this works, then you can conclude $ P \rightarrow Q $. So you know that you're going to assume $ p \vee ( q \wedge r ) $ and try to prove $ ( ( q \wedge r ) \rightarrow p ) \rightarrow p $.

Now, the thing that you assumed is a $ \vee $ statement, so you can use $ \vee $ elimination. So now you have two tasks: assume $ p $ and prove $ ( ( q \wedge r ) \rightarrow p ) \rightarrow p $; and assume $ q \wedge r $ and prove $ ( ( q \wedge r ) \rightarrow p ) \rightarrow p $. In the second case, you can also use $ \wedge $ elimination (although as it happens, you can skip this step in this particular problem).

Meanwhile, looking at the desired conclusion, that's another $ \rightarrow $ statement. So you're going to assume $ ( q \wedge r ) \rightarrow p $ and try to prove $ p $. Exactly how you do that will be different in the two cases, but it's what you're going to try to do. You have a new assumption here, so you can analyse it using its elimination rule (which is Modus Ponens).

In this way, you work simultaneously from the top (applying elimination rules to your assumptions) and the bottom (seeking what you need in order to apply introduction rules to get your desired conclusion). These will meet in the middle; for example, at one point in this problem, in one of the cases, you should see that you have $ p $ as an assumption and also want $ p $ as a conclusion, so those connect.

This method of direct natural proof will prove anything made of $ \wedge $, $ \vee $, and $ \rightarrow $ that's valid in so-called intuitionistic logic. But there are some tautologies of classical logic (such as $ ( ( p \rightarrow q ) \rightarrow p ) \rightarrow p $, Pierce's Law) that won't work. And even in intuitionistic logic, using negation ($ \neg $) is a little more subtle. (You mentioned Modus Tollens, but this isn't the only thing that you need for $ \neg $.)

A really systematic way to handle anything in classical propositional logic, with or without $ \neg $, is to start with $ p \vee \neg p $ for every propositional variable, and do $ \vee $ elimination on all of them, then seek a direct proof in each of $ 2 ^ n $ cases. This is effectively just making a truth table, a brute force method. So a direct proof in natural deduction isn't always possible, but when it is, it's the most elegant.


Following this guide, which explains the process of writing such a proof . . .

$$\begin{array}{|lc} 1.\, p\lor(q\land r) & \text{Assumption} \\ \hline \rlap{\begin{array}{|lc} 2.\, p & \text{Assumption} \\ \hline \rlap{\begin{array}{|lc} 3.\, (q\land r)\to p & \text{Assumption} \\ \hline 4.\, p & \text{2} \end{array}}\\ 5.\, ((q\land r)\to p)\to p & \to\text{-Intro(3,4)}\\ \end{array}}\\ 6.\, p\to(((q\land r)\to p)\to p) & \to\text{-Intro(2,5)}\\ \rlap{\begin{array}{|lc} 7.\, q\land r & \text{Assumption}\\ \hline \rlap{\begin{array}{|lc} 8.\, (q\land r)\to p & \text{Assumption}\\ \hline 9.\, q\land r & \text{7}\\ 10.\, p & \text{MP(8,9)} \end{array}}\\ 11.\, ((q\land r)\to p)\to p & \to\text{-Intro(8,10)} \end{array}}\\ 12.\, (q\land r)\to(((q\land r)\to p)\to p) & \to\text{-Intro(7,11)}\\ 13.\, ((q\land r)\to p)\to p & \lor\text{-elim(1,6,12)}& \end{array}$$


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .