三重否定除去
$ \lnot\lnot\lnot P \vdash \lnot Pのこと。
一般的に呼ばれている名前はない
名前がないと指し示しづらいので、takker.iconが勝手につけておいた
解釈
この解釈を思いつけたら面白そうだ
証明
方針
$ P\vdash\lnot\lnot Pと$ \lnot(\lnot\lnot P)\iff(\lnot\lnot P\implies\bot)を使うだけ
https://scrapbox.io/files/65d16b685a09250023130bf5.svg
code:proof.tikz(tex)
\usepackage{fitch}
\begin{document}
$\Large\begin{nd}
\hypo {1} {\lnot\lnot\lnot P}
\open
\hypo {2} {P}
\open
\hypo {3} {\lnot P}
\have {4}{\bot} \ne{2,3}
\close
\have {5} {\lnot\lnot P} \ni{3-4}
\have {6} {\bot} \ne{1,5}
\close
\have {7} {\lnot P} \ni{2-6}
\end{nd}$
\end{document}