含意の導入規則と除去規則｜記号論理学で「ならば」を扱う

自然演繹において含意（→）は中心的な役割を果たします。「p ならば q」を証明したり、すでに証明された含意を使ったりする方法を、導入規則と除去規則として学びます。

含意除去（→E）

含意除去は、前回学んだモーダスポネンスそのものです。p → q と p から q を導きます。

$$\frac{p\to qp}{q}(\to E)$ この規則は直感的に明らかでしょう。「p ならば q」と「p」がわかっているなら、「q」を結論できます。 証明の中では、すでに導いた含意 p → q と、その前件 p を使って、後件 q を取り出すときに使います。 <!-- outer_0 --> ## 含意導入（→I） 含意導入は、含意 p → q を新たに導くための規則です。p を仮定し、そこから q を導き、その後で仮定 p を解消して p → q を結論します。 $\frac{[p]⋮q}{p\to q}(\to I)$$

角括弧 [p] は仮定を表します。仮定 p のもとで q を導くことに成功したら、「p を仮定すれば q が導ける」ことがわかったので、p → q を結論できます。このとき仮定 p は「解消」され、もう使えなくなります。

含意導入の具体例

p → p を証明してみましょう。これは「p ならば p」という自明な命題です。

このように、仮定してそのまま結論に使い、含意を作るのが最も単純な例です。

より複雑な例

p → (q → p) を証明してみましょう。これは「p ならば、q ならば p」という命題で、p が真なら q が何であっても p が導けるという意味です。

まず p を仮定します。次に q を仮定します。p はすでに仮定されているので、使えます。ここで含意導入を適用し、仮定 q を解消して q → p を得ます。さらに含意導入を適用し、仮定 p を解消して p → (q → p) を得ます。

仮定の管理

自然演繹では、どの仮定が「開いている」（まだ解消されていない）かを管理することが重要です。

開いた仮定は、その後の推論で自由に使えます。しかし、含意導入で解消された仮定は、それ以降使えません。証明が完成したとき、すべての仮定が解消されていれば、前提なしで結論が導かれたことになります。

仮定が残っている場合、その仮定を前提とした証明になります。「p を仮定すれば q が導ける」という形の結果です。

含意の入れ子

含意の含意、たとえば (p → q) → (p → r) のような式も、同じ手順で扱えます。外側の含意を導入するには、p → q を仮定し、そこから p → r を導き、仮定を解消します。

含意導入を入れ子にして使うことで、任意の深さの含意を含む式を証明できます。

次回は、連言と選言の推論規則を学びます。これらと含意の規則を組み合わせることで、命題論理の多くの定理を証明できるようになります。