# Intro Natural Deduction Problem: Given premise (p -> q) -> p show p using deduction

This is from the Daniel Bonevac Deduction text, page 122 #12.

Given premise (p -> q) -> p show p using deduction.

I can do this using made up rules on steps 4+5, not given in the book. The other steps are proper steps given in the book.

```1. (p -> q) -> p.     A
2. Show p
3. | ¬p.              AIP
4. | ¬p -> ¬(p -> q)  made up rule. take contrapositive of conditional 1
5. | ¬(p -> q).       ->E, 4, 3
6. | ¬(¬p ∨ q).       made up rule. convert conditional 5 to disjunction form.
7. | (¬p ∨ q).        ∨I, 3
```

We've only covered conjunction exploitation/introduction, negation exploitation/introduction, indirect proof, reiteration, conditional exploitation, conditional proof, biconditional exploitation/introduction.

The fundamental rules covered:

```&E: Conjunction Exploitation
&I: Conjunction Introduction
¬¬: Negation introduction/exploitation
AIP: Indirect Proof (Show p, then assume ¬p, derive contradiction, conclude and cancel Show)
R: Reiteration
->E: Conditional Exploitation
ACP: Conditional Proof (Show p->q, assume p, derive q, conclude and cancel Show)
I: Biconditional introduction
E: Biconditional exploitation
```

How could the the above proof be completed using only the given rules?

Hint

Assume  ¬p and  p; we have a contradiction and derive q. Thus, by →-intro, derive (p → q), discharging assumption .

Then derive è from premise and we have a new contradiction, concluding with p by Double Negation, discharging .

Different systems have different implementations of the rules of inference (and 'exploitation' is not a common rule name), but the proof outlined above should generally look like:

`````` 1.|_ (p -> q) -> p   Premise
2.|  |_ ¬p           Assumption
3.|  |  |_ p         Assumption
4.|  |  |  |_ ¬q     Assumption
5.|  |  |  |  p      Reiteration 3
6.|  |  |  |  ¬p      Reiteration 2
7.|  |  |  q         Indirect Proof 4-5,6
8.|  |  p -> q       Conditional Introduction 3-6
.|  |  :
.|  |  :
.|  p               Indirect Proof 2-?
``````
• I don't follow the first sentence. Can you please elaborate on that? Isn't the existing proof I posted doing an indirect proof of p by assuming ¬p seeking a contradiction?
– clay
Jul 29 '20 at 21:58
• Yes, it does, @clay . But your proof used a derived rule (contraposition). Mauro suggests using only the fundamental rules - those which you have covered. Jul 29 '20 at 23:14
• @GrahamKemp, that's the question that I asked. How do I do the proof with just the fundamental rules. Mauro answered, I've read through the answer a dozen times. I don't understand exactly what he's suggesting and which fundamental rules that I'd use. That's why I asked for an elaboration.
– clay
Jul 29 '20 at 23:39
• @clay It would be easier if we knew which system you are using; different systems have different implementations of the same rule names. For instance: you have not listed a rule of explosion (aka ex falso quodlibet), so do your negation introduction/elimination rules use the falsum symbol? Jul 29 '20 at 23:43
• I don't see any rule of explosion in my text. The negation introduction/exploitation didn't use the falsum symbol. Thank you for the hints thus far.
– clay
Jul 29 '20 at 23:49