プログラマー向けというか、数理論理学の枠組みをプログラムとして実装したい人とか形式化数学をやりたい人向けの記事かもしれません（形式化数学についてはこちらの記事もどうぞ）。
なお、ソースコード全体はGitHubにあります。
https://github.com/pizyumi/rena
連載まとめ
含意のみに関する主要な定理
今回はここまで開発してきたシステムを用いて含意のみに関する主要な定理を証明したいと思います。
ただし、含意のみに関する主要な定理の全てを証明する訳ではありませんので注意してください。
実は含意のみに関する主要な定理の中には自然演繹を用いて証明するのに含意除去規則と含意導入規則以外の推論規則が必要なものがあり、そのような定理は必要な推論規則を実装した後で証明することにします。
証明戦略
数学的言明の証明というものは基本的には簡単に見付かるものではなく、数学者が労力と年月をかけてやっと発見するものです。
しかし、実は含意を含む数学的言明を自然演繹を用いて証明するには1つ非常に有効な戦略があります。
勿論全ての含意を含む数学的言明がこの戦略を使って簡単に証明できる訳ではないのですが、まずはその戦略について解説します。
-
含意を含む数学的言明の証明戦略・・・証明したい言明が
P → Qという形をしている時（ここでP、Qは任意の言明）、取り敢えず言明Pを仮定し、言明Qが得られないか試す。もし言明Qが得られた場合にはそこから含意導入規則を適用し、仮定Pを落とし、言明P → Qを結論する。
これは含意を含む数学的言明を証明しようとする場合には非常に有効な戦略であるため、定理の形式的証明に興味のある方は是非覚えて、使えるようになってください。
なお、この戦略は繰り返し使用することもできます。
たとえば、証明したい言明がP → (Q → R)という形をしている時（ここでP、Q、Rは任意の言明）には言明Pと言明Qを仮定し、言明Rが得られないか試すのが有効です。
この最も基本的な証明戦略を覚えたところで含意のみに関する主要な定理を9個証明していきましょう！
P1 → P1（同一律）
これは含意導入規則を使う定理の中で最も単純なものです。
上の戦略を用いてP1を仮定し、含意導入規則を1回適用するだけです。
P1 → ( P2 → P1 )（添加律）
上の同一律P1 → P1の真ん中に言明P2が入る形となっています。
上の戦略を用いてP1を仮定しますが、次のステップ(2)を思い付くのはちょっと難しいかもしれません。
含意導入規則を適用してP2 → P1を結論していますが、この時導入した言明P2は仮定していない言明です。つまり、含意導入規則の適用において仮定は落ちていません。
第2回の記事で説明しましたが、含意導入規則では仮定が落ちないパターンも許されていました。
このような証明方法は偶に出てきますので、しっかり意識して覚えておいてください。
それ以降は難しい部分はありません。含意導入規則を1回適用するだけです。
P1 → ( ( P1 → P2 ) → P2 )
上の戦略を用いてP1を仮定し、更にP1 → P2も仮定します。
そうすると、含意除去規則を適用してP2が結論できます。
後は含意導入規則を2回適用して全ての仮定を落とします。
これは含意除去規則を使う定理の中では最も単純なものです。
( P1 → P2 ) → ( ( P2 → P3 ) → ( P1 → P3 ) )（推移律）
この定理は仮言三段論法とも言います。
上の戦略を用いて仮定した言明から含意除去規則を使用して必要な結論を導き出すだけです。
( P1 → P2 ) → ( ( P3 → P1 ) → ( P3 → P2 ) )
この定理は推移律（仮言三段論法）の別バージョンといった感じの定理です。
証明方法も推移律（仮言三段論法）の場合とほぼ同じで、上の戦略を用いて仮定した言明から含意除去規則を使用して必要な結論を導き出すだけです。
( P1 → ( P1 → P2 ) ) → ( P1 → P2 )
これはP1 → ( P1 → P2 )ならばP1 → P2ということであり、重複している前提（P1）は重複を排除できるという原理を定理として表したものと考えることができます。
証明は上の戦略を用いて仮定→含意除去→含意導入というお決まりの流れです。
( P1 → ( P2 → P3 ) ) → ( P2 → ( P1 → P3 ) )
これはP1 → ( P2 → P3 )ならばP2 → ( P1 → P3 )ということであり、前提の順序は入れ替えることができるという原理を定理として表したものと考えることができます。
証明は上の戦略を用いて仮定→含意除去→含意導入というお決まりの流れです。
( P1 → ( P2 → P3 ) ) → ( ( P1 → P2 ) → ( P1 → P3 ) )
これはP1 → ( P2 → P3 )ならば( P1 → P2 ) → ( P1 → P3 )ということであり、前提を分配するような変形が可能であるということを表しています。
この定理はHilbert流の論理体系（自然演繹とは異なる論理体系の1つ）では公理とされることの多いものです。自然演繹では定理となります。
証明は上の戦略を用いて仮定→含意除去→含意導入というお決まりの流れです。
( ( P1 → P2 ) → ( P1 → P3 ) ) → ( P1 → ( P2 → P3 ) )
これは上の定理を逆にしたものです。
この定理の証明はちょっと難しいかもしれません。
何故なら、添加律の証明の場合と同様に、ステップ(4)で仮定が落ちない含意導入規則の適用のパターンを使っているからです。
それ以外では難しい点はありません。ステップ(4)以外は上の戦略を用いて仮定→含意除去→含意導入というお決まりの流れです。
今回はここまで
今回はここまでとします。次回は否定に関する3つの推論規則について説明します。