自然演繹
(演繹論理学 から転送)
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/08/01 09:51 UTC 版)
自然演繹（しぜんえんえき、英: 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 における空集合の前提から証明可能な列
ある証明の例（モーダストレンス）:
| p → q, ¬q ⊢ ¬p [Modus Tollendo Tollens (MTT)] | |||
| 前提番号 | 行番号 | 論理式 (wff) | 根拠となる規則と使っている行 |
|---|---|---|---|
| 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 | |||
別の証明の例（排中律）:
| ⊢p ∨ ¬p | |||
| 前提番号 | 行番号 | 論理式 (wff) | 根拠となる規則と使っている行 |
|---|---|---|---|
| 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 の定式化に若干修正を施したものだが、ペール・マルティン＝レーフの影響もある。
形式的定義
演繹（または証明）は、命題論理のような形式体系の文脈では正確に定義できる。命題 α は、前提の集合 Σ に推論規則を繰り返し適用することで演繹される。演繹は、この推論規則の繰り返し適用の記録である。
より形式的には、命題の有限な列 β1 ,..., β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 という命題（形式的に記せば "
ここまで述べてきた論理は、単種（single-sorted）論理であり、一種類のオブジェクトだけを扱った命題からなる論理である。この単純なフレームワークの拡張としては、様々なものが提案されてきた。ここでは、個体（individuals）と項（term）という種を導入する。より正確に言えば、新たな判断 "t is a term"（または "t term"）を導入する（t は概略的な表現）。変項（variables）の可算無限集合 V と、関数シンボル（functions symbols）の可算無限集合 F を想定し、項を次のように構築する。
v ∈ V ------ var-F v term |
f ∈ F t1 term t2 term ... tn term
------------------------------------------ app-F
f (t1, t2, ..., tn) term
|
命題を表すため、述語（predicates）の第三の可算無限集合 P を想定し、項群に対する原子述語を次のように定式化する。
φ ∈ P t1 term t2 term ... tn term
------------------------------------------ pred-F
φ (t1, t2, ..., tn) prop
|
さらに、2種類の量化（全称量化 (∀) と存在量化 (∃)）を導入する。
------ u
x term
⋮
A prop
---------- ∀Fu
∀x. A prop
|
------ u
x term
⋮
A prop
---------- ∃Fu
∃x. A prop
|
このような量化された命題には、次のような導入規則と除去規則がある。
------ u
a term
⋮
[a/x] A true
------------ ∀Iu, 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
-------------------------- ∃Ea, u,v
C true
|
これらの規則で、[t/x] A と書かれている部分は、A に存在する全ての x の実体を t と置換することを意味する（詳しくはラムダ計算を参照されたい）。規則名の上付き文字は、その規則によって排除される要素を意味している。a という項は ∀I の結論には出現しない（このような項をパラメータと呼ぶ）。また、規則 ∃E における仮説名 u と v は、仮説的導出の第二前提に局所化されている。これまでの節で論じてきた命題論理は決定可能だったが、量化子を加えたことで決定不能となる。
ここまで述べた量化表現は「一階; first-order」である。その場合、量化されるオブジェクトと命題は区別される。高階論理ではその部分が異なり、命題は区別されない。命題の量化には量化の範囲があり、それが規則にも反映される。
------ u
p prop
⋮
A prop
---------- ∀Fu
∀p. A prop
|
------ u
p prop
⋮
A prop
---------- ∃Fu
∃p. A prop
|
高階論理における導入規則と除去規則は、ここでは扱わない。一階論理と高階論理の間には様々な段階がある。例えば、二階論理は、項を量化した命題と、命題を量化したものを命題として扱う。
証明理論と型理論
ここまでの説明は、命題の性質に重きを置いており、「証明」の形式的定義をしていなかった。証明を形式的に記述するには、仮説的導出の記法を若干変える必要がある。前件に（変項の無限可算集合 V から）「証明変項; proof variables」によるラベルを付け、後件を実際の証明で装飾する。前件あるいは仮説はターンスタイル(⊢)を挟んで、後件の前に記される。このような変形を「局所化仮説; localized hypotheses」と呼ぶこともある。以上の変更を図にまとめると次のようになる。
---- u1 ---- u2 ... ---- un
J1 J2 Jn
⋮
J
|
⇒ | u1:J1, u2:J2, ..., un:Jn ⊢ 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つの要素の証明の対となる。従って、次のようになる。
π1 proof π2 proof -------------------- pair-F (π1, π2) proof |
Γ ⊢ π1 : A Γ ⊢ π2 : B ------------------------ ∧I Γ ⊢ (π1, π2) : A ∧ B |
除去規則 ∧E1 と ∧E2 は論理積の右か左のいずれかの要素を選択する。従って、証明は2つの投影（第一 = fst と 第二 = snd）の対となる。
π proof ----------- fst-F fst π proof |
Γ ⊢ π : A ∧ B ------------- ∧E1 Γ ⊢ fst π : A |
|
π proof ----------- snd-F snd π proof |
Γ ⊢ π : A ∧ B ------------- ∧E2 Γ ⊢ snd π : B |
含意については、導入によって仮説の局所化（あるいは束縛）が形成され、これを λ を使って記述する。規則にある "Γ, u:A" は、仮説群 Γ に追加の仮説 u を加えることを意味する。
π proof ------------ λ-F λu. π proof |
Γ, u:A ⊢ π : B ----------------- ⊃I Γ ⊢ λu. π : A ⊃ B |
|
π1 proof π2 proof ------------------- app-F π1 π2 proof |
Γ ⊢ π1 : A ⊃ B Γ ⊢ π2 : A ---------------------------- ⊃E Γ ⊢ π1 π2 : B |
明確化された証明では、証明を処理し、論じることが可能となる。証明に関する重要な操作は、ある証明を別の証明の前提に置き換える操作である。これを一般に「代入定理; substitution theorem」と呼び、数学的帰納法によって証明可能である。
- 代入定理
- Γ ⊢ π1 : A かつ Γ, u:A ⊢ π2 : B なら、 Γ ⊢ [π1/u] π2 : 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 |
Γ ⊢ π1 : Πx:A. B Γ ⊢ π2 : A ----------------------------- ΠE Γ ⊢ π1 π2 : [π2/x] B |
Γ ⊢ π1 : A Γ, x:A ⊢ π2 : B ----------------------------- ΣI Γ ⊢ (π1, π2) : Σx:A. B |
Γ ⊢ π : Σx:A. B ---------------- ΣE1 Γ ⊢ fst π : A |
Γ ⊢ π : Σx:A. B ------------------------ ΣE2 Γ ⊢ snd π : [fst π/x] B |
普遍的な依存型理論は非常に強力であり、プログラムの想像可能ないかなる属性もプログラムの型で直接表すことができる。ただし、その普遍性と引き換えに、あるプログラムがある型であるかを決定不能となっている。このため、依存型理論を実際に使う場合、任意のプログラムの量化を許さないで、特定の決定可能な領域（整数、文字列、線形プログラムなど）のみを扱うことが多い。
依存型理論では型がプログラムに依存することを許すのだが、そこから自然に生じる疑問として、プログラムが型に依存するとか他の組合せの依存は可能か、というものがある。この疑問には様々な答えがある。一般的な手法はプログラムを型に関して量化するもので、「パラメトリック・ポリモルフィズム」と呼ぶ。これは、型とプログラムを明確に区別する「断定的ポリモルフィズム」と、両者の区別があいまいな「非断定的ポリモルフィズム」に分類される。依存性とポリモルフィズムの組合せは様々なものが考えられ、Henk Barendregt の ラムダ・キューブが有名である。
論理と型理論の境界領域は、研究が盛んな分野である。新たな論理は、論理フレームワークとして型理論的設定で形式化されることが多い。そのような論理フレームワークとして、calculus of constructions や LF は高階依存型理論に基づいており、決定可能性と表現能力のトレードオフを考慮して考案されている。これらの論理フレームワーク自体は常に自然演繹体系に則っており、自然演繹手法の汎用性を示している。
古典論理と様相論理
話を単純化するため、ここまでの説明では直観論理を使ってきた。古典論理は、直観論理に次の公理あるいは排中律を追加して拡張したものと言える。
- 「任意の命題 p について、命題 p ∨ ¬p は真である」
この文自体は、導入も除去も明確でない。実は、これは2種類の連結子に関係している。ゲンツェンは、排中律を以下の3つの（等価な）定式化のうちの1つとして扱った。これらはヒルベルトと Arend Heyting の論理体系にも類似の形式で提示されていた。
-------------- XM1 A ∨ ¬A true |
¬¬A true ---------- XM2 A true |
-------- u
¬A true
⋮
p true
------ XM3u, 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
|
- 様相代入定理
- Ω;⋅ ⊢ π1 : A true かつ Ω, u: (A valid) ; Γ ⊢ π2 : C true ならば、 Ω;Γ ⊢ [π1/u] π2 : 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） 高崎金久、京都大学大学院教授
- 自然演繹のページへのリンク
