自然演繹のソースを表示

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

== 自然演繹論理 ==
自然演繹論理のあるバージョンには、[[公理]]が存在しない。[[ジョン・レモン]]が開発した体系 L は、証明の構文規則に関する次のような9つの基本的規則だけを持つ。

# 仮定の規則 "The Rule of Assumption" (A)
# [[モーダスポネンス]] "Modus Ponendo Ponens" (MPP)
# [[二重否定の除去|二重否定の規則]] "The Rule of Double Negation" (DN)
# 条件付き証明の規則 "The Rule of Conditional Proof" (CP)
# [[論理積の導入|∧-導入の規則]] "The Rule of ∧-introduction" (∧I)
# [[論理積の消去|∧-除去の規則]] "The Rule of ∧-elimination" (∧E)
# [[論理和の導入|∨-導入の規則]] "The Rule of ∨-introduction" (∨I)
# [[論理和の消去|∨-除去の規則]] "The Rule of ∨-elimination" (∨E)
# [[背理法]] "Reductio Ad Absurdum" (RAA)

L では、証明は以下のような条件で定義されている。

# [[well-formed formula|論理式]]（wff）の有限な列を持つ。
# 各行は、L の規則によって正当化される。
# 証明の最終行が結論であり、証明の前提（群）のみを使って導かれなければならない。また、前提が存在しない場合もある。

前提がない場合、その列を[[定理]]と呼ぶ。従って、L における定理は、次のように定義される。
* 空集合の前提を使って L において証明可能な列
* L における空集合の前提から証明可能な列

ある証明の例（[[モーダストレンス]]）:

{| class="wikitable"
|align="center" bgcolor="#FFEBAD" colspan="4"|''p'' → ''q'', ¬''q'' ⊢ ¬''p''  [Modus Tollendo Tollens (MTT)]
|-
!前提番号
!行番号
!論理式 (''wff'')
!根拠となる規則と使っている行
|-
|bgcolor="#bbffbb"|1
|bgcolor="#bbffbb"|(1)
|bgcolor="#bbffbb"|(''p'' → ''q'')
|bgcolor="#bbffbb"| A
|-
|bgcolor="#bbffbb"|2
|bgcolor="#bbffbb"|(2)
|bgcolor="#bbffbb"|¬''q''
|bgcolor="#bbffbb"| A
|-
|bgcolor="#bbffbb"|3
|bgcolor="#bbffbb"|(3)
|bgcolor="#bbffbb"|''p''
|bgcolor="#bbffbb"| A (for RAA)
|-
|bgcolor="#bbffbb"|1,3
|bgcolor="#bbffbb"|(4)
|bgcolor="#bbffbb"|''q''
|bgcolor="#bbffbb"| 1,3,MPP
|-
|bgcolor="#bbffbb"|1,2,3
|bgcolor="#bbffbb"|(5)
|bgcolor="#bbffbb"|''q'' ∧ ¬''q''
|bgcolor="#bbffbb"| 2,4,∧I
|-
|bgcolor="#bbffbb"|1,2
|bgcolor="#bbffbb"|(6)
|bgcolor="#bbffbb"|¬''p''
|bgcolor="#bbffbb"| 3,5,RAA
|-
|align="center" bgcolor="#BBBBFF" colspan="4"|Q.E.D
|-
|}

別の証明の例（[[排中律]]）:

{| class="wikitable"
|align="center" bgcolor="#FFEBAD" colspan="4"|⊢''p'' ∨  ¬''p''
|-
!前提番号
!行番号
!論理式 (''wff'')
!根拠となる規則と使っている行
|-
|bgcolor="#bbffbb"|1
|bgcolor="#bbffbb"|(1)
|bgcolor="#bbffbb"|¬(''p'' ∨  ¬''p'')
|bgcolor="#bbffbb"|A (for RAA)
|-
|bgcolor="#bbffbb"|2
|bgcolor="#bbffbb"|(2)
|bgcolor="#bbffbb"|¬''p''
|bgcolor="#bbffbb"|A (for RAA)
|-
|bgcolor="#bbffbb"|2
|bgcolor="#bbffbb"|(3)
|bgcolor="#bbffbb"|(''p'' ∨  ¬''p'')
|bgcolor="#bbffbb"|2, ∨I
|-
|bgcolor="#bbffbb"|1, 2
|bgcolor="#bbffbb"|(4)
|bgcolor="#bbffbb"|(''p'' ∨  ¬''p'') ∧ ¬(''p'' ∨  ¬''p'')
|bgcolor="#bbffbb"|1, 2, ∧I
|-
|bgcolor="#bbffbb"|1
|bgcolor="#bbffbb"|(5)
|bgcolor="#bbffbb"|¬¬''p''
|bgcolor="#bbffbb"|2, 4, RAA
|-
|bgcolor="#bbffbb"|1
|bgcolor="#bbffbb"|(6)
|bgcolor="#bbffbb"|''p''
|bgcolor="#bbffbb"|5, DN
|-
|bgcolor="#bbffbb"|1
|bgcolor="#bbffbb"|(7)
|bgcolor="#bbffbb"|(''p'' ∨  ¬''p'')
|bgcolor="#bbffbb"|6, ∨I
|-
|bgcolor="#bbffbb"|1
|bgcolor="#bbffbb"|(8)
|bgcolor="#bbffbb"|(''p'' ∨  ¬''p'') ∧ ¬(''p'' ∨  ¬''p'')
|bgcolor="#bbffbb"|1, 7, ∧I
|-
|bgcolor="#bbffbb"|
|bgcolor="#bbffbb"|(9)
|bgcolor="#bbffbb"|¬¬(''p'' ∨  ¬''p'')
|bgcolor="#bbffbb"|1, 8, RAA
|-
|bgcolor="#bbffbb"|
|bgcolor="#bbffbb"|(10)
|bgcolor="#bbffbb"|(''p'' ∨  ¬''p'')
|bgcolor="#bbffbb"|9, DN
|-
|align="center" bgcolor="#BBBBFF" colspan="4"|Q.E.D
|-
|}

自然演繹論理の体系 L の各規則では、入力とエントリの許容できる型が決まっており、その入力で使われる前提の扱い方もそれぞれ決まっている。

== 背景 ==
自然演繹は、[[ダフィット・ヒルベルト|ヒルベルト]]、[[ゴットロープ・フレーゲ|フレーゲ]]、[[バートランド・ラッセル|ラッセル]]らに共通する[[命題論理]]的公理化に対する不満から生じた。そのような公理化の最も有名な例としては、ラッセルと[[アルフレッド・ノース・ホワイトヘッド|ホワイトヘッド]]の『数学原理』がある。[[1926年]]、[[ポーランド]]で行われた一連の講義で、[[ヤン・ウカシェヴィチ]]は論理のより自然な扱いを主張した。これに触発された Stanisław Jaśkowski がより自然な演繹を定義しようと試み、[[1929年]]には図表的記法を使った方法を提案し、[[1934年]]から[[1935年]]にかけてより洗練された提案を一連の論文として発表した。しかし、その提案は一般には全く認知されなかった。現代の自然演繹の形式はそれとは独立に[[1935年]]にドイツ人数学者[[ゲルハルト・ゲンツェン]]が学位論文で提案したものである。「自然演繹」という用語（のドイツ語版 natürlichen Schließens）はその論文で使われたものであった。<ref> Gentzen, ''Untersuchungen über das logische Schließen'' (Mathematische Zeitschrift 39, pp.176-210, 1935)</ref>

ゲンツェンは数論の一貫性を確立したいと考えており、自然演繹をさっそく応用した。彼は、その証明の複雑性に不満を持ち、1938年には[[シークエント計算]]を新たな証明の道具として考案した。[[1961年]]と[[1962年]]の一連の講義で、Dag Prawitz は自然演繹の包括的なまとめを行った。彼の1965年の学術論文 ''Natural deduction: a proof-theoretical study'' は自然演繹の最終版ともいうべきもので、[[様相論理学|様相論理]]や[[二階述語論理]]への応用も含んでいた。

以下で説明するのは、ゲンツェンや Prawitz の定式化に若干修正を施したものだが、[[ペール・マルティン＝レーフ]]の影響もある。

== 形式的定義 ==
'''[[演繹]]'''（または'''証明'''）は、[[命題論理]]のような[[形式体系]]の文脈では正確に定義できる。[[命題]] α は、前提の集合 Σ に[[推論規則]]を繰り返し適用することで演繹される。演繹は、この推論規則の繰り返し適用の記録である。

より形式的には、命題の有限な列 ''β<sub>1</sub> ,..., β<sub>n</sub>'' が、前提の集合 Σ からの α の'''演繹'''であるとは、次が成り立つ場合である。
:* ''β<sub>n</sub> = α'' であり、かつ
:* 全ての 1 ≤ ''i'' ≤ ''n'' について、''β<sub>i</sub>'' が前提であるか（すなわち、''β<sub>i</sub>'' ∈ Σ）または ''β<sub>i</sub>'' がそれ以前に出現した命題に何らかの推論規則を適用した結果である。

公理的命題論理のバージョンによって採用する[[公理]]や推論規則が異なる。例えば、[[ゴットロープ・フレーゲ|フレーゲ]]は、6つの公理と2つの規則を採用した。[[バートランド・ラッセル]]と[[アルフレッド・ノース・ホワイトヘッド]]は、5つの公理からなる体系を示唆した。

[[ヤン・ウカシェヴィチ]]による公理的命題論理のバージョンでは、次のような公理群 ''A'' を採用した。
:*[PL1] ''p'' → (''q'' → ''p'')
:*[PL2] (''p'' → (''q'' → ''r'')) → ((''p'' → ''q'') → (''p'' → ''r''))
:*[PL3] (¬''p'' → ¬''q'') → (''q'' → ''p'')
そして、推論規則 ''R'' としては、モーダスポネンスを採用した。
:*[MP] α と α → β から、β を推論する。

推論規則により、Σ に含まれる論理式と公理群から新たな論理式を導出できる。

== 判断と命題 ==
判断とは、何らかの認識可能なこと、すなわち知識の対象である。誰かが実際に何かを知っていれば、その何かは自明である。従って、「雨が降っている」は判断であり、実際に雨が降っていることを知っている人にとって、その言葉は自明である。この場合、その言葉を聞いた人が窓の外を見たり、外に出てみれば、自明となる「証拠」が簡単に得られる。しかし数理論理学では、証拠は直接観測不可能なことが多く、むしろより基本的な自明な判断から導き出される（演繹される）。演繹の過程は証明を構成する。言い換えれば、判断はその証明を知る人にとっては自明となる。

論理における最も重要な判断は「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'' という命題（形式的に記せば "<math>A \wedge B</math>"）を生成するとする。これを推論規則の形式で書くと次のようになる。

<div style="margin-left: 2em;">
<math>\frac{A\hbox{ prop} \qquad B\hbox{ prop}}{A \wedge B\hbox{ prop}}\ \wedge_F</math>
</div>
この推論規則は図式的（schematic）である。''A'' と ''B'' は任意の式に置き換えることができる。この推論規則の一般形式は次の通り。
<div style="margin-left: 2em;">
<math>\frac{J_1 \qquad J_2 \qquad \cdots \qquad J_n}{J}\ \hbox{name}</math>
</div>
ここで、それぞれの <math>J_i</math> が判断であり、推論規則名が "name" となる。線の上にある各判断は前提（premises）と呼ばれ、線の下にある判断は結論（conclusions）と呼ばれる。その他の典型的な論理命題として、[[論理和]] (<math>A \vee B</math>)、[[否定]] (<math>\neg A</math>)、[[論理包含|含意]] (<math>A \supset B</math>) があり、論理定数として真 (<math>\top</math>) と偽 (<math>\bot</math>) がある。これらの構成規則は次の通りである。
<div style="margin-left: 2em;">
<math>
\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
</math><br /><br /><math>
\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
</math>
</div>

== 導入と除去 ==
ここで判断 "''A'' true" について述べる。論理結合子を結論として導入する推論規則を導入規則（introduction rules）と呼ぶ。[[論理積]]を導入するとは、命題 ''A'' と ''B'' について "''A and B'' true" を結論とすることに他ならない。このとき、"''A'' true" と "''B'' true" の証拠が必要である。これを推論規則で表すと、次のようになる。
<div style="margin-left: 2em">
<math>
\frac{A\hbox{ true} \qquad B\hbox{ true}}{A \wedge B\hbox{ true}}\ \wedge_I
</math>
</div>
このような規則において、各オブジェクトが命題であることは自明とされる。すなわち、この規則を正確に記すと次のようになる。
<div style="margin-left: 2em">
<math>
\frac{A\hbox{ prop} \qquad B\hbox{ prop} \qquad A\hbox{ true} \qquad B\hbox{ true}}{A \wedge B\hbox{ true}}\ \wedge_I
</math>
</div>
これを次のようにも書き表せる。
<div style="margin-left: 2em">
<math>
\frac{A \wedge B\hbox{ prop} \qquad A\hbox{ true} \qquad B\hbox{ true}}{A \wedge B\hbox{ true}}\ \wedge_I
</math>
</div>
この形式では、第一の前提は構成規則 <math>\wedge_F</math> に従って得られたものである。以下では判断 "prop" は自明として省略する。なお、真は前提が全くないところからも導かれる。
<div style="margin-left: 2em">
<math>
\frac{\ }{\top\hbox{ true}}\ \top_I
</math>
</div>
命題の真理値が決まる過程が1つでない場合、その結合子には複数の推論規則が対応することになる。
<div style="margin-left: 2em">
<math>
\frac{A\hbox{ true}}{A \vee B\hbox{ true}}\ \vee_{I1}
\qquad
\frac{B\hbox{ true}}{A \vee B\hbox{ true}}\ \vee_{I2}
</math>
</div>
なお、何の前提もなく偽を導入する導入規則は存在しない。従って、単純な判断から偽であることを推論することはできない。

導入規則と対になる除去規則（elimination rules）がある（削除規則とも）。すなわち、複合型の命題を解体するものである。例えば、"''A ∧ B'' true" から "''A'' true" と "''B'' true" を結論とすることができる。
<div style="margin-left: 2em">
<math>
\frac{A \wedge B\hbox{ true}}{A\hbox{ true}}\ \wedge_{E1}
\qquad
\frac{A \wedge B\hbox{ true}}{B\hbox{ true}}\ \wedge_{E2}
</math>
</div>
推論規則の適用例として、論理積の[[交換法則]]の例を示す。''A ∧ B'' が真なら、''B ∧ A'' も真である。その導出過程は、下にある推論の前提が前の推論の結論となるような記法で表される。

<div style="margin-left: 2em">
<!-- there are serious vertical spacing issues here, but since Wikipedia's texvc parser doesn't support \displaystyle, our hands are tied somewhat -->
<math>
 \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
</math>
</div>

ここまで述べてきた推論の手法では、含意の導入や論理和の除去といった規則を述べるのに十分ではない。そのためには、仮説的導出（hypothetical derivation）の一般的記法を必要とする。

== 仮説的導出 ==
数理論理学での一般的操作として、「仮定からの推論; reasoning from assumptions」がある。例として、次のような演繹過程を見てみよう。
<div style="margin-left: 2em">
<math>
\cfrac{A \wedge \left ( B \wedge C \right ) \ true}{\cfrac{B \wedge C \ true}{B \ true} \wedge E_1} \wedge E_2
</math>
</div>
このような導出によって ''B'' が真であることが確定するわけではないが、次のような事実は確定する。
:もし ''A ∧ (B ∧ C)'' が真なら ''B'' は真である。
論理学では、「A ∧ (B ∧ C) が真と仮定すれば、B は真である」と言え、言い換えれば、"''B true''" という判断は "''A ∧ (B ∧ C) true''" という判断に依存している。これが「仮説的導出; hypothetical derivation」であり、次のように記される。
<div style="margin-left: 2em">
<math>
\begin{matrix}
A \wedge \left ( B \wedge C \right ) \ true \\
\vdots \\
B \ true
\end{matrix}
</math>
</div>
その意味は「''B true'' は ''A ∧ (B ∧ C) true'' から導出可能である」となる。もちろん、この例では導出過程は明らかだが、一般に導出が自明とは限らない。仮設的導出の一般形は次のようになる。
<div style="margin-left: 2em">
<math>
\begin{matrix}
D_1 \quad D_2 \cdots D_n \\
\vdots \\
J
\end{matrix}
</math>
</div>
仮説的導出には、先頭行に書かれた前件群（''D<sub>i</sub>''、antecedent derivations）と最終行に書かれた1つの後件判断（''J''、succedent judgement）がある。それぞれの前提が仮説的導出の結果となっている場合もある。以下、判断（judgement）は前提のない導出として扱う。

仮説的判断の考え方は、含意の結合子に利用される。含意の導入規則と除去規則は次のようになる。
<div style="margin-left: 2em">
<math>
\cfrac{
 \begin{matrix}
 \cfrac{}{A \ true} u \\
 \vdots \\
 B \ true
 \end{matrix}
}{A \supset B \ true} \supset I^u
\qquad \cfrac{A \supset B \ true \quad A \ true}{B \ true} \supset E
</math>
</div>

導入規則では、前件 ''u'' は結論には現れない。これは仮説の「範囲」を限定する機構であり、その存在理由は "''B true''" を確立することにある。それ以外の目的で使うことはできず、特に導入後に使うことはできない。例として、"''A ⊃ (B ⊃ (A ∧ B)) true''" の導出を示す。
<div style="margin-left: 2em">
<math>
 \cfrac{\cfrac{\cfrac{{}}{A \ true} u \quad \cfrac{{}}{B \ true} w}{A \wedge B \ true}\wedge I}{
 \cfrac{B \supset \left ( A \wedge B \right ) \ true}{
 A \supset \left ( B \supset \left ( A \wedge B \right ) \right ) \ true
 } \supset I^u
 } \supset I^w
 </math>
</div>
この導出過程には前提が満足されないということはないが、それぞれの導出は仮説的である。例えば、"''B ⊃ (A ∧ B) true''" の導出は（''u''と名づけられた）前件 "''A true''" を仮説としている。

仮説的導出を使うと、論理和の除去規則を書くことができる。
<div style="margin-left: 2em">
<math>
\cfrac{
 A \vee B \hbox{ true}
 \quad
 \begin{matrix}
 \cfrac{}{A \ true} u \\
 \vdots \\
 C \ true
 \end{matrix}
 \quad
 \begin{matrix}
 \cfrac{}{B \ true} w \\
 \vdots \\
 C \ true
 \end{matrix}
}{C \ true} \vee E^{u,w}
</math>
</div>
これを説明すると、''A ∨ B'' が真で、''A true'' と ''B true'' それぞれから ''C true'' が導かれるなら、''C'' は必ず真となる。ここで、''A true'' や ''B true'' を保証しているわけではないことに注意されたい。偽については、次の除去規則が得られる。
<div style="margin-left: 2em">
<math>
\frac{\perp true}{C \ true} \perp E
</math>
</div>
これを解釈すると、偽が真であれば、任意の命題 ''C'' が真である、ということになる。

否定については、含意と類似している。
<div style="margin-left: 2em">
<math>
\cfrac{
 \begin{matrix}
 \cfrac{}{A \ true} u \\
 \vdots \\
 p \ true
 \end{matrix}
}{\lnot A \ true} \lnot I^{u,p}
\qquad
\cfrac{\lnot A \ true \quad A \ true}{C \ true} \lnot E
</math>
</div>
導入規則では、仮説 ''u'' も後件 ''p'' も結論に現れない。これら規則は概略的なので、この導入規則を解釈すると、"''A true''" から任意の命題 ''p'' について "''p true''" であることを導ける場合、''A'' は偽である（すなわち "''not A true''"）、ということになる。除去規則については、''A'' と ''not A'' が共に真である場合、矛盾が生じ、あらゆる命題 ''C'' が真となる。含意と否定の規則がよく似ているため、''not A'' と ''A ⊃ ⊥'' が等価（互いにもう一方を導出可能）であることは容易にわかる。

== 一貫性、完全性、正規形 ==
数学的[[理論]]は、（仮定なしで）偽を証明可能でないなら一貫性があると言われ、論理の推論規則を使って全ての定理が証明可能なら完全性があると言われる。これは論理一般に言えることで、通常はモデルの何らかの観念に対応する。しかし、それとは別に推論規則の統語的な性質としての一貫性と完全性もあり、こちらはモデルとは無関係である。まず、局所一貫性（あるいは局所還元性）とは、ある結合子の導入規則のすぐ後に同じ結合子の除去規則を使っている導出過程があったとき、その部分を除いた等価な導出過程に変換可能であることを意味する。例として論理積の場合を示す。
<table style="margin-left: 2em;"><tr><td>
 ------ u   ------w
 A true     B true
 ------------------ ∧I
     A ∧ B true
     ---------- ∧E<sub>1</sub>
       A true
</td><td width="30" align="center">⇒</td><td>
 ------ u
 A true
</td></tr></table>

これと対になる局所完全性では、除去規則を使って結合子をその導入規則の入力となる形式に分解できることを意味する。論理積での例を示す。
<table style="margin-left: 2em;"><tr><td>
 ---------- u
 A ∧ B true
</td><td width="30" align="center">⇒</td><td>
 ---------- u    ---------- u
 A ∧ B true      A ∧ B true
 ---------- ∧E<sub>1</sub>   ---------- ∧E<sub>2</sub>
   A true           B true
   ----------------------- ∧I
        A ∧ B true
</td></tr></table>

これらの記法は、[[ラムダ計算]]でのβ-簡約やη-変換に正確に対応している。局所完全性では、全ての導出過程がそれに基本的結合子を導入したものと等価であることが示されている。実際、除去の後に導入が行われる順序なら、その導出を「正規; normal」であると称する。正規導出では、全ての除去は導入の前に行われる。多くの論理では、あらゆる導出には等価な正規導出があり、これを「正規形; normal form」と呼ぶ。正規形の存在は、自然演繹だけでは証明が困難だが、[[1961年]]の Dag Prawitz の著書などに示されている。間接的には、カット規則のない[[シークエント計算]]を使えば、もっと簡単に示すことができる。

== 一階と高階の拡張 ==
[[画像:first_order_natural_deduction.png|thumb|right|一階論理体系の要約]]

ここまで述べてきた論理は、単種（single-sorted）論理であり、一種類のオブジェクトだけを扱った命題からなる論理である。この単純なフレームワークの拡張としては、様々なものが提案されてきた。ここでは、個体（individuals）と項（term）という種を導入する。より正確に言えば、新たな判断 "''t is a term''"（または "''t term''"）を導入する（''t'' は概略的な表現）。変項（variables）の[[可算無限集合]] ''V'' と、関数シンボル（functions symbols）の可算無限集合 ''F'' を想定し、項を次のように構築する。
<table style="margin-left: 2em;"><tr><td>
 v ∈ V
 ------ var-F
 v term
</td><td width="10%"></td><td>
 f ∈ F    t<sub>1</sub> term    t<sub>2</sub> term  ...  t<sub>n</sub> term
 ------------------------------------------ app-F
      f (t<sub>1</sub>, t<sub>2</sub>, ..., t<sub>n</sub>) term
</td></tr></table>
命題を表すため、述語（predicates）の第三の可算無限集合 ''P'' を想定し、項群に対する原子述語を次のように定式化する。
<table style="margin-left: 2em;"><tr><td>
 φ ∈ P    t<sub>1</sub> term    t<sub>2</sub> term   ...   t<sub>n</sub> term
 ------------------------------------------ pred-F
      φ (t<sub>1</sub>, t<sub>2</sub>, ..., t<sub>n</sub>) prop
</td></tr></table>
さらに、2種類の[[量化]]（全称量化 (∀) と存在量化 (∃)）を導入する。
<table style="margin-left: 2em;"><tr><td>
   ------ u
   x term
     {{Unicode|⋮}}
   A prop
 ---------- ∀F<sup>u</sup>
 ∀x. A prop
</td><td width="10%"></td><td>
   ------ u
   x term
     {{Unicode|⋮}}
   A prop
 ---------- ∃F<sup>u</sup>
 ∃x. A prop
</td></tr></table>
このような量化された命題には、次のような導入規則と除去規則がある。

<table style="margin-left: 2em;"><tr><td>
   ------ u
   a term
     {{Unicode|⋮}}
 [a/x] A true
 ------------ ∀I<sup>u, a</sup>
 ∀x. A true
</td><td width="10%"></td><td>
 ∀x. A true t term
 -------------------- ∀E
 [t/x] A true
</td></tr><tr><td>
 [t/x] A true
 ------------ ∃I
  ∃x. A true
</td><td width="10%"></td><td>
                ------ u  ------------ v
                a term    [a/x] A true
                       {{Unicode|⋮}}
 ∃x. A true          C true
 -------------------------- ∃E<sup>a, u,v</sup>
            C true
</td></tr></table>
これらの規則で、[''t''/''x''] ''A'' と書かれている部分は、''A'' に存在する全ての ''x'' の実体を ''t'' と置換することを意味する（詳しくは[[ラムダ計算]]を参照されたい）。規則名の上付き文字は、その規則によって排除される要素を意味している。''a'' という項は ∀I の結論には出現しない（このような項をパラメータと呼ぶ）。また、規則 ∃E における仮説名 ''u'' と ''v'' は、仮説的導出の第二前提に局所化されている。これまでの節で論じてきた命題論理は[[決定可能]]だったが、量化子を加えたことで決定不能となる。

ここまで述べた量化表現は「一階; first-order」である。その場合、量化されるオブジェクトと命題は区別される。[[高階論理]]ではその部分が異なり、命題は区別されない。命題の量化には量化の範囲があり、それが規則にも反映される。
<table style="margin-left: 2em;"><tr><td>
   ------ u
   p prop
     {{Unicode|⋮}}
   A prop
 ---------- ∀F<sup>u</sup>
 ∀p. A prop
</td><td width="10%"></td><td>
   ------ u
   p prop
     {{Unicode|⋮}}
   A prop
 ---------- ∃F<sup>u</sup>
 ∃p. A prop
</td></tr></table>
高階論理における導入規則と除去規則は、ここでは扱わない。一階論理と高階論理の間には様々な段階がある。例えば、二階論理は、項を量化した命題と、命題を量化したものを命題として扱う。

== 証明理論と型理論 ==
ここまでの説明は、命題の性質に重きを置いており、「証明」の形式的定義をしていなかった。証明を形式的に記述するには、仮説的導出の記法を若干変える必要がある。前件に（変項の無限可算集合 ''V'' から）「証明変項; proof variables」によるラベルを付け、後件を実際の証明で装飾する。前件あるいは仮説はターンスタイル({{Unicode|⊢}})を挟んで、後件の前に記される。このような変形を「局所化仮説; localized hypotheses」と呼ぶこともある。以上の変更を図にまとめると次のようになる。
<table style="margin-left: 2em;"><tr><td>
 ---- u<sub>1</sub> ---- u<sub>2</sub> ... ---- u<sub>n</sub>
  J<sub>1</sub>      J<sub>2</sub>          J<sub>n</sub>
               {{Unicode|⋮}}
               J
</td><td width="10%" align="center">⇒</td><td>
 u<sub>1</sub>:J<sub>1</sub>, u<sub>2</sub>:J<sub>2</sub>, ..., u<sub>n</sub>:J<sub>n</sub> {{Unicode|⊢}} J
</td></tr></table>
詳細が不要な場合、仮説群をまとめて Γ と記す。証明を正確にするには、証明不能な判断 "''A true''" ではなく、"π ''is a proof of (A true)''"（πは A true の証明である）という判断を扱う。これを記号的に "π : ''A true''" と記する。標準的手法では、証明は判断 "π ''proof''" に構成規則を適用することで示される。最も単純な証明として、ラベル付き仮説を使ったものがある。この場合の証拠はラベル自身である。
<table style="margin-left: 2em;"><tr><td>
 u ∈ V
 ------- proof-F
 u proof
</td><td width="10%"></td><td>
 --------------------- hyp
 u:A true {{Unicode|⊢}} u : A true
</td></tr></table>
簡潔さを保つため、以下では判断ラベル ''true'' を省略する。従って、"Γ {{Unicode|⊢}} π : ''A''" となる。ここで、明確な証明でいくつかの結合子を再評価する。論理積については、論理積の証明の形式を見つけるために、その導入規則 ∧I を見てみる。それらは、2つの要素の証明の対となる。従って、次のようになる。
<table style="margin-left: 2em;"><tr><td>
 π<sub>1</sub> proof    π<sub>2</sub> proof
 -------------------- pair-F
 (π<sub>1</sub>, π<sub>2</sub>) proof
</td><td width="10%"></td><td>
 Γ {{Unicode|⊢}} π<sub>1</sub> : A    Γ {{Unicode|⊢}} π<sub>2</sub> : B
 ------------------------ ∧I
 Γ {{Unicode|⊢}} (π<sub>1</sub>, π<sub>2</sub>) : A ∧ B
</td></tr></table>
除去規則 ∧E<sub>1</sub> と ∧E<sub>2</sub> は論理積の右か左のいずれかの要素を選択する。従って、証明は2つの投影（第一 = '''fst''' と 第二 = '''snd'''）の対となる。
<table style="margin-left: 2em;"><tr><td>
 π proof
 ----------- '''fst'''-F
 '''fst''' π proof
</td><td width="10%"></td><td>
 Γ {{Unicode|⊢}} π : A ∧ B
 ------------- ∧E<sub>1</sub>
 Γ {{Unicode|⊢}} '''fst''' π : A
</td></tr><tr><td>
 π proof
 ----------- '''snd'''-F
 '''snd''' π proof
</td><td width="10%"></td><td>
 Γ {{Unicode|⊢}} π : A ∧ B
 ------------- ∧E<sub>2</sub>
 Γ {{Unicode|⊢}} '''snd''' π : B
</td></tr></table>
含意については、導入によって仮説の局所化（あるいは束縛）が形成され、これを λ を使って記述する。規則にある "Γ, ''u'':''A''" は、仮説群 Γ に追加の仮説 ''u'' を加えることを意味する。
<table style="margin-left: 2em;"><tr><td>
 π proof
 ------------ λ-F
 λu. π proof
</td><td width="10%"></td><td>
 Γ, u:A {{Unicode|⊢}} π : B
 ----------------- ⊃I
 Γ {{Unicode|⊢}} λu. π : A ⊃ B
</td></tr><tr><td>
 π<sub>1</sub> proof   π<sub>2</sub> proof
 ------------------- app-F
 π<sub>1</sub> π<sub>2</sub> proof
</td><td width="10%"></td><td>
 Γ {{Unicode|⊢}} π<sub>1</sub> : A ⊃ B    Γ {{Unicode|⊢}} π<sub>2</sub> : A
 ---------------------------- ⊃E
 Γ {{Unicode|⊢}} π<sub>1</sub> π<sub>2</sub> : B
</td></tr></table>
明確化された証明では、証明を処理し、論じることが可能となる。証明に関する重要な操作は、ある証明を別の証明の前提に置き換える操作である。これを一般に「代入定理; substitution theorem」と呼び、[[数学的帰納法]]によって証明可能である。

; 代入定理 : Γ {{Unicode|⊢}} π<sub>1</sub> : ''A'' ''かつ'' Γ, ''u'':''A'' {{Unicode|⊢}} π<sub>2</sub> : ''B'' ''なら、'' Γ {{Unicode|⊢}} [π<sub>1</sub>/''u''] π<sub>2</sub> : B ''である。''

これまで、判断 "Γ {{Unicode|⊢}} π : ''A''" は、純粋に論理的な意味しかなかった。[[型理論]]では、論理的な観点からより計算的な観点へと変換が行われる。論理的には命題とされていたものが「型」となり、証明は[[ラムダ計算]]におけるプログラムとなる。従って、"π : ''A''" は、「プログラム π の型は ''A'' である」という解釈になる。論理結合子も異なった解釈となる。論理積は積（×）、含意は関数矢印（→）などとなる。ただし、これらの違いは単に表面的なものである。型理論では、構成規則、導入規則、除去規則を自然演繹的に表現する。実際、自然演繹を知っていれば、単純階型理論は容易に理解できる。

論理と型理論の違いは、焦点が型（命題）からプログラム（証明）に移っている点である。型理論は、プログラムの変換可能性や還元可能性に興味の中心がある。全ての型について、還元不可能な正規のプログラムが存在する。これを「正規形」または「値」と呼ぶ。全てのプログラムが正規形に還元可能なら、その型理論は「正規化; normalising」（あるいは弱正規化）されていると言える。正規形が唯一である場合、その理論は「強正規化; strongly normalising」されていると言える。正規化性は複雑な型理論では滅多にない特性であり、その点で論理の世界とは一線を画すことになる（多くの論理において、論理導出には等価な正規な導出があるという事実を思い出していただきたい）。再帰的定義が可能な型理論では、1つの値に還元できないプログラムを書くことが可能である。そのようなプログラムは一般にいかなる型も与えることが可能である。特に、再帰プログラムは型 ⊥ を持つこともあるが、"⊥ ''true''" についての論理的証明は存在しない。以上から、「型としての命題、プログラムとしての証明」というパラダイムは一方向にしか働かない。もし型理論を論理に無理やり変換したとしても、一貫性のない論理しか得られない。

論理と同様、型理論には様々な拡張や変種があり、一階版も高階版もある。型理論の興味深い変種として[[依存型]]理論がある。これは、プログラム全体に量化を施せるものである。量化型は ∀ と ∃ の代わりに Π と Σ を使って記述する。構成規則は次のようになる。
<table style="margin-left: 2em;"><tr><td>
 Γ {{Unicode|⊢}} A type    Γ, x:A {{Unicode|⊢}} B type
 ----------------------------- Π-F
 Γ {{Unicode|⊢}} Πx:A. B type
</td><td width="10%"></td><td>
 Γ {{Unicode|⊢}} A type  Γ, x:A {{Unicode|⊢}} B type
 ---------------------------- Σ-F
 Γ {{Unicode|⊢}} Σx:A. B type
</td></tr></table>
これらの型は矢印と積の型の一般化であり、導入規則と除去規則は次のようになる。
<table style="margin-left: 2em;"><tr><td>
 Γ, x:A {{Unicode|⊢}} π : B
 -------------------- ΠI
 Γ {{Unicode|⊢}} λx. π : Πx:A. B
</td><td width="10%"></td><td>
 Γ {{Unicode|⊢}} π<sub>1</sub> : Πx:A. B   Γ {{Unicode|⊢}} π<sub>2</sub> : A
 ----------------------------- ΠE
 Γ {{Unicode|⊢}} π<sub>1</sub> π<sub>2</sub> : [π<sub>2</sub>/x] B
</td></tr></table>
<table style="margin-left: 2em;"><tr><td>
 Γ {{Unicode|⊢}} π<sub>1</sub> : A    Γ, x:A {{Unicode|⊢}} π<sub>2</sub> : B
 ----------------------------- ΣI
 Γ {{Unicode|⊢}} (π<sub>1</sub>, π<sub>2</sub>) : Σx:A. B
</td><td width="10%"></td><td>
 Γ {{Unicode|⊢}} π : Σx:A. B
 ---------------- ΣE<sub>1</sub>
 Γ {{Unicode|⊢}} '''fst''' π : A
</td><td width="10%"></td><td>
 Γ {{Unicode|⊢}} π : Σx:A. B
 ------------------------ ΣE<sub>2</sub>
 Γ {{Unicode|⊢}} '''snd''' π : ['''fst''' π/x] B
</td></tr></table>
普遍的な依存型理論は非常に強力であり、プログラムの想像可能ないかなる属性もプログラムの型で直接表すことができる。ただし、その普遍性と引き換えに、あるプログラムがある型であるかを決定不能となっている。このため、依存型理論を実際に使う場合、任意のプログラムの量化を許さないで、特定の決定可能な領域（整数、文字列、線形プログラムなど）のみを扱うことが多い。

依存型理論では型がプログラムに依存することを許すのだが、そこから自然に生じる疑問として、プログラムが型に依存するとか他の組合せの依存は可能か、というものがある。この疑問には様々な答えがある。一般的な手法はプログラムを型に関して量化するもので、「パラメトリック・ポリモルフィズム」と呼ぶ。これは、型とプログラムを明確に区別する「断定的ポリモルフィズム」と、両者の区別があいまいな「非断定的ポリモルフィズム」に分類される。依存性とポリモルフィズムの組合せは様々なものが考えられ、Henk Barendregt の [[ラムダ・キューブ]]が有名である。

論理と型理論の境界領域は、研究が盛んな分野である。新たな論理は、論理フレームワークとして型理論的設定で形式化されることが多い。そのような論理フレームワークとして、[[:en:calculus of constructions|calculus of constructions]] や [[:en:LF (logical framework)|LF]] は高階依存型理論に基づいており、決定可能性と表現能力のトレードオフを考慮して考案されている。これらの論理フレームワーク自体は常に自然演繹体系に則っており、自然演繹手法の汎用性を示している。

== 古典論理と様相論理 ==
話を単純化するため、ここまでの説明では[[直観論理]]を使ってきた。[[古典論理]]は、直観論理に次の[[公理]]あるいは[[排中律]]を追加して拡張したものと言える。

:「任意の命題 p について、命題 p ∨ ¬p は真である」

この文自体は、導入も除去も明確でない。実は、これは2種類の連結子に関係している。[[ゲルハルト・ゲンツェン|ゲンツェン]]は、排中律を以下の3つの（等価な）定式化のうちの1つとして扱った。これらは[[ダフィット・ヒルベルト|ヒルベルト]]と Arend Heyting の論理体系にも類似の形式で提示されていた。

<table style="margin-left: 2em;"><tr><td>
 -------------- XM<sub>1</sub>
 A ∨ ¬A true
</td><td width="5%"></td><td>
 ¬¬A true
 ---------- XM<sub>2</sub>
 A true
</td><td width="5%"></td><td>
 -------- ''u''
 ¬A true
 {{Unicode|⋮}}
 ''p'' true
 ------ XM<sub>3</sub><sup>''u, p''</sup>
 A true
</td></tr></table>

この排中律の扱い方は、純粋主義的観点からは好ましくないのに加えて、正規形の定義においてさらなる複雑さを生む。

導入規則と除去規則だけからなる従来からの自然演繹にとって好ましい対処法は、1992年、Michel Parigot が λμ と呼ばれる[[ラムダ計算]]の一種として提案した。彼の手法の鍵となった洞察は、真理値を中心とした判断 "''A true''" を、より古典的な記法に置換したことである。局所的形式では、Γ {{Unicode|⊢}} ''A'' の代わりに Γ {{Unicode|⊢}} Δ とした。この Δ は Γ と同様な命題の集合である。Γ は命題群の論理積であるが、Δ は命題群の論理和である。この構造は[[シークエント計算]]から直接持ってきたものだが、λμ での新規な点は、古典的な自然演繹的照明に計算的意味を与えた点であり、それには[[継続]]あるいは[[LISP]]やその後継で見られる throw/catch が用いられる。

もう1つの重要な拡張は[[様相論理学]]などの論理に関するもので、それらは単なる基本的な真理値の判断以上のことをする必要がある。1965年に Dag Prawitz が様相論理のための自然演繹的記法を述べており、その後も様々な研究が行われてきた。簡単な例を示すため、必要性の様相論理での新たな判断 "''A valid''" を考える。これは次のような意味である。

:「もし "B true" という形式の前提無しで "A true" ならば、"A valid" である」

この断定的判断は単項結合子 {{Unicode|◻}}''A''（"''necessarily A''"）として表され、以下のような導入規則と除去規則となる。

<table style="margin-left: 2em;"><tr><td>
 A valid
 -------- {{Unicode|◻}}I
 {{Unicode|◻}} A true
</td><td width="5%"></td><td>
 {{Unicode|◻}} A true
 -------- {{Unicode|◻}}E
 A true
</td></tr></table>

なお、前提 "''A valid''" には定義規則がないが、その代わりに[[妥当性]]の断定的定義が使われる。この様相は、局所化された形式で仮説を明示的に示すとより明確になる。"Ω;Γ {{Unicode|⊢}} ''A true''" と記したとき、Γ は以前のように真なる仮説群を表し、Ω は妥当な仮説群を表す。右辺には単純な判断 "''A true''" しかない。"Ω {{Unicode|⊢}} ''A valid''" は定義から "Ω;{{Unicode|⋅}} {{Unicode|⊢}} ''A true''" と同じ意味であるため、妥当性はここでは不要である。導入規則と除去規則は次の通りである。
<table style="margin-left: 2em;"><tr><td>
 Ω;{{Unicode|⋅}} {{Unicode|⊢}} π : A true
 -------------------- {{Unicode|◻}}I
 Ω;{{Unicode|⋅}} {{Unicode|⊢}} '''box''' π : {{Unicode|◻}} A true
</td><td width="5%"></td><td>
 Ω;Γ {{Unicode|⊢}} π : {{Unicode|◻}} A true
 ---------------------- {{Unicode|◻}}E
 Ω;Γ {{Unicode|⊢}} '''unbox''' π : A true
</td></tr></table>

様相仮説には独自の仮説規則と代入定理がある。

<table style="margin-left: 2em;"><tr><td>
 ------------------------------- valid-hyp
 Ω, u: (A valid) ; Γ {{Unicode|⊢}} u : A true
</td></tr></table>

; 様相代入定理 : Ω;{{Unicode|⋅}} {{Unicode|⊢}} π<sub>1</sub> : ''A true'' かつ Ω, ''u'': (''A valid'') ; Γ {{Unicode|⊢}} π<sub>2</sub> : ''C true'' ならば、 Ω;Γ {{Unicode|⊢}} [π<sub>1</sub>/''u''] π<sub>2</sub> : ''C true'' である。

このような仮説の集合を区別して判断するフレームワークを、「多項的; polyadic」コンテキストなどと呼び、非常に強力で拡張性がある。様々な様相論理に適用可能で、他にも[[線型論理]]や[[部分構造論理]]にも適用した例がある。

== 関連項目 ==
* [[一階述語論理]]
* [[様相論理学]]
* [[直観論理]]
* [[シークエント計算]]

== 脚注 ==
{{脚注ヘルプ}}{{Reflist}}

== 参考文献 ==
* Jon Barwise and John Etchemendy, 2000. ''Language Proof and Logic''. CSLI (University of Chicago Press) and New York: Seven Bridges Press. 
* {{cite book | author = Jean-Yves Girard | url = http://www.cs.man.ac.uk/~pt/stable/Proofs+Types.html | publisher = Cambridge University Press, Cambridge, England
 | series = Cambridge Tracts in Theoretical Computer Science | title = Proofs and Types | date = 1990年}} 翻訳と付録部分は Paul Taylor と Yves Lafont
* {{cite journal | author=Per Martin-Löf | url = http://www.hf.uio.no/filosofi/njpl/vol1no1/meaning/meaning.pdf | title = On the meanings of the logical constants and the justifications of the logical laws | journal=Nordic Journal of Philosophical Logic | volume=1 | issue=1 | date=1996年 | pages=11-60 }} 
* {{cite journal | author=Frank Pfenning and Rowan Davies | url = http://www-2.cs.cmu.edu/~fp/papers/mscs00.pdf | title = A judgmental reconstruction of modal logic | journal=Mathematical Structures in Computer Science | volume=11 | issue=4 | date=2001年 | pages=511-540 }}

== 外部リンク ==
* Clemente, Daniel, "[http://www.danielclemente.com/logica/dn.en.html Introduction to natural deduction.]"
* [http://www.winterdrache.de/freeware/domino/ Domino On Acid.] ドミノのゲームで自然演繹を視覚化したもの
* Pelletier, Jeff, "[http://www.sfu.ca/~jeffpell/papers/pelletierNDtexts.pdf A History of Natural Deduction and Elementary Logic Textbooks.]"
* [http://www.math.h.kyoto-u.ac.jp/~takasaki/edu/logic/logic7.html VII. 自然演繹（その1）] 高崎金久、京都大学大学院教授

{{Mathematical logic}}

{{DEFAULTSORT:しせんえんえき}}
[[Category:演繹]]
[[Category:証明法]]
[[Category:証明論]]
[[Category:論理計算]]
[[Category:数学に関する記事]]