否定翻訳
negatibe translation
命題$ \varphiが、古典論理で証明可能なとき、かつそのときに限り、$ \varphi^\astは直観主義論理で証明可能
名前は揺れている
否定的翻訳
人物
negative formula
論理式$ \varphiを否定翻訳したもの
$ \varphi^\astや$ \varphi^Nと表記する
$ \vdash_{CL}\varphi\leftrightarrow \varphi^*
変換
$ \varphi^*=\lnot\lnot \varphi
$ (\lnot \varphi)^*=\lnot \varphi^*
$ (\varphi\land \psi)^*=\varphi^*\land \psi^*
$ (\varphi\land \psi)^*=\lnot(\lnot \varphi^*\land \psi^*)
$ (\varphi\to \psi)^*=\varphi^*\to \psi^*
$ (\forall x\varphi)^*=\forall x\varphi^*
$ (\exist x\varphi)^*=\lnot\forall x\lnot \varphi^*
関連
参考
p.25あたり