((¬P⇒¬Q)⇒(Q⇒P))⇒二重否定除去

対偶の除去から二重否定除去を導出できる

証明

https://scrapbox.io/files/65f2a5d8c5d8da002472c66e.svg

code:proof.tikz(tex)

\usepackage{fitch}

\usepackage{amsmath}

\begin{document}

$\Large\begin{nd}

\hypo {1} {\lnot\lnot P}

\open

\hypo {2} {\lnot P}

\have {3} {\bot} \ne{1,2}

\have {4} {\lnot\lnot\lnot P} \be{3}

\close

\have {5} {\lnot P\implies\lnot\lnot\lnot P} \ii{2-4}

\have {6} {\lnot\lnot P\implies P}

\by{$(\lnot P\implies\lnot Q)\implies(Q\implies P)$}{5}

\end{nd}$

\end{document}