含意の導入規則と除去規則｜記号論理学で「ならば」を扱う
自然演繹において含意（→）は中心的な役割を果たします。「p ならば q」を証明したり、すでに証明された含意を使ったりする方法を、導入規則と除去規則として学びます。
含意除去（→E）
含意除去は、前回学んだモーダスポネンスそのものです。p → q と p から q を導きます。
$ この規則は直感的に明らかでしょう。「p ならば q」と「p」がわかっているなら、「q」を結論できます。 証明の中では、すでに導いた含意 p → q と、その前件 p を使って、後件 q を取り出すときに使います。 <!-- outer_0 --> ## 含意導入（→I） 含意導入は、含意 p → q を新たに導くための規則です。p を仮定し、そこから q を導き、その後で仮定 p を解消して p → q を結論します。 $
角括弧 [p] は仮定を表します。仮定 p のもとで q を導くことに成功したら、「p を仮定すれば q が導ける」ことがわかったので、p → q を結論できます。このとき仮定 p は「解消」され、もう使えなくなります。
含意導入の具体例
p → p を証明してみましょう。これは「p ならば p」という自明な命題です。
p を仮定する（仮定番号 1 とする）。
仮定 p から p 自体はすでに得られている（何もしなくてよい）。
含意導入を適用し、仮定 1 を解消して 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 を導く
p → (q → p) を導く
仮定の管理
自然演繹では、どの仮定が「開いている」（まだ解消されていない）かを管理することが重要です。
開いた仮定は、その後の推論で自由に使えます。しかし、含意導入で解消された仮定は、それ以降使えません。証明が完成したとき、すべての仮定が解消されていれば、前提なしで結論が導かれたことになります。
仮定が残っている場合、その仮定を前提とした証明になります。「p を仮定すれば q が導ける」という形の結果です。
含意の入れ子
含意の含意、たとえば (p → q) → (p → r) のような式も、同じ手順で扱えます。外側の含意を導入するには、p → q を仮定し、そこから p → r を導き、仮定を解消します。
含意導入を入れ子にして使うことで、任意の深さの含意を含む式を証明できます。
既存の含意を使って結論を取り出す。モーダスポネンス。
新しい含意を作り出す。仮定して導いて解消する。
次回は、連言と選言の推論規則を学びます。これらと含意の規則を組み合わせることで、命題論理の多くの定理を証明できるようになります。
