3
$\begingroup$

I'm studying for a test and I wanted to double check some work I've done on one of the harder review questions. The question is asking me to prove the following the following contraposition:

$\lnot P \to \lnot Q \Rightarrow Q \to P$

using natural deduction system N. The rules given by the instructor include the elimination rules, the introduction rules, the contradiction rule, and the weakening rule. Here's my work, with the rules noted in parenthesis along with the line numbers used:

  1. Axiom: $\lnot P \to \lnot Q \Rightarrow \lnot P \to \lnot Q$
  2. Axiom: $\lnot P \Rightarrow \lnot P$
  3. ($\to E$ 1,2): $\lnot P, \lnot P \to \lnot Q \Rightarrow \lnot Q$
  4. Axiom: $Q \Rightarrow Q$
  5. ($\lnot E$ 3,4) $Q, \lnot P, \lnot P \to \lnot Q \Rightarrow$
  6. ($\lnot I$ 5) $Q, \lnot P \to \lnot Q \Rightarrow \lnot\lnot P$
  7. Axiom: $\lnot\lnot P \Rightarrow \lnot\lnot P$
  8. Axiom: $\Rightarrow P \lor\lnot P$
  9. Axiom: $P \Rightarrow P$
  10. Axiom: $\lnot P \Rightarrow \lnot P$
  11. ($\lnot E$ 7, 10) $\lnot\lnot P, P \Rightarrow$
  12. (C 11) $\lnot\lnot P, \lnot P \Rightarrow P$
  13. ($\lor E$ 8, 9, 12) $\lnot\lnot P \Rightarrow P$
  14. ( $\to I$, 13) $\lnot\lnot P \to P$
  15. ($\to E$ 6, 14) $Q, \lnot P \to \lnot Q \Rightarrow P$
  16. ($\to I$ 15) $\lnot P \to \lnot Q \Rightarrow Q \to P$

I'm pretty sure this is accurate, but with so many steps I'd appreciate it if there's something I missed.

$\endgroup$
  • $\begingroup$ What is rule 'C' on line 12? Is that inferring anything from a Contradiction? I.e. from $\Gamma \Rightarrow$ infer $\Gamma \Rightarrow \phi$ for any \$\phi$? $\endgroup$ – Bram28 Mar 5 '17 at 23:34
  • $\begingroup$ Yes, the C in line 12 stands for contradiction. $\endgroup$ – 009 Mar 5 '17 at 23:49
2
$\begingroup$

You have a typo on line 11, which should be:

$\neg \neg P, \neg P \Rightarrow$

But other than that everything looks fine!! I don't know system N, so I can't attest to whether or not you applied the rules defined for it correctly, but at least logically everything checks out!

$\endgroup$
  • $\begingroup$ Yeah, the instructor I have does things a bit differently from the other discrete math teachers at my campus. $\endgroup$ – 009 Mar 5 '17 at 23:50

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.