(¬P⇒¬Q)⇒¬¬(Q⇒P)
https://scrapbox.io/files/660d43b2e8353a002306a68f.svg
code:proof.tikz(tex)
\usepackage{fitch}
\usepackage{amsmath}
\begin{document}
$\Large\begin{nd}
\hypo {pq} {\lnot P\implies\lnot Q}
\open
\hypo {nqp} {\lnot(Q\implies P)}
\open
\hypo {p} {P}
\open
\hypo {q} {Q}
\have {p2} {P} \r{p}
\close
\have {qp} {Q\implies P} \ii{q-p2}
\have {b} {\bot} \ie{nqp,qp}
\close
\have {np} {\lnot P} \ii{p-b}
\have {nq} {\lnot Q} \ie{pq,np}
\open
\hypo {q} {Q}
\have {b} {\bot} \ie{nq,q}
\have {p} {P} \be{b}
\close
\have {qp} {Q\implies P} \ii{q-p}
\have {b} {\bot} \ie{nqp,qp}
\close
\have {nnpq} {\lnot\lnot(P\implies Q)} \ii{pq-b}
\end{nd}$
\end{document}