二重否定除去と導入をヒルベルト流の演繹で証明してみた

はじめに

　こんにち論理和、n=1です。今回はヒルベルト流の演繹、特にウェカシェビチの演繹体系での二重否定除去と導入を証明していきます。

前提知識

　まずウェカシェビチの演繹体系の説明です。この体系の中では$\varphi,\ \psi,\ \rho$が 論理式 のとき以下の3つの公理が採用されています。
$$ [A1]\quad \varphi \to (\psi \to \varphi) $$
$$ [A2]\quad (\varphi \to (\psi \to \rho)) \to ((\varphi \to \psi) \to (\varphi \to \rho)) $$
$$ [A3]\quad (\neg \psi \to \neg \varphi) \to (\varphi \to \psi) $$
また、推論規則としてすでに$\varphi,\ \varphi \to \psi$が導出されていたら$\psi$を導出するモダスポネンス(MP)のみを用います。

例

　$p \to p$を証明する場合は以下のようになります。
$$ 1.\quad \vdash p \to ((p \to p) \to p) \quad [A1\quad \varphi := p,\ \psi := p \to p] $$
$$ 2.\quad \vdash (p \to ((p \to p) \to p)) \to ((p \to (p \to p)) \to (p \to p)) \quad [A2 \quad \varphi := p,\ \psi := p \to p,\ \rho := p] $$
$$ 3.\quad \vdash(p \to (p \to p)) \to (p \to p) \quad [MP\quad 2,1] $$
$$ 4.\quad \vdash p \to (p \to p) \quad [A1\quad \varphi := p,\ \psi := p] $$
$$ 5.\quad \vdash p \to p \quad [MP\quad 3, 4]\ . \blacksquare $$
左の数字は証明までの番号で、MPを用いるときどこから導出したのか分かりやすいよう書いています。右の$[\quad]$は式を導出するのに使った公理、またはMPとそれに使った番号です。また、$\vdash$は導出されたことを示しています。MPの番号は$\varphi \to \psi,\ \varphi$の順で書いています。

二重否定除去($\neg \neg p \to p$)の証明

　それでは二重否定除去の証明列をとりあえず書いていきます。
$$ 1.\quad \vdash \neg \neg p \to (\neg \neg \neg \neg p \to \neg \neg p) \quad [A1\quad \varphi := \neg \neg p,\ \psi := \neg \neg \neg \neg p] $$
$$ 2.\quad \vdash (\neg \neg \neg \neg p \to \neg \neg p) \to (\neg p \to \neg \neg \neg p)\quad [A3\quad \varphi := \neg p,\ \psi := \neg \neg \neg p] $$
$$ 3.\quad \vdash ((\neg \neg \neg \neg p \to \neg \neg p) \to (\neg p \to \neg \neg \neg p)) \to (\neg \neg p \to ((\neg \neg \neg \neg p \to \neg \neg p) \to (\neg p \to \neg \neg \neg p))) \quad [A1 \quad \varphi := (\neg \neg \neg \neg p \to \neg \neg p) \to (\neg p \to \neg \neg \neg p),\ \psi := \neg \neg p] $$
$$ 4.\quad \vdash \neg \neg p \to ((\neg \neg \neg \neg p \to \neg \neg p) \to (\neg p \to \neg \neg \neg p))\quad [MP\quad 3, 2] $$
$$ 5.\quad \vdash (\neg \neg p \to ((\neg \neg \neg \neg p \to \neg \neg p) \to (\neg p \to \neg \neg \neg p))) \to ((\neg \neg p \to (\neg \neg \neg \neg p \to \neg \neg p)) \to (\neg \neg p \to (\neg p \to \neg \neg \neg p)))\quad [A2 \quad \varphi := \neg \neg p,\ \psi := \neg \neg \neg \neg p \to \neg \neg p,\ \rho := \neg p \to \neg \neg \neg p] $$
$$ 6.\quad \vdash (\neg \neg p \to (\neg \neg \neg \neg p \to \neg \neg p)) \to (\neg \neg p \to (\neg p \to \neg \neg \neg p))\quad [MP\quad 5, 4] $$
$$ 7.\quad \vdash \neg \neg p \to (\neg p \to \neg \neg \neg p)\quad [MP\quad 6, 1] $$
$$ 8.\quad \vdash (\neg p \to \neg \neg \neg p) \to (\neg \neg p \to p)\quad [A3 \quad \varphi := p,\ \psi := \neg \neg p] $$
$$ 9.\quad \vdash ((\neg p \to \neg \neg \neg p) \to (\neg \neg p \to p)) \to (\neg \neg p \to ((\neg p \to \neg \neg \neg p) \to (\neg \neg p \to p)))\quad [A1 \quad \varphi := (\neg p \to \neg \neg \neg p) \to (\neg \neg p \to p) ,\ \psi := \neg \neg p] $$
$$ 10.\quad \vdash \neg \neg p \to ((\neg p \to \neg \neg \neg p) \to (\neg \neg p \to p))\quad [MP\quad 9, 8] $$
$$ 11.\quad \vdash (\neg \neg p \to ((\neg p \to \neg \neg \neg p) \to (\neg \neg p \to p))) \to ((\neg \neg p \to (\neg p \to \neg \neg \neg p)) \to (\neg \neg p \to (\neg \neg p \to p)))\quad [A2\quad \varphi := \neg \neg p,\ \psi := \neg p \to \neg \neg \neg p,\ \rho := \neg \neg p \to p] $$
$$ 12.\quad \vdash (\neg \neg p \to (\neg p \to \neg \neg \neg p)) \to (\neg \neg p \to (\neg \neg p \to p))\quad [MP\quad 11, 10] $$
$$ 13.\quad \vdash \neg \neg p \to (\neg \neg p \to p)\quad [MP\quad 12, 7] $$
$$ 14.\quad \vdash (\neg \neg p \to (\neg \neg p \to p)) \to ((\neg \neg p \to \neg \neg p) \to (\neg \neg p \to p))\quad [A2\quad \varphi := \neg \neg p,\ \psi := \neg \neg p,\ \rho := p] $$
$$ 15. \quad \vdash (\neg \neg p \to \neg \neg p) \to (\neg \neg p \to p)\quad [MP\quad 14, 13] $$
$$ 16.\quad \vdash \neg \neg p \to ((\neg \neg p \to \neg \neg p) \to \neg \neg p) \quad [A1\quad \varphi := \neg \neg p,\ \psi := \neg \neg p \to \neg \neg p] $$
$$ 17.\quad \vdash (\neg \neg p \to ((\neg \neg p \to \neg \neg p) \to \neg \neg p)) \to ((\neg \neg p \to (\neg \neg p \to \neg \neg p)) \to (\neg \neg p \to \neg \neg p)) \quad [A2 \quad \varphi := \neg \neg p,\ \psi := \neg \neg p \to \neg \neg p,\ \rho := \neg \neg p] $$
$$ 18.\quad \vdash(\neg \neg p \to (\neg \neg p \to \neg \neg p)) \to (\neg \neg p \to \neg \neg p) \quad [MP\quad 17,16] $$
$$ 19.\quad \vdash \neg \neg p \to (\neg \neg p \to \neg \neg p) \quad [A1\quad \varphi := \neg \neg p,\ \psi := \neg \neg p] $$
$$ 20.\quad \vdash \neg \neg p \to \neg \neg p \quad [MP\quad 18, 19] $$
$$ 21. \quad \vdash \neg \neg p \to p \quad [MP\quad 15, 20]\ .\blacksquare $$

解説

　これは何をしているのかというと、1.～13.までは三段論法を活用して、14.,15.で整理をして16.～20.で15の式を結論に持っていくというものでした。
　1の$\neg \neg p \to (\neg \neg \neg \neg p \to \neg \neg p)$は、抽象的に見ると$\varphi \to (\neg \neg \psi \to \neg \neg \rho)$と見えます。そして、$[A3]$より$(\neg \neg \psi \to \neg \neg \rho)\to (\neg \rho \to \neg\psi),\ (\neg \rho \to \neg \psi) \to (\psi \to \rho)$なので三段論法的に$(\neg \neg \psi \to \neg \neg \rho) \to (\psi \to \rho)$、さらに$\varphi \to (\neg \neg \psi \to \neg \neg \rho)$であることから三段論法を使えば$\varphi \to (\psi \to \rho)$が導出できます。これを具体的に行ったものが1～13です。
　14, 15で13の$\neg \neg p \to (\neg \neg p \to p)$を$[A2]$で分解し、$(\neg \neg p \to \neg \neg p) \to (\neg \neg p \to p)$にしてしまえば最初に挙げた例のように$\neg \neg p \to \neg \neg p$さえ出してしまえば欲しかった$\neg \neg p \to p$が導出できます。そして$\neg \neg p \to \neg \neg p$を導出するのが16～20でした。

二重否定導入($p \to \neg \neg p$)の証明

$$ 1.\quad \vdash \neg \neg \neg p \to (\neg \neg \neg \neg \neg p \to \neg \neg \neg p)\quad [A1\quad \varphi := \neg \neg \neg p,\ \psi := \neg \neg \neg \neg \neg p] $$
$$ 2.\quad \vdash (\neg \neg \neg \neg \neg p \to \neg \neg \neg p) \to (\neg \neg p \to \neg \neg \neg \neg p)\quad [A3\quad \varphi := \neg \neg p,\ \psi := \neg \neg \neg \neg p] $$
$$ 3.\quad \vdash ((\neg \neg \neg \neg \neg p \to \neg \neg \neg p) \to (\neg \neg p \to \neg \neg \neg \neg p)) \to (\neg \neg \neg p \to ((\neg \neg \neg \neg \neg p \to \neg \neg \neg p) \to (\neg \neg p \to \neg \neg \neg \neg p)))\quad [A1\quad \varphi := (\neg \neg \neg \neg \neg p \to \neg \neg \neg p) \to (\neg \neg p \to \neg \neg \neg \neg p),\ \psi := \neg \neg \neg p] $$
$$ 4.\quad \vdash \neg \neg \neg p \to ((\neg \neg \neg \neg \neg p \to \neg \neg \neg p) \to (\neg \neg p \to \neg \neg \neg \neg p))\quad [MP\quad 3, 2] $$
$$ 5.\quad \vdash (\neg \neg \neg p \to ((\neg \neg \neg \neg \neg p \to \neg \neg \neg p) \to (\neg \neg p \to \neg \neg \neg \neg p))) \to ((\neg \neg \neg p \to (\neg \neg \neg \neg \neg p \to \neg \neg \neg p)) \to (\neg \neg \neg p \to (\neg \neg p \to \neg \neg \neg \neg p)))\quad [A2\quad \varphi := \neg \neg \neg p,\ \psi := \neg \neg \neg \neg \neg p \to \neg \neg \neg p,\ \rho := \neg \neg p \to \neg \neg \neg \neg p] $$
$$ 6.\quad \vdash (\neg \neg \neg p \to (\neg \neg \neg \neg \neg p \to \neg \neg \neg p)) \to (\neg \neg \neg p \to (\neg \neg p \to \neg \neg \neg \neg p))\quad [MP\quad 5, 4] $$
$$ 7.\quad \vdash \neg \neg \neg p \to (\neg \neg p \to \neg \neg \neg \neg p)\quad [MP\quad 6, 1] $$
$$ 8.\quad \vdash (\neg \neg p \to \neg \neg \neg \neg p) \to (\neg \neg \neg p \to \neg p)\quad [A3\quad \varphi := \neg \neg \neg p,\ \psi := \neg p] $$
$$ 9.\quad \vdash ((\neg \neg p \to \neg \neg \neg \neg p) \to (\neg \neg \neg p \to \neg p)) \to (\neg \neg \neg p \to ((\neg \neg p \to \neg \neg \neg \neg p) \to (\neg \neg \neg p \to \neg p)))\quad [A1\quad \varphi := (\neg \neg p \to \neg \neg \neg \neg p) \to (\neg \neg \neg p \to \neg p),\ \psi := \neg \neg \neg p] $$
$$ 10.\quad \vdash \neg \neg \neg p \to ((\neg \neg p \to \neg \neg \neg \neg p) \to (\neg \neg \neg p \to \neg p))\quad [MP\quad 9, 8] $$
$$ 11.\quad \vdash (\neg \neg \neg p \to ((\neg \neg p \to \neg \neg \neg \neg p) \to (\neg \neg \neg p \to \neg p))) \to ((\neg \neg \neg p \to (\neg \neg p \to \neg \neg \neg \neg p)) \to (\neg \neg \neg p \to (\neg \neg \neg p \to \neg p)))\quad [A2\quad \varphi := \neg \neg \neg p,\ \psi := \neg \neg p \to \neg \neg \neg \neg p,\ \rho := \neg \neg \neg p \to \neg p] $$
$$ 12.\quad \vdash (\neg \neg \neg p \to (\neg \neg p \to \neg \neg \neg \neg p)) \to (\neg \neg \neg p \to (\neg \neg \neg p \to \neg p))\quad [MP\quad 11, 10] $$
$$ 13.\quad \vdash \neg \neg \neg p \to (\neg \neg \neg p \to \neg p)\quad [MP\quad 12, 7] $$
$$ 14.\quad \vdash (\neg \neg \neg p \to (\neg \neg \neg p \to \neg p)) \to ((\neg \neg \neg p \to \neg \neg \neg p) \to (\neg \neg \neg p \to \neg p))\quad [A2\quad \varphi := \neg \neg \neg p,\ \psi := \neg \neg \neg p,\ \rho := \neg p] $$
$$ 15.\quad \vdash (\neg \neg \neg p \to \neg \neg \neg p) \to (\neg \neg \neg p \to \neg p)\quad [MP\quad 14, 13] $$
$$ 16.\quad \vdash \neg \neg \neg p \to ((\neg \neg \neg p \to \neg \neg p) \to \neg \neg \neg p) \quad [A1\quad \varphi := \neg \neg \neg p,\ \psi := \neg \neg \neg p \to \neg \neg \neg p] $$
$$ 17.\quad \vdash (\neg \neg \neg p \to ((\neg \neg \neg p \to \neg \neg \neg p) \to \neg \neg \neg p)) \to ((\neg \neg \neg p \to (\neg \neg \neg p \to \neg \neg \neg p)) \to (\neg \neg \neg p \to \neg \neg \neg p)) \quad [A2 \quad \varphi := \neg \neg \neg p,\ \psi := \neg \neg \neg p \to \neg \neg \neg p,\ \rho := \neg \neg \neg p] $$
$$ 18.\quad \vdash(\neg \neg \neg p \to (\neg \neg \neg p \to \neg \neg \neg p)) \to (\neg \neg \neg p \to \neg \neg \neg p) \quad [MP\quad 17,16] $$
$$ 19.\quad \vdash \neg \neg \neg p \to (\neg \neg \neg p \to \neg \neg \neg p) \quad [A1\quad \varphi := \neg \neg \neg p,\ \psi := \neg \neg \neg p] $$
$$ 20.\quad \vdash \neg \neg \neg p \to \neg \neg \neg p \quad [MP\quad 18, 19] $$
$$ 21.\quad \vdash \neg \neg \neg p \to \neg p\quad [MP\quad 15, 20] $$
$$ 22.\quad \vdash (\neg \neg \neg p \to \neg p) \to (p \to \neg \neg p)\quad [A3\quad \varphi := p,\ \psi := \neg \neg p] $$
$$ 23.\quad \vdash p \to \neg \neg p\quad [MP\quad 22, 21]\ .\blacksquare $$

プチ解説

　プチ解説です。二重否定除去$\neg \neg p \to p$の証明列のが$\neg \neg p \to (\neg \neg \neg \neg p \to \neg \neg p)$から始まるのはある程度予想できます。
　$\vdash \varphi \to \psi$を示すのには、$\vdash \varphi \to (\varphi \to \psi)$が示せれば$[A2]$より$\vdash (\varphi \to \varphi) \to (\varphi \to \psi)$が直ちに示せて示せます。なので二重否定除去では13の$\vdash \neg \neg p \to (\neg \neg p \to p)$が示せればよさそうなことが分かります。そして、$[A1]$より$\neg \neg p \to (A \to \neg \neg p)$は示せるのでこの形と$\neg \neg p \to (\neg \neg p \to p)$が三段論法なりでつながりが示せればよさそうです。ここで$[A3]$を思い出すと$(\neg p \to \neg \neg \neg p) \to (\neg \neg p \to p)$で$(\neg \neg \neg \neg p \to \neg \neg p) \to (\neg p \to \neg \neg \neg p)$であり、$A:=\neg \neg \neg \neg p$とすれば$[A1]$の形にうまく合致するので解決し、$\vdash \neg \neg p \to (\neg \neg \neg \neg p \to \neg \neg p)$から始めればよいと予想がたちます。
　二重否定導入$p \to \neg \neg p$は単純に$p \to (p \to \neg \neg p)$とすると$[A3]$での対偶による$\neg$の個数がそろわなくなるので、$\neg$を1つ足してずらし$\vdash \neg \neg \neg p \to (\neg \neg \neg p \to \neg p)$を目的にスタートにしたところ以外は同様です。
　また、この手のもので演繹するとき、テクニックとして$\vdash p \to p$や${p}\vdash q \to p$、三段論法の作り方は覚えておくとほんの少し役に立つかもしれません。

最後に

　カルマールの完全性証明(Kalmár’s Compleness Proof)をもとにトートロジーをウェカシェビチの演繹体系のみの構成に直すアルゴリズムを作って見たら、$[A2]$の逆の$((\varphi \to \psi) \to (\varphi \to \rho)) \to (\varphi \to (\psi \to \rho))$を示すのに何回か改良しても19,474行証明にかかってしまいました。みなさんは良いアルゴリズムを組みましょう。
　以上で二重否定除去と導入をヒルベルト流の演繹で証明してみたは終わりです。投稿を見てくださりありがとうございました。