自然演繹

自然演繹（しぜんえんえき、英: 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 では、証明は以下のような条件で定義されている。

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

前提がない場合、その列を定理と呼ぶ。従って、L における定理は、次のように定義される。

空集合の前提を使って L において証明可能な列
L における空集合の前提から証明可能な列

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

前提番号	行番号	論理式 (wff)	根拠となる規則と使っている行
p → q, ¬q ⊢ ¬p [Modus Tollendo Tollens (MTT)]
1	(1)	(p → q)	A
2	(2)	¬q	A
3	(3)	p	A (for RAA)
1,3	(4)	q	1,3,MPP
1,2,3	(5)	q ∧ ¬q	2,4,∧I
1,2	(6)	¬p	3,5,RAA
Q.E.D

別の証明の例（ある定理）:

前提番号	行番号	論理式 (wff)	根拠となる規則と使っている行
⊢p ∨ ¬p
1	(1)	¬(p ∨ ¬p)	A (for RAA)
2	(2)	¬p	A (for RAA)
2	(3)	(p ∨ ¬p)	2, ∨I
1, 2	(4)	(p ∨ ¬p) ∧ ¬(p ∨ ¬p)	1, 2, ∧I
1	(5)	¬¬p	2, 4, RAA
1	(6)	p	5, DN
1	(7)	(p ∨ ¬p)	6, ∨I
1	(8)	(p ∨ ¬p) ∧ ¬(p ∨ ¬p)	1, 7, ∧I
	(9)	¬¬(p ∨ ¬p)	1, 8, RAA
	(10)	(p ∨ ¬p)	9, DN
Q.E.D

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

背景

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

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

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

形式的定義

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

より形式的には、命題の有限な列 β₁ ,..., β_n が、前提の集合 Σ からの α の演繹であるとは、次が成り立つ場合である。

β_n = α であり、かつ
全ての 1 ≤ i ≤ n について、β_i が前提であるか（すなわち、β_i ∈ Σ）または β_i がそれ以前に出現した命題に何らかの推論規則を適用した結果である。

公理的命題論理のバージョンによって採用する公理や推論規則が異なる。例えば、フレーゲは、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]"）を生成するとする。これを推論規則の形式で書くと次のようになる。

[math]\frac{A\hbox{ prop} \qquad B\hbox{ prop}}{A \wedge B\hbox{ prop}}\ \wedge_F[/math]

この推論規則は図式的（schematic）である。A と B は任意の式に置き換えることができる。この推論規則の一般形式は次の通り。

[math]\frac{J_1 \qquad J_2 \qquad \cdots \qquad J_n}{J}\ \hbox{name}[/math]

ここで、それぞれの [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]) がある。これらの構成規則は次の通りである。

[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]

[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]

導入と除去

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

[math] \frac{A\hbox{ true} \qquad B\hbox{ true}}{A \wedge B\hbox{ true}}\ \wedge_I [/math]

このような規則において、各オブジェクトが命題であることは自明とされる。すなわち、この規則を正確に記すと次のようになる。

[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]

これを次のようにも書き表せる。

[math] \frac{A \wedge B\hbox{ prop} \qquad A\hbox{ true} \qquad B\hbox{ true}}{A \wedge B\hbox{ true}}\ \wedge_I [/math]

この形式では、第一の前提は構成規則 [math]\wedge_F[/math] に従って得られたものである。以下では判断 "prop" は自明として省略する。なお、真は前提が全くないところからも導かれる。

[math] \frac{\ }{\top\hbox{ true}}\ \top_I [/math]

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

[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]

なお、何の前提もなく偽を導入する導入規則は存在しない。従って、単純な判断から偽であることを推論することはできない。

導入規則と対になる除去規則（elimination rules）がある（削除規則とも）。すなわち、複合型の命題を解体するものである。例えば、"A ∧ B true" から "A true" と "B true" を結論とすることができる。

[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]

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

[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]

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

仮説的導出

数理論理学での一般的操作として、「仮定からの推論; reasoning from assumptions」がある。例として、次のような演繹過程を見てみよう。

[math] \cfrac{A \wedge \left ( B \wedge C \right ) \ true}{\cfrac{B \wedge C \ true}{B \ true} \wedge E_1} \wedge E_2 [/math]

このような導出によって B が真であることが確定するわけではないが、次のような事実は確定する。

もし A ∧ (B ∧ C) が真なら B は真である。

論理学では、「A ∧ (B ∧ C) が真と仮定すれば、B は真である」と言え、言い換えれば、"B true" という判断は "A ∧ (B ∧ C) true" という判断に依存している。これが「仮説的導出; hypothetical derivation」であり、次のように記される。

[math] \begin{matrix} A \wedge \left ( B \wedge C \right ) \ true \\ \vdots \\ B \ true \end{matrix} [/math]

その意味は「B true は A ∧ (B ∧ C) true から導出可能である」となる。もちろん、この例では導出過程は明らかだが、一般に導出が自明とは限らない。仮設的導出の一般形は次のようになる。

[math] \begin{matrix} D_1 \quad D_2 \cdots D_n \\ \vdots \\ J \end{matrix} [/math]

仮説的導出には、先頭行に書かれた前件群（D_i、antecedent derivations）と最終行に書かれた1つの後件判断（J、succedent judgement）がある。それぞれの前提が仮説的導出の結果となっている場合もある。以下、判断（judgement）は前提のない導出として扱う。

仮説的判断の考え方は、含意の結合子に利用される。含意の導入規則と除去規則は次のようになる。

[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]

導入規則では、前件 u は結論には現れない。これは仮説の「範囲」を限定する機構であり、その存在理由は "B true" を確立することにある。それ以外の目的で使うことはできず、特に導入後に使うことはできない。例として、"A ⊃ (B ⊃ (A ∧ B)) true" の導出を示す。

[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]

この導出過程には前提が満足されないということはないが、それぞれの導出は仮説的である。例えば、"B ⊃ (A ∧ B) true" の導出は（uと名づけられた）前件 "A true" を仮説としている。

仮説的導出を使うと、論理和の除去規則を書くことができる。

[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]

これを説明すると、A ∨ B が真で、A true と B true それぞれから C true が導かれるなら、C は必ず真となる。ここで、A true や B true を保証しているわけではないことに注意されたい。偽については、次の除去規則が得られる。

[math] \frac{\perp true}{C \ true} \perp E [/math]

これを解釈すると、偽が真であれば、任意の命題 C が真である、ということになる。

否定については、含意と類似している。

[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]

導入規則では、仮説 u も後件 p も結論に現れない。これら規則は概略的なので、この導入規則を解釈すると、"A true" から任意の命題 p について "p true" であることを導ける場合、A は偽である（すなわち "not A true"）、ということになる。除去規則については、A と not A が共に真である場合、矛盾が生じ、あらゆる命題 C が真となる。含意と否定の規則がよく似ているため、not A と A ⊃ ⊥ が等価（互いにもう一方を導出可能）であることは容易にわかる。

一貫性、完全性、正規形

数学的理論は、（仮定なしで）偽を証明可能でないなら一貫性があると言われ、論理の推論規則を使って全ての定理が証明可能なら完全性があると言われる。これは論理一般に言えることで、通常はモデルの何らかの観念に対応する。しかし、それとは別に推論規則の統語的な性質としての一貫性と完全性もあり、こちらはモデルとは無関係である。まず、局所一貫性（あるいは局所還元性）とは、ある結合子の導入規則のすぐ後に同じ結合子の除去規則を使っている導出過程があったとき、その部分を除いた等価な導出過程に変換可能であることを意味する。例として論理積の場合を示す。

------ u   ------w
A true     B true
------------------ ∧I
    A ∧ B true
    ---------- ∧E₁
      A true

⇒

------ u
A true

これと対になる局所完全性では、除去規則を使って結合子をその導入規則の入力となる形式に分解できることを意味する。論理積での例を示す。

---------- u
A ∧ B true

⇒

---------- u    ---------- u
A ∧ B true      A ∧ B true
---------- ∧E₁   ---------- ∧E₂
  A true           B true
  ----------------------- ∧I
       A ∧ B true

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

一階と高階の拡張

ファイル:First order natural deduction.png

一階論理体系の要約

ここまで述べてきた論理は、単種（single-sorted）論理であり、一種類のオブジェクトだけを扱った命題からなる論理である。この単純なフレームワークの拡張としては、様々なものが提案されてきた。ここでは、個体（individuals）と項（term）という種を導入する。より正確に言えば、新たな判断 "t is a term"（または "t term"）を導入する（t は概略的な表現）。変項（variables）の可算無限集合 V と、関数シンボル（functions symbols）の可算無限集合 F を想定し、項を次のように構築する。

v ∈ V
------ var-F
v term

f ∈ F    t₁ term    t₂ term  ...  t_n term
------------------------------------------ app-F
     f (t₁, t₂, ..., t_n) term

命題を表すため、述語（predicates）の第三の可算無限集合 P を想定し、項群に対する原子述語を次のように定式化する。

φ ∈ P    t₁ term    t₂ term   ...   t_n term
------------------------------------------ pred-F
     φ (t₁, t₂, ..., t_n) prop

さらに、2種類の量化（全称量化 (∀) と存在量化 (∃)）を導入する。

  ------ u
  x term
    ⋮
  A prop
---------- ∀F^u
∀x. A prop

  ------ u
  x term
    ⋮
  A prop
---------- ∃F^u
∃x. A prop

このような量化された命題には、次のような導入規則と除去規則がある。

  ------ u
  a term
    ⋮
[a/x] A true
------------ ∀I^{u, a}
∀x. A true

∀x. A true t term
-------------------- ∀E
[t/x] A true

[t/x] A true
------------ ∃I
 ∃x. A true

               ------ u  ------------ v
               a term    [a/x] A true
                      ⋮
∃x. A true          C true
-------------------------- ∃E^{a, u,v}
           C true

これらの規則で、[t/x] A と書かれている部分は、A に存在する全ての x の実体を t と置換することを意味する（詳しくはラムダ計算を参照されたい）。規則名の上付き文字は、その規則によって排除される要素を意味している。a という項は ∀I の結論には出現しない（このような項をパラメータと呼ぶ）。また、規則 ∃E における仮説名 u と v は、仮説的導出の第二前提に局所化されている。これまでの節で論じてきた命題論理は決定可能だったが、量化子を加えたことで決定不能となる。

ここまで述べた量化表現は「一階; first-order」である。その場合、量化されるオブジェクトと命題は区別される。高階論理ではその部分が異なり、命題は区別されない。命題の量化には量化の範囲があり、それが規則にも反映される。

  ------ u
  p prop
    ⋮
  A prop
---------- ∀F^u
∀p. A prop

  ------ u
  p prop
    ⋮
  A prop
---------- ∃F^u
∃p. A prop

高階論理における導入規則と除去規則は、ここでは扱わない。一階論理と高階論理の間には様々な段階がある。例えば、二階論理は、項を量化した命題と、命題を量化したものを命題として扱う。

証明理論と型理論

ここまでの説明は、命題の性質に重きを置いており、「証明」の形式的定義をしていなかった。証明を形式的に記述するには、仮説的導出の記法を若干変える必要がある。前件に（変項の無限可算集合 V から）「証明変項; proof variables」によるラベルを付け、後件を実際の証明で装飾する。前件あるいは仮説はターンスタイル(⊢)を挟んで、後件の前に記される。このような変形を「局所化仮説; localized hypotheses」と呼ぶこともある。以上の変更を図にまとめると次のようになる。

---- u₁ ---- u₂ ... ---- u_n
 J₁      J₂          J_n
              ⋮
              J

⇒

u₁:J₁, u₂:J₂, ..., u_n:J_n ⊢ J

詳細が不要な場合、仮説群をまとめて Γ と記す。証明を正確にするには、証明不能な判断 "A true" ではなく、"π is a proof of (A true)"（πは A true の証明である）という判断を扱う。これを記号的に "π : A true" と記する。標準的手法では、証明は判断 "π proof" に構成規則を適用することで示される。最も単純な証明として、ラベル付き仮説を使ったものがある。この場合の証拠はラベル自身である。

u ∈ V
------- proof-F
u proof

--------------------- hyp
u:A true ⊢ u : A true

簡潔さを保つため、以下では判断ラベル true を省略する。従って、"Γ ⊢ π : A" となる。ここで、明確な証明でいくつかの結合子を再評価する。論理積については、論理積の証明の形式を見つけるために、その導入規則 ∧I を見てみる。それらは、2つの要素の証明の対となる。従って、次のようになる。

π₁ proof    π₂ proof
-------------------- pair-F
(π₁, π₂) proof

Γ ⊢ π₁ : A    Γ ⊢ π₂ : B
------------------------ ∧I
Γ ⊢ (π₁, π₂) : A ∧ B

除去規則 ∧E₁ と ∧E₂ は論理積の右か左のいずれかの要素を選択する。従って、証明は2つの投影（第一 = fst と第二 = snd）の対となる。

π proof
----------- fst-F
fst π proof

Γ ⊢ π : A ∧ B
------------- ∧E₁
Γ ⊢ fst π : A

π proof
----------- snd-F
snd π proof

Γ ⊢ π : A ∧ B
------------- ∧E₂
Γ ⊢ snd π : B

含意については、導入によって仮説の局所化（あるいは束縛）が形成され、これを λ を使って記述する。規則にある "Γ, u:A" は、仮説群 Γ に追加の仮説 u を加えることを意味する。

π proof
------------ λ-F
λu. π proof

Γ, u:A ⊢ π : B
----------------- ⊃I
Γ ⊢ λu. π : A ⊃ B

π₁ proof   π₂ proof
------------------- app-F
π₁ π₂ proof

Γ ⊢ π₁ : A ⊃ B    Γ ⊢ π₂ : A
---------------------------- ⊃E
Γ ⊢ π₁ π₂ : B

明確化された証明では、証明を処理し、論じることが可能となる。証明に関する重要な操作は、ある証明を別の証明の前提に置き換える操作である。これを一般に「代入定理; substitution theorem」と呼び、数学的帰納法によって証明可能である。

代入定理: Γ ⊢ π₁ : A かつ Γ, u:A ⊢ π₂ : B なら、 Γ ⊢ [π₁/u] π₂ : B である。

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

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

論理と同様、型理論には様々な拡張や変種があり、一階版も高階版もある。型理論の興味深い変種として依存型理論がある。これは、プログラム全体に量化を施せるものである。量化型は ∀ と ∃ の代わりに Π と Σ を使って記述する。構成規則は次のようになる。

Γ ⊢ A type    Γ, x:A ⊢ B type
----------------------------- Π-F
Γ ⊢ Πx:A. B type

Γ ⊢ A type  Γ, x:A ⊢ B type
---------------------------- Σ-F
Γ ⊢ Σx:A. B type

これらの型は矢印と積の型の一般化であり、導入規則と除去規則は次のようになる。

Γ, x:A ⊢ π : B
-------------------- ΠI
Γ ⊢ λx. π : Πx:A. B

Γ ⊢ π₁ : Πx:A. B   Γ ⊢ π₂ : A
----------------------------- ΠE
Γ ⊢ π₁ π₂ : [π₂/x] B

Γ ⊢ π₁ : A    Γ, x:A ⊢ π₂ : B
----------------------------- ΣI
Γ ⊢ (π₁, π₂) : Σx:A. B

Γ ⊢ π : Σx:A. B
---------------- ΣE₁
Γ ⊢ fst π : A

Γ ⊢ π : Σx:A. B
------------------------ ΣE₂
Γ ⊢ snd π : [fst π/x] B

普遍的な依存型理論は非常に強力であり、プログラムの想像可能ないかなる属性もプログラムの型で直接表すことができる。ただし、その普遍性と引き換えに、あるプログラムがある型であるかを決定不能となっている。このため、依存型理論を実際に使う場合、任意のプログラムの量化を許さないで、特定の決定可能な領域（整数、文字列、線形プログラムなど）のみを扱うことが多い。

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

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

古典論理と様相論理

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

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

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

-------------- XM₁
A ∨ ¬A true

¬¬A true
---------- XM₂
A true

-------- u
¬A true
⋮
p true
------ XM₃^{u, p}
A true

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

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

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

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

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

A valid
-------- ◻I
◻ A true

◻ A true
-------- ◻E
A true

なお、前提 "A valid" には定義規則がないが、その代わりに妥当性の断定的定義が使われる。この様相は、局所化された形式で仮説を明示的に示すとより明確になる。"Ω;Γ ⊢ A true" と記したとき、Γ は以前のように真なる仮説群を表し、Ω は妥当な仮説群を表す。右辺には単純な判断 "A true" しかない。"Ω ⊢ A valid" は定義から "Ω;⋅ ⊢ A true" と同じ意味であるため、妥当性はここでは不要である。導入規則と除去規則は次の通りである。

Ω;⋅ ⊢ π : A true
-------------------- ◻I
Ω;⋅ ⊢ box π : ◻ A true

Ω;Γ ⊢ π : ◻ A true
---------------------- ◻E
Ω;Γ ⊢ unbox π : A true

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

------------------------------- valid-hyp
Ω, u: (A valid) ; Γ ⊢ u : A true

様相代入定理: Ω;⋅ ⊢ π₁ : A true かつ Ω, u: (A valid) ; Γ ⊢ π₂ : C true ならば、 Ω;Γ ⊢ [π₁/u] π₂ : C true である。

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

脚注

↑ Gentzen, Untersuchungen über das logische Schließen (Mathematische Zeitschrift 39, pp.176-210, 1935)

参考文献

Jon Barwise and John Etchemendy, 2000. Language Proof and Logic. CSLI (University of Chicago Press) and New York: Seven Bridges Press.
Jean-Yves Girard (1990年). Proofs and Types, Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge, England. 翻訳と付録部分は Paul Taylor と Yves Lafont
Per Martin-Löf (1996年). “On the meanings of the logical constants and the justifications of the logical laws”. Nordic Journal of Philosophical Logic 1 (1): 11-60.
Frank Pfenning and Rowan Davies (2001年). “A judgmental reconstruction of modal logic”. Mathematical Structures in Computer Science 11 (4): 511-540.

外部リンク

Clemente, Daniel, "Introduction to natural deduction."
Domino On Acid. ドミノのゲームで自然演繹を視覚化したもの
Pelletier, Jeff, "A History of Natural Deduction and Elementary Logic Textbooks."
VII. 自然演繹（その1）高崎金久、京都大学大学院教授

[1] Gentzen, Untersuchungen über das logische Schließen (Mathematische Zeitschrift 39, pp.176-210, 1935)

[1]

自然演繹

Contents

自然演繹論理

背景

形式的定義

判断と命題

導入と除去

仮説的導出

一貫性、完全性、正規形

一階と高階の拡張

証明理論と型理論

古典論理と様相論理

関連項目

脚注

参考文献

外部リンク

案内メニュー

表示

個人用ツール

navigation

search

tool