二重否定除去
二重否定
を除去してもOK
$ \lnot\lnot \varphi \implies \varphi
古典論理
では成り立つ
直観主義論理
では成り立たない
その他
/takker/二重否定除去と背理法は同値
三重否定除去
メモ
$ \lnot \varphi
が
$ \varphi \to \bot
の糖衣構文であるという立場を取るなら
$ \lnot \lnot \varphi \to \varphi
とは実質的に
背理法
と同じである．
すなわち
$ \lnot\lnot \varphi \to \varphi = (\lnot \varphi \to \bot) \to \varphi
古典論理で成り立つが直観主義論理では成り立たないものの証明
メモ:
直観主義論理
では成り立たない．