Kuroda否定変換
メモ
Thm.1
$ \vdash_\mathsf{K} \varphi \iff \vdash_\mathsf{J}\varphi^K
ここで表記は以下．
$ \vdash_\mathsf{J}は直観主義述語論理（の任意の計算方法）で証明可能 論理式$ \varphiに対しKuroda否定変換$ Kを行った論理式を$ \varphi^Kとして表す． proof:
Thm 2のGlivenkoの定理を示せば，$ \Gamma \equiv \emptyset,\Delta \equiv \varphiとして題意が満たされる． $ \llbracket f(\tau_1,\dots,\tau_n) \rrbracket^K \equiv f(\tau_1,\dots,\tau_n)
$ \llbracket P(\varphi_1,\dots,\varphi_n) \rrbracket^K \equiv P(\llbracket \varphi_1 \rrbracket^K ,\dots,\llbracket \varphi_n \rrbracket^K)
$ \llbracket \exists_{\vec{x}}. \varphi \rrbracket^K \equiv \exists_{\vec{x}}. \llbracket \varphi \rrbracket^K
$ \llbracket \forall_{\vec{x}}. \varphi \rrbracket^K \equiv \forall_{\vec{x}}. \lnot\lnot\llbracket \varphi \rrbracket^K
$ \Gamma \vdash_\mathsf{K} \Delta \iff \lnot\Delta^K,\Gamma^K \vdash_\mathsf{J} \bot
もちろん，$ \Gamma^K \equiv {\varphi_1}^K,\dots,{\varphi_n}^Kとする．
proof:
Remark
Remark
なお，$ Kをちょっと変更した変種では，直観主義論理だけでなく最小論理にすら変換可能だということがわかっている 以下がサーベイとしてまとまっている？