自然演繹

自然演繹（しぜんえんえき、英: Natural deduction）は、「自然な」ものとしての論理的推論の形式的モデルを提供する証明理論の手法であり、哲学的論理学の用語である。

背景

自然演繹は、ヒルベルト、フレーゲ、ラッセルらに共通する命題論理的公理化に対する不満から生じた。そのような公理化の最も有名な例としては、ラッセルとホワイトヘッドの『数学原理』がある。1926年、ポーランドで行われた一連の講義で、ヤン・ウカシェヴィチは論理のより自然な扱いを主張した。これに触発された Stanisław Jaśkowski がより自然な演繹を定義しようと試み、1929年には図表的記法を使った方法を提案し、1934年から1935年にかけてより洗練された提案を一連の論文として発表した。しかし、その提案は一般には全く認知されなかった。現代の自然演繹の形式はそれとは独立に1935年にドイツ人数学者ゲルハルト・ゲンツェンが学位論文で提案したものである。「自然演繹」という用語（のドイツ語版 natürlichen Schließens）はその論文で使われたものであった。
ゲンツェンは数論の一貫性を確立したいと考えており、自然演繹をさっそく応用した。彼は、その証明の複雑性に不満を持ち、1938年にはシークエント計算を新たな証明の道具として考案した。1961年と1962年の一連の講義で、Dag Prawitz は自然演繹の包括的なまとめを行った。彼の1965年の学術論文 Natural deduction: a proof-theoretical study は自然演繹の最終版ともいうべきもので、様相論理や二階述語論理への応用も含んでいた。
以下で説明するのは、ゲンツェンや Prawitz の定式化に若干修正を施したものだが、ペール・マルティン＝レーフの影響もある。

判断と命題

判断とは、何らかの認識可能なこと、すなわち知識の対象である。誰かが実際に何かを知っていれば、その何かは自明である。従って、「雨が降っている」は判断であり、実際に雨が降っていることを知っている人にとって、その言葉は自明である。この場合、その言葉を聞いた人が窓の外を見たり、外に出てみれば、自明となる「証拠」が簡単に得られる。しかし数理論理学では、証拠は直接観測不可能なことが多く、むしろより基本的な自明な判断から導き出される（演繹される）。演繹の過程は証明を構成する。言い換えれば、判断はその証明を知る人にとっては自明となる。
論理における最も重要な判断は「A は真である」という形式となる。この A は任意の「命題」を表す式で置換される。真かどうかの判断には、より基本的な判断「A は命題である」が必須となる。他にも様々な判断が研究されている。例えば、「A は偽である」（論理学）、「A は時刻 t では真である」（時相論理）、「A は真でなければならない」あるいは「A は真でありうる」（様相論理学）、「プログラム M の型は τ である」（プログラミング言語と型理論）、「A は利用可能な資源から達成できる」（線型論理）などである。以下では、「A は命題である」を "A prop"、「A は真である」を "A true" と表す。
判断 "A prop" は、A の妥当な証明の構造を定義し、そこから命題の構造が定義される。このため、このような判断に対する推論規則を「構成規則; formation rules」とも呼ぶ。ここで、A と B という2つの命題があり（すなわち、"A prop" と "B prop" は自明）、それらを結合した A かつ B という命題（形式的に記せば "A \wedge B"）を生成するとする。これを推論規則の形式で書くと次のようになる。
\frac{A\hbox{ prop} \qquad B\hbox{ prop}}{A \wedge B\hbox{ prop}}\ \wedge_F
この推論規則は図式的（schematic）である。A と B は任意の式に置き換えることができる。この推論規則の一般形式は次の通り。
\frac{J_1 \qquad J_2 \qquad \cdots \qquad J_n}{J}\ \hbox{name}
ここで、それぞれの J_i が判断であり、推論規則名が "name" となる。線の上にある各判断は前提（premises）と呼ばれ、線の下にある判断は結論（conclusions）と呼ばれる。その他の典型的な論理命題として、論理和 (A \vee B)、否定 (\neg A)、含意 (A \supset B) があり、論理定数として真 (\top) と偽 (\bot) がある。これらの構成規則は次の通りである。

\frac{A\hbox{ prop} \qquad B\hbox{ prop}}{A \vee B\hbox{ prop}}\ \vee_F
\qquad
\frac{A\hbox{ prop} \qquad B\hbox{ prop}}{A \supset B\hbox{ prop}}\ \supset_F

\frac{\hbox{ }}{\top\hbox{ prop}}\ \top_F
\qquad
\frac{\hbox{ }}{\bot\hbox{ prop}}\ \bot_F
\qquad
\frac{A\hbox{ prop}}{\neg A\hbox{ prop}}\ \neg_F

導入と除去

ここで判断 "A true" について述べる。論理結合子を結論として導入する推論規則を導入規則（introduction rules）と呼ぶ。論理積を導入するとは、命題 A と B について "A and B true" を結論とすることに他ならない。このとき、"A true" と "B true" の証拠が必要である。これを推論規則で表すと、次のようになる。

\frac{A\hbox{ true} \qquad B\hbox{ true}}{A \wedge B\hbox{ true}}\ \wedge_I
このような規則において、各オブジェクトが命題であることは自明とされる。すなわち、この規則を正確に記すと次のようになる。

\frac{A\hbox{ prop} \qquad B\hbox{ prop} \qquad A\hbox{ true} \qquad B\hbox{ true}}{A \wedge B\hbox{ true}}\ \wedge_I
これを次のようにも書き表せる。

\frac{A \wedge B\hbox{ prop} \qquad A\hbox{ true} \qquad B\hbox{ true}}{A \wedge B\hbox{ true}}\ \wedge_I
この形式では、第一の前提は構成規則 \wedge_F に従って得られたものである。以下では判断 "prop" は自明として省略する。なお、真は前提が全くないところからも導かれる。

\frac{\ }{\top\hbox{ true}}\ \top_I
命題の真理値が決まる過程が1つでない場合、その結合子には複数の推論規則が対応することになる。

\frac{A\hbox{ true}}{A \vee B\hbox{ true}}\ \vee_{I1}
\qquad
\frac{B\hbox{ true}}{A \vee B\hbox{ true}}\ \vee_{I2}
なお、何の前提もなく偽を導入する導入規則は存在しない。従って、単純な判断から偽であることを推論することはできない。
導入規則と対になる除去規則（elimination rules）がある（削除規則とも）。すなわち、複合型の命題を解体するものである。例えば、"A ∧ B true" から "A true" と "B true" を結論とすることができる。

\frac{A \wedge B\hbox{ true}}{A\hbox{ true}}\ \wedge_{E1}
\qquad
\frac{A \wedge B\hbox{ true}}{B\hbox{ true}}\ \wedge_{E2}
推論規則の適用例として、論理積の交換法則の例を示す。A ∧ B が真なら、B ∧ A も真である。その導出過程は、下にある推論の前提が前の推論の結論となるような記法で表される。

 \cfrac{\cfrac{A \wedge B\hbox{ true}}{B\hbox{ true}}\ \wedge_{E2} 
 \qquad
 \cfrac{A \wedge B\hbox{ true}}{A\hbox{ true}}\ \wedge_{E1}}
 {B \wedge A\hbox{ true}}\ \wedge_I
ここまで述べてきた推論の手法では、含意の導入や論理和の除去といった規則を述べるのに十分ではない。そのためには、仮説的導出（hypothetical derivation）の一般的記法を必要とする。