Prove that $P \implies Q \vdash \neg Q \implies\lnot P$

Question

I'm trying to prove $$P \implies Q \vdash \neg Q \implies\lnot P$$ with natural deduction but I'm kind of stuck. I tried going from the conclusion side, which lead me to this: $$ \frac{\frac{[P] \quad \bot}{[\neg Q] \qquad \neg P \qquad(\neg E)}}{\qquad\neg Q\implies \neg P \qquad (\implies E)} $$

which is where I'm kind of stuck

Answer 1

Unfortunately, (1) I don't know of a good way of drawing proof trees in MathJax and (2) there is no universally agreed set of natural deduction rules. Here is a proof presented as a sequence of labelled steps using rules similar to those presented here.

$$\begin{align*} 1 \quad& P \Rightarrow Q & \quad & \mbox{ASM - left open} \\ 2 \quad& \lnot Q && \mbox{ASM - discharged at step 7} \\ 3 \quad& P && \mbox{ASM - discharged at step 6} \\ 4 \quad& Q && \mbox{1, 3, $\Rightarrow$-E} \\ 5 \quad& \bot && \mbox{2, 4, $\lnot$-E} \\ 6 \quad& \lnot P && \mbox{3, 5, $\lnot$-I} \\ 7 \quad& \lnot Q \Rightarrow \lnot P && \mbox{2,6, $\Rightarrow$-I} \end{align*}$$

Giving us $1 \vdash 7$, i.e., $P \Rightarrow Q \vdash \lnot Q \Rightarrow \lnot P$.

---

Here is a proof tree for the above that Graham Kemp has kindly added:

$$\sf\dfrac{\dfrac{\dfrac{\qquad\dfrac{P\to Q\quad{[P]}^2}{Q}{\small{\to}\rm E}\quad\lower{1.5ex}{{[\lnot Q]}^1}}{\bot}{\small\lnot\rm E}}{\lnot P}{\small\lnot\rm I^2}}{\lnot Q\to\lnot P\qquad}{\small{\to}\rm I^1}$$

Answer 2

(Posted after previous answer was accepted 3 hours ago)

Same proof, but this may be a little more readable format (screenshot from my proof checker):