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?

1 Answer 1



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

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


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, 2020 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, 2020 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, 2020 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, 2020 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, 2020 at 23:49

You must log in to answer this question.

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