I am trying to answer Question 3(e) in Exercise 1.2 of Huth and Ryan's Logic in Computer Science book for revision and I am stuck on it. The question asks you to prove the validity of the following sequent:

$\neg(P \to Q) \vdash Q \to P$

Any help would be appreciated.

  • $\begingroup$ Can you prove it informally? $\endgroup$ – Git Gud May 26 '16 at 8:41
  • $\begingroup$ I can understand why it makes sense informally, but I have no idea how to actually write that out formally $\endgroup$ – lessthanmediocre May 26 '16 at 8:44
  • $\begingroup$ OK. Here's an idea. You start by assuming the LHS holds, then start a subproof with $Q$ as a premise. From here my hint is this: prove $P\to Q$ within this subproof. $\endgroup$ – Git Gud May 26 '16 at 8:46
  • 1
    $\begingroup$ That's fine. Now maybe change your name to atleastmediocre and find alternative proofs. It's unlikely that the informal proof you had in mind looks like this. Try to formalize the informal proof you thought of. $\endgroup$ – Git Gud May 26 '16 at 9:27
  • 1
    $\begingroup$ @DougSpoonwood Your alternative totally escaped me. Now it's natural to me too. $\endgroup$ – Git Gud Sep 24 '16 at 14:26

1) $\lnot (P \to Q)$ --- premise

2) $Q$ --- assumed [a]

3) $P \to Q$ --- from 2) by $\to$-intro

4) $\bot$ --- contradiction from 1) and 3)

5) $P$ --- from 4) by $\bot$-eim

6) $Q \to P$ --- from 2) and 5) by $\to$-intro, discharging [a].


Following the nomenclature as demonstrated in the solutions of your book (this particular question is not included, so this is not plagiarism):

1. ¬(P→Q)  assumption
  2. Q     assumption
    3. P   assumption
    4. Q   copy 2
  5. P→Q   →i 3-4
  6. ⊥     ¬e 5 1
  7. P     ⊥e 6
8. Q→P     →i 2-7

Where it used boxes, I used indentation. I won't draw boxes. I simply refuse to do so.


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.