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?



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 '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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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