# Solving theorem proof with only primitive rules of logic!

I am having trouble solving the theorem proof of (P-> ~Q)->(Q->~P). I can only use primitive rules and I understand I have to use arrow introduction to introduce my antecedent, but after that I am a bit lost. Any help would be appreciated.

• What book are you using? – quasi May 16 '17 at 1:28
• logic primer by colin allen and michael hand – J.T. Kool May 16 '17 at 1:51

To Prove: $(P\to \neg Q)\to(Q\to \neg P)$

Assume $P\to\neg Q$ and $Q$, and show this implies $\neg P$ via a contradition.

Then discharge the assumptions in the right order, by two applications of implication-introduction

• I introduced P->~Q and tried to introduce P and Q by means of reductio but kept running into contradictions. – J.T. Kool May 16 '17 at 1:52
• Yes,. You are supposed to. If assuming $P$ with $P\to\neg Q$ and $Q$ infers a contradiction, then ... – Graham Kemp May 16 '17 at 2:11
• 1 1 P->~Q A->(1) then assume P with Reduction which gives me ~Q from arrow elimination then I would assume Q with Reductio which is a contradiction and I can get P from there however how am I supposed to discharge the assumption of Q out of my proof. – J.T. Kool May 16 '17 at 2:42
• When assuming $Q$ infers $\neg P$, then you have $Q\to \neg P$ by implication (arrow) introduction. This is a way to discharge the assumption. – Graham Kemp May 16 '17 at 3:53

\begin{array}{llll} 1&(1)&P \rightarrow \neg Q&A\\ 2&(2)&Q&A\\ 3&(3)&P&A\\ 1,3&(4)&\neg Q&1,3 \rightarrow E\\ 1,2&(5)&\neg P&2,4 \ RAA \ (3)\\ 1&(6)&Q \rightarrow \neg P&5 \rightarrow I \ (2)\\ &(7)&(P \rightarrow \neg Q) \rightarrow (Q \rightarrow \neg P)&6 \rightarrow I \ (1)\\ \end{array}

• Minor edit needed on line $(7)$: It should be $6 \rightarrow I \ (1)$. – quasi May 16 '17 at 3:23
• @quasi Thanks :) – Bram28 May 16 '17 at 3:37
• @Bram28 (5) is $\neg$-intro, not RAA. – Kenny Lau Sep 20 '17 at 17:32
• @KennyLau Most books would indeed call it $\neg$ Intro, but the OP uses the book 'Logic Primer', in which this rule is named RAA – Bram28 Sep 20 '17 at 19:20
• @Bram28 that is... unfortunate. – Kenny Lau Sep 20 '17 at 19:22