自然演繹入門：人間の思考に近い証明体系 - 記号論理学

自然演繹（natural deduction）は、人間の自然な推論過程を模した証明体系です。仮定を立てて推論し、その仮定を解消するという流れで証明を構築します。ヒルベルト流の公理系と比べて直感的で、証明の構造が見やすいという特徴があります。

自然演繹の基本的な考え方

自然演繹の特徴は、各論理結合子に対して「導入規則」と「除去規則」のペアを持つことです。導入規則はその結合子を含む式を作る方法、除去規則はその結合子を含む式から情報を取り出す方法を定めます。

たとえば連言 ∧ について、p と q から p ∧ q を作るのが導入規則、p ∧ q から p や q を取り出すのが除去規則です。

仮定と仮定の解消

自然演繹の重要な概念は「仮定」です。証明の途中で一時的に何かを仮定し、推論を進め、最終的にその仮定を解消します。

含意 p → q を証明したいとき、まず p を仮定し、そこから q を導きます。q が導けたら、「p を仮定すれば q が導ける」ことがわかったので、p → q を結論し、仮定 p を解消します。

この「仮定して推論、その後解消」というパターンが自然演繹の核心です。

証明の書き方

自然演繹の証明は、縦に行を並べて書くことが多いです。各行には、論理式、その正当化（使った規則）、仮定の番号などを書きます。

自然演繹の利点

自然演繹には、ヒルベルト流と比べていくつかの利点があります。

まず、証明が人間の思考に近い形で進みます。「これを仮定すると何が言えるか」という思考実験を形式化しているからです。

また、各規則が対称的で覚えやすいです。連言には連言導入と連言除去、選言には選言導入と選言除去、というように整理されています。

さらに、証明の各部分が何をしているかが明確です。どこで仮定を立て、どこで解消したかが構造としてわかります。

ゲンツェンの貢献

自然演繹は、1930年代にドイツの論理学者ゲルハルト・ゲンツェン（Gerhard Gentzen）が考案しました。ゲンツェンは同時にシーケント計算という別の体系も開発し、証明論の基礎を築きました。

ゲンツェンの研究は、証明そのものを数学的対象として扱う「証明論」の出発点となりました。証明の構造を分析し、証明を変換する方法を研究する分野です。

これから学ぶこと

次回以降、各論理結合子の導入規則と除去規則を詳しく学んでいきます。含意、連言、選言、否定のそれぞれについて、どのように規則を使うかを見ていきます。

自然演繹をマスターすれば、真理値表を作らなくても証明を構築できるようになります。これは変数が多い場合に特に有効であり、数学的な証明の基礎的な訓練にもなります。