自然演繹
A ∧ B true A true ∧ E 1 A ∧ B true B true ∧ E 2 {\displaystyle {\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 も真である。その導出過程は、下にある推論の前提が前の推論の結論となるような記法で表される。
A ∧ B true B true ∧ E 2 A ∧ B true A true ∧ E 1 B ∧ A true ∧ I {\displaystyle {\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)の一般的記法を必要とする。
数理論理学での一般的操作として、「仮定からの推論; reasoning from assumptions」がある。例として、次のような演繹過程を見てみよう。
A ∧ ( B ∧ C ) t r u e B ∧ C t r u e B t r u e ∧ E 1 ∧ E 2 {\displaystyle {\cfrac {A\wedge \left(B\wedge C\right)\ true}{{\cfrac {B\wedge C\ true}{B\ true}}\wedge E_{1}}}\wedge E_{2}}
このような導出によって B が真であることが確定するわけではないが、次のような事実は確定する。
もし A ∧ (B ∧ C) が真なら B は真である。
論理学では、「A ∧ (B ∧ C) が真と仮定すれば、B は真である」と言え、言い換えれば、"B true" という判断は "A ∧ (B ∧ C) true" という判断に依存している。これが「仮説的導出; hypothetical derivation」であり、次のように記される。
A ∧ ( B ∧ C ) t r u e ⋮ B t r u e {\displaystyle {\begin{matrix}A\wedge \left(B\wedge C\right)\ true\\\vdots \\B\ true\end{matrix}}}
その意味は「B true は A ∧ (B ∧ C) true から導出可能である」となる。もちろん、この例では導出過程は明らかだが、一般に導出が自明とは限らない。仮設的導出の一般形は次のようになる。
自然演繹は、ヒルベルト、フレーゲ、ラッセルらに共通する命題論理的公理化に対する不満から生じた。そのような公理化の最も有名な例としては、ラッセルとホワイトヘッドの『数学原理』がある。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 の定式化に若干修正を施したものだが、ペール・マルティン=レーフの影響もある。
Ω;⋅ ⊢ π1 : A true かつ Ω, u: (A valid) ; Γ ⊢ π2 : C true ならば、 Ω;Γ ⊢ [π1/u] π2 : C true である。
このような仮説の集合を区別して判断するフレームワークを、「多項的; polyadic」コンテキストなどと呼び、非常に強力で拡張性がある。様々な様相論理に適用可能で、他にも線型論理や部分構造論理にも適用した例がある。