古典論理を直観主義論理に翻訳する

命題\varphiが、古典論理で証明可能なとき、かつそのときに限り、\varphi^\astは直観主義論理で証明可能

名前は揺れている

否定的翻訳

人物

論理式\varphiを否定翻訳したもの

\varphi^\astや\varphi^Nと表記する

\vdash_{CL}\varphi\leftrightarrow \varphi^*

ref 論理学の表記

変換

\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^*

関連

CPS変換との関連

参考

『論理の哲学』 p.126

p.25あたり