[Math] Natural deduction proof

combinatoricslogicnatural-deduction

So i been learning about Natural deduction and i got an exam coming up on it but i just want to understand a bit more about it. So far we have learnt 4 rules and thats all we need to know.

We got :

premise
AndIntro
AndElim 
ImpIntro
Modus Ponens

Now i am just trying to understand how we go about proofing this question using those rules:

P implies (Q implies R) ` (P and Q) implies R

I have got the answer for it but i just dont get what i am suppose to be doing. Any help would be great.

The answer we have got down is :

1. P implies (Q implies R) premise
2. Assume (P and Q)
3. P AndElim to 2
4. (Q implies R) Modus Ponens to 1, 2
5. Q AndElim to 2
6. R Modus Ponens to 4, 5
7. (P and Q) impliesR ImpIntro to 2-6

But like i asked i just dont know how we got to it. An explanation of this would be great. Thanks for the help

Best Answer

In natural deduction proofs, it is good to "think ahead", and at any stage of a proof look at what you are trying to derive at that stage, and ask yourself "How can I prove that?"

So, in this case, you start with the premiss

$(P \to (Q \to R))$

and your target is to derive

$((P \land Q) \to R)$.

OK: ask what kind of proposition is that target? what is its main connective?? It's a conditional (with antecedent $(P \land Q)$ and consequent $R$). And how can you derive a conditional? Typically by using ImpIntro, yes? So the obvious thing to try is to assume the antecedent of the target and try to get to the consequent. So the proof is going to look like this ...

$(P \to (Q \to R))$

$\quad|\quad(P \land Q)$

$\quad|\quad\ldots$

$\quad|\quad R$

$((P \land Q) \to R)$.

Or at least, that's how it will look if we follow best practice and indent a proof every time we make a new assumption and finish the indented part when the assumption is "discharged" by the rule ImpIntro (i.e. the assumption is no longer in play).

So now our target is to get to $R$, and in this case we are allowed to use every above. It should be quite obvious how to do this.

But in case not, let's plod through, thinking strategically again. Where is $R$ to be found in the premisses? As the consequent of a conditional inside the consequent of a bigger conditional. How can we dig stuff out of a conditional? By modus ponens of course (what else)? How can we get to use modus ponens on a conditional? By having the antecedent to appeal to. So we need the antecedents $P$ and then $Q$ to get us to $R$. How can we get them? ... OK now you can see what to do to complete the proof for yourself!

Practice on some natural deduction examples and this kind of strategic thinking will become second nature!

For another example, let's go the other way about and try to get from the premiss

$((P \land Q) \to R)$

to the conclusion

$(P \to (Q \to R))$.

Again the conclusion is a conditional, so what do you do? You are going to use ImpIntro, so assume the antecedent and aim for the consequent:

$((P \land Q) \to R)$

$\quad|\quad P$

$\quad|\quad\ldots$

$\quad|\quad (Q \to R)$

$(P \to (Q \to R))$.

Now your aiming for the conditional $(Q \to R)$. How do you prove that? Assume the antecedent and derive the consequent of course. So let's do that ....

$((P \land Q) \to R)$

$\quad|\quad P$

$\quad|\quad|\quad Q$

$\quad|\quad|\quad\ldots$

$\quad|\quad|\quad R$

$\quad|\quad (Q \to R)$

$(P \to (Q \to R))$.

Note we have indented again, because we have a new temporary assumption in play, made while the previous one is still active. So now we need to derive $R$. How are we going to do that? Obviously we need to use the initial conditional premiss plus modus ponens. So we are going to need to derive the antecedent of that initial conditional, i,e, $(P \land Q)$. So .... we need

$((P \land Q) \to R)$

$\quad|\quad P$

$\quad|\quad|\quad Q$

$\quad|\quad|\quad\ldots$

$\quad|\quad|\quad(P \land Q)$

$\quad|\quad|\quad R$

$\quad|\quad (Q \to R)$

$(P \to (Q \to R))$.

But we are done! There is nothing more to be filled in (why?). Easy eh? The proof writes itself, if you think strategically.

Related Question