自然演繹とは？

自然演繹（しぜんえんえき、natural deduction）は、1935年にゲルハルト・ゲンツェン（Gerhard Gentzen）が提案した証明論の体系です。公理を最小限に抑え、代わりに各論理演算子（∧・∨・→・¬・∀・∃など）に対して「導入規則」と「消去規則」の対を用意し、仮定を立てては使い終わったら消去するという形で証明を進めます。

自然演繹の基本的な規則の例は次のとおりです。

• →導入：仮定PのもとでQが証明できたなら、仮定を消去してP→Qを導く
• →消去（モーダスポネンス）：P→QとPがあればQが導ける
• ∧導入：PとQが両方あればP∧Qを導ける
• ∧消去：P∧QからPだけ（またはQだけ）を取り出せる

この体系は従来の公理系（ヒルベルト流）と比べて、証明の流れが人間の思考過程に近く直感的にわかりやすいという特徴があります。証明を木構造（証明木・導出木）として視覚的に表現できるため、教育・研究の両面で広く用いられています。

また、自然演繹とカリー＝ハワード対応（Curry-Howard correspondence）により、証明と型付きラムダ計算のプログラムが対応することが知られています。この関係は関数型プログラミング言語の型理論・依存型・定理証明支援系（Coq・Agdaなど）の理論的基盤となっており、論理学と計算機科学を橋渡しする重要な概念です。