二重否定除去と背理法は同値
https://scrapbox.io/files/67ab0548e73711f25e4eafc8.svg
逆も導ける
https://scrapbox.io/files/67ab060610104d9fb85cb8a4.svg
全然手応えのない証明だったtakker.icon
ほぼ定義を書いているようなものだった
ていうかこれただの定義じゃん
$ \lnot P:\iff(P\implies\bot)だから$ (\lnot P\implies\bot)\iff\lnot\lnot P
code:L→R.tikz(tex)
\usepackage{fitch}
\usepackage{amsmath}
\begin{document}
$\Large\begin{nd}
\open
\hypo {np} {\lnot P}
\have {b} {\bot}
\close
\have {nnp} {\lnot\lnot P} \ii{np-b}
\have {p} {P} \nne{nnp}
\end{nd}$
\end{document}
code:R→L.tikz(tex)
\usepackage{fitch}
\usepackage{amsmath}
\begin{document}
$\Large\begin{nd}
\have {nnp} {\lnot\lnot P}
\open
\hypo {np} {\lnot P}
\have {b} {\bot} \ie{nnp,np}
\close
\have {p} {P} \by{RAA}{np-b}
\end{nd}$
\end{document}