命題論理におけるGlivenkoの定理
$ \Gamma \vdash_\mathbf{iPL} \lnot\lnot\varphi \iff \Gamma \vdash_\mathbf{cPL} \varphi
proof
次のことは使っても良いとする.
$ \Gamma \vdash_\mathbf{iPL} \varphi \implies \Gamma \vdash_\mathbf{cPL} \varphi
$ \bf iPLでは
二重否定導入:$ \vdash_\mathbf{iPL} \varphi \implies \vdash_\mathbf{iPL} \lnot\lnot\varphi 三重否定除去:$ \vdash_\mathbf{iPL} \lnot\lnot\lnot\varphi \implies \vdash_\mathbf{iPL} \lnot\varphi 二重否定分配$ \vdash_\mathbf{iPL} \lnot\lnot(\varphi \to \psi ) \leftrightarrow (\lnot\lnot\varphi \to \lnot\lnot\psi)
$ \toについて
$ \varphi \to \psi \vdash_\mathbf{iPL} \lnot\lnot\varphi \to \lnot\lnot\psi(対偶0を2回適用) $ \lnot\lnot\varphi \vdash_\mathbf{iPL} (\varphi \to \psi ) \to \lnot\lnot\psi(演繹定理を使って上手く順番を入れ替える) $ \lnot\lnot\varphi \vdash_\mathbf{iPL} \lnot\lnot(\varphi \to \psi ) \to \lnot\lnot\lnot\lnot\psi(再び対偶0を2回) $ \lnot\lnot\varphi \vdash_\mathbf{iPL} \lnot\lnot(\varphi \to \psi ) \to \lnot\lnot\psi(三重否定除去) $ \vdash_\mathbf{iPL} \lnot\lnot(\varphi \to \psi ) \to (\lnot\lnot\varphi \to \lnot\lnot\psi)(再び演繹定理を使って上手く順番を入れ替える) $ \leftarrowについて
まず次が成り立つ
$ \Gamma \vdash_\mathbf{iPL} \lnot \varphi \lor \psi \to (\varphi \to \psi)
$ \Gamma \vdash_\mathbf{iPL} \lnot(\varphi \lor \psi) \to \lnot \varphi \land \lnot \psi
これらより
$ \Gamma \vdash_\mathbf{iPL} \lnot(\varphi \to \psi) \to \lnot(\lnot \varphi \lor \psi)
$ \Gamma \vdash_\mathbf{iPL} \lnot(\lnot \varphi \lor \psi) \to \lnot\lnot \varphi \land \lnot \psi
だから繋いで$ \Gamma \vdash_\mathbf{iPL} \lnot(\varphi \to \psi) \to \lnot\lnot \varphi \land \lnot \psiとなる.
$ \Gamma \vdash_\mathbf{iPL} (\lnot\lnot\varphi \to \lnot\lnot\psi) \to \lnot(\varphi \to \psi) \to \lnot\lnot \psi \land \lnot \psi
$ \Gamma \vdash_\mathbf{iPL} (\lnot\lnot\varphi \to \lnot\lnot\psi) \to \lnot(\varphi \to \psi) \to \bot
$ \Gamma \vdash_\mathbf{iPL} (\lnot\lnot\varphi \to \lnot\lnot\psi) \to \lnot \lnot(\varphi \to \psi)
よってOK
$ \impliesについて
$ \Gamma \vdash_\mathbf{iPL} \lnot\lnot\varphi \implies \Gamma \vdash_\mathbf{cPL} \lnot\lnot\varphiであるから二重否定除去より直ちに得られる. $ \impliedbyについて
モーダスポネンスの場合
$ \Gamma \vdash_\mathbf{cPL} \psi \to \varphiかつ$ \Gamma \vdash_\mathbf{cPL} \psiで$ \Gamma \vdash_\mathbf{cPL} \varphiだったとする.
帰納法の仮定より
1. $ \Gamma \vdash_\mathbf{iPL} \lnot\lnot(\psi \to \varphi)
2. $ \Gamma \vdash_\mathbf{iPL} \lnot\lnot \psi
1.と二重否定分配より$ \Gamma \vdash_\mathbf{iPL} \lnot\lnot\psi \to \lnot\lnot\varphiが成り立つ.
よってモーダスポネンスより$ \Gamma \vdash_\mathbf{iPL} \lnot\lnot \varphiが言える.OK
まず次の事実が非常に便利な補題である.
排中律:$ \Gamma \vdash_\mathbf{cPL} \varphi \lor \psiの場合
$ \Gamma \vdash_\mathbf{iPL} \lnot\lnot(\varphi \lor \psi)を示せば良い
一般に$ \Gamma \vdash_\mathbf{iPL} \lnot(\varphi \lor \psi) \to \lnot \varphi \land \lnot \psiが成り立つ.
具体例として$ \Gamma \vdash_\mathbf{iPL} \lnot(\varphi \lor \lnot \varphi) \to \lnot \varphi \land \lnot \lnot \varphiが成り立つ
ところで$ \Gamma \vdash_\mathbf{iPL} \lnot\varphi \land \lnot\lnot\varphi \to \botだから
$ \Gamma \vdash_\mathbf{iPL} \lnot(\varphi \lor \lnot \varphi) \to \bot,すなわち$ \Gamma \vdash_\mathbf{iPL} \lnot\lnot(\varphi \lor \lnot \varphi)
二重否定除去:$ \Gamma \vdash_\mathbf{cPL} \lnot\lnot\varphi \to \varphiの場合
$ \Gamma \vdash_\mathbf{iPL} \lnot\lnot(\lnot\lnot\varphi \to \varphi)を示せば良い
一般に$ \Gamma \vdash_\mathbf{iPL} (\lnot\lnot \varphi \to \lnot\lnot\psi) \to \lnot\lnot(\varphi \to \psi)が成り立つ
まず次が成り立つ.
$ \Gamma \vdash_\mathbf{iPL} \lnot \varphi \lor \psi \to (\varphi \to \psi)
$ \Gamma \vdash_\mathbf{iPL} \lnot(\varphi \lor \psi) \to \lnot \varphi \land \lnot \psi
上参照
$ \Gamma \vdash_\mathbf{iPL} \lnot(\varphi \to \psi) \to \lnot\lnot \varphi \land \lnot\psi
具体例として$ \Gamma \vdash_\mathbf{iPL} (\lnot\lnot\lnot\lnot \varphi \to \lnot\lnot\varphi) \to \lnot\lnot(\lnot\lnot\varphi \to \varphi).
二重否定導入$ \Gamma \vdash_\mathbf{iPL} \lnot \varphi \to \lnot\lnot\lnot\varphiに対偶0を使って$ \Gamma \vdash_\mathbf{iPL} \lnot\lnot\lnot\lnot \varphi \to \lnot\lnot\varphiが成り立つからMPより$ \Gamma \vdash_\mathbf{iPL} \lnot\lnot(\lnot\lnot\varphi \to \varphi)