仮説的導出
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/08/01 09:51 UTC 版)
数理論理学での一般的操作として、「仮定からの推論; 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 から導出可能である」となる。もちろん、この例では導出過程は明らかだが、一般に導出が自明とは限らない。仮設的導出の一般形は次のようになる。 D 1 D 2 ⋯ D n ⋮ J {\displaystyle {\begin{matrix}D_{1}\quad D_{2}\cdots D_{n}\\\vdots \\J\end{matrix}}} 仮説的導出には、先頭行に書かれた前件群（Di、antecedent derivations）と最終行に書かれた1つの後件判断（J、succedent judgement）がある。それぞれの前提が仮説的導出の結果となっている場合もある。以下、判断（judgement）は前提のない導出として扱う。 仮説的判断の考え方は、含意の結合子に利用される。含意の導入規則と除去規則は次のようになる。 A t r u e u ⋮ B t r u e A ⊃ B t r u e ⊃ I u A ⊃ B t r u e A t r u e B t r u e ⊃ E {\displaystyle {\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} 導入規則では、前件 u は結論には現れない。これは仮説の「範囲」を限定する機構であり、その存在理由は "B true" を確立することにある。それ以外の目的で使うことはできず、特に導入後に使うことはできない。例として、"A ⊃ (B ⊃ (A ∧ B)) true" の導出を示す。 A t r u e u B t r u e w A ∧ B t r u e ∧ I B ⊃ ( A ∧ B ) t r u e A ⊃ ( B ⊃ ( A ∧ B ) ) t r u e ⊃ I u ⊃ I w {\displaystyle {\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}} この導出過程には前提が満足されないということはないが、それぞれの導出は仮説的である。例えば、"B ⊃ (A ∧ B) true" の導出は（uと名づけられた）前件 "A true" を仮説としている。 仮説的導出を使うと、論理和の除去規則を書くことができる。 A ∨ B true A t r u e u ⋮ C t r u e B t r u e w ⋮ C t r u e C t r u e ∨ E u , w {\displaystyle {\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}} これを説明すると、A ∨ B が真で、A true と B true それぞれから C true が導かれるなら、C は必ず真となる。ここで、A true や B true を保証しているわけではないことに注意されたい。偽については、次の除去規則が得られる。 ⊥ t r u e C t r u e ⊥ E {\displaystyle {\frac {\perp true}{C\ true}}\perp E} これを解釈すると、偽が真であれば、任意の命題 C が真である、ということになる。 否定については、含意と類似している。 A t r u e u ⋮ p t r u e ¬ A t r u e ¬ I u , p ¬ A t r u e A t r u e C t r u e ¬ E {\displaystyle {\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} 導入規則では、仮説 u も後件 p も結論に現れない。これら規則は概略的なので、この導入規則を解釈すると、"A true" から任意の命題 p について "p true" であることを導ける場合、A は偽である（すなわち "not A true"）、ということになる。除去規則については、A と not A が共に真である場合、矛盾が生じ、あらゆる命題 C が真となる。含意と否定の規則がよく似ているため、not A と A ⊃ ⊥ が等価（互いにもう一方を導出可能）であることは容易にわかる。
※この「仮説的導出」の解説は、「自然演繹」の解説の一部です。
「仮説的導出」を含む「自然演繹」の記事については、「自然演繹」の概要を参照ください。
- 仮説的導出のページへのリンク
