正規化定理(自然演繹)
概要
正規化定理(自然演繹)（normalization theorem for natural deduction）とは、自然演繹の導出から、導入規則で作った論理式をすぐ除去規則で壊す遠回りを有限回の変換ですべて取り除き、同じ結論を同じかより少ない仮定から導く正規な導出が得られるという定理である。連言・含意・否定と矛盾の規則の体系では、正規な導出に現れる論理式はどれも結論か仮定の部分論理式であり、そこから無矛盾性や保存性が従う。選言を加えると交換変換が要る。
自然演繹 の導出には「遠回り」がありうる。たとえば $A$ と $B$ の導出から $\land\mathrm I$ で $A\land B$ を作り、すぐに $\land\mathrm E$ で $A$ を取り出すのは、最初から $A$ の導出を使えば済む回り道である。$A$ を仮定して $B$ を導き $\to\mathrm I$ で $A\to B$ を作り、すぐに $\to\mathrm E$ で $A$ の導出と組み合わせて $B$ を得るのも、仮定 $A$ の場所に $A$ の導出を差し込めば省ける。正規化定理（normalization theorem）は、このような遠回りをすべて取り除けること、すなわちどの導出も、同じ結論を同じかより少ない仮定から導く 正規な導出 に変形できることを述べる。
正規な導出は形がよく分かる。そこに現れる論理式はどれも、結論か仮定の 部分論理式 である（部分論理式性）。このことから、何も仮定せずに $\bot$ を導く導出がないこと（無矛盾性）や、$\land$ と $\to$ だけの論理式は $\land$ と $\to$ の規則だけで証明できること（保存性）がすぐに従う。自然演繹の正規化は、Prawitz が選言や量化記号を含む体系まで詳しく展開した証明論の基本的な道具で（GLT89 §10.5、p. 78）、型理論 の Curry–Howard 対応を通じて、型付きラムダ計算の項の計算（β 簡約）と同じものになる。
この記事では、自然演繹の規則のうち $\land$・$\to$・$\lnot$ と $\bot_{\mathrm I}$ の規則からなる体系で、正規化定理と部分論理式性を完全に証明する。選言 $\lor$ を加えると、遠回りの取り除き方に新しい種類の変換が要ることを例で示し、その場合の結果は引用で述べる。
設定
論理式・推論規則・導出・開いた仮定の集合 $\mathrm{Open}(D)$・結論 $\mathrm{concl}(D)$ は 自然演繹 の記事の節「定義」と定義「自然演繹の導出」のとおりとする。とくに、仮定を外す規則は、その前提の導出の開いた仮定のうち外せるものをすべて外す。この記事では、そのうち次の 7 つの規則だけを使う体系を $\mathbf{NJ}^{-}$ と書く。
$$
\dfrac{A\qquad B}{A\land B}\ {\scriptstyle\land\mathrm I}\qquad
\dfrac{A\land B}{A}\ {\scriptstyle\land\mathrm E}\qquad
\dfrac{A\land B}{B}\ {\scriptstyle\land\mathrm E}\qquad
\dfrac{\begin{array}{c}[A]^{n}\\ \vdots\\ B\end{array}}{A\to B}\ {\scriptstyle\to\mathrm I^{n}}\qquad
\dfrac{A\to B\qquad A}{B}\ {\scriptstyle\to\mathrm E}
$$
$$
\dfrac{\begin{array}{c}[A]^{n}\\ \vdots\\ \bot\end{array}}{\lnot A}\ {\scriptstyle\lnot\mathrm I^{n}}\qquad
\dfrac{\lnot A\qquad A}{\bot}\ {\scriptstyle\lnot\mathrm E}\qquad
\dfrac{\bot}{A}\ {\scriptstyle\bot_{\mathrm I}}
$$
$\lor\mathrm I$・$\lor\mathrm E$ と背理法 $\bot_{\mathrm C}$ は使わない。$\bot_{\mathrm C}$ を除いた自然演繹は直観主義論理の体系であり（自然演繹 の記事の節「背理法の規則の役割」）、$\mathbf{NJ}^{-}$ はその $\lor$ を含まない部分である。導出は論理式の 出現（木の頂点）からなり、同じ論理式が木の別の場所に何度も現れうる。以下「論理式」と言うとき、文脈によって出現を指す。
- 除去規則 $\land\mathrm E$・$\to\mathrm E$・$\lnot\mathrm E$ の前提のうち、除去される結合子をもつもの（$A\land B$、$A\to B$、$\lnot A$）を 主前提、それ以外（$\to\mathrm E$・$\lnot\mathrm E$ の $A$）を 副前提 という。
- 導出の中の論理式の出現が 極大論理式 であるとは、それが導入規則 $\land\mathrm I$・$\to\mathrm I$・$\lnot\mathrm I$ か $\bot_{\mathrm I}$ の結論であり、同時に除去規則の主前提であることをいう。
- 極大論理式を含まない導出を 正規 な導出という。
極大論理式は、作った直後に壊す遠回りの跡である。$\bot_{\mathrm I}$ の結論も数えるのは、$\bot$ から一度に複雑な論理式を導いてからそれを分解するのも、分解した後の論理式を直接 $\bot_{\mathrm I}$ で導けば済む遠回りだからである。導入規則の結論が副前提になっているのは遠回りではない。
論理式の 次数 $g(A)$ を、$A$ に現れる結合子 $\land,\to,\lnot$ の個数とする（命題変数と $\bot$ の次数は $0$）。論理式の 部分論理式 を、$A$ 自身と、$A=B\land C$ または $A=B\to C$ なら $B,C$ の部分論理式、$A=\lnot B$ なら $B$ の部分論理式と $\bot$、と帰納的に定める。$\lnot B$ の部分論理式に $\bot$ を入れるのは、$\lnot B$ が $B\to\bot$ と同じ規則の形をもつからである。主前提の次数は $1$ 以上なので、極大論理式の次数も $1$ 以上である。
変換
極大論理式を取り除く操作を定める。そのために、導出の仮定の場所に別の導出を差し込む操作を用意する。
導出 $D$、論理式 $A$、結論が $A$ の導出 $E$ について、$D$ の葉のうち開いた仮定である $A$（根までの道の途中で外されていない $A$ の出現）をすべて $E$ に置き換えた木を $D[E/A]$ と書く。正確には $D$ の組み立てについて帰納的に、$D$ が仮定 $A$ だけなら $E$、ほかの仮定だけなら $D$ 自身とし、$D$ の最後の規則の各前提の導出 $D_i$ について、その規則が $D_i$ の仮定 $A$ を外すなら $D_i$ のまま、外さないなら $D_i[E/A]$ に替える。
- $D[E/A]$ は導出で、結論は $\mathrm{concl}(D)$ であり、$\mathrm{Open}(D[E/A])\subset(\mathrm{Open}(D)\setminus\{A\})\cup\mathrm{Open}(E)$ である（$\mathrm{Open}(D)$ に $A$ がなければ $D[E/A]=D$）。
- 導出 $D$ の中の部分導出 $D_0$ を、同じ結論をもち $\mathrm{Open}(D_0')\subset\mathrm{Open}(D_0)$ を満たす導出 $D_0'$ に置き換えた木 $D'$ は導出で、結論は $\mathrm{concl}(D)$、$\mathrm{Open}(D')\subset\mathrm{Open}(D)$ である。
どちらも導出の組み立てについての帰納法である。規則が使えるかどうかは前提の結論だけで決まり、仮定を外す規則は「外せるものを外す」だけなので、開いた仮定が減っても規則は使えたままである。
詳細
1：$D$ が仮定だけのときは定義どおりである。最後の規則を $r$、前提の導出を $D_1,\dots,D_k$ とし、$D_i':=D_i$（$r$ が $D_i$ の仮定 $A$ を外すとき）または $D_i[E/A]$（そうでないとき）とする。帰納法の仮定により $D_i'$ の結論は $D_i$ と同じなので、$r$ を同じ形で使える。$r$ が $D_i$ について外す論理式を $X_i$（ない場合は空）とすると、$\mathrm{Open}(D_i')\setminus\{X_i\}$ は、$X_i=A$ なら $\mathrm{Open}(D_i)\setminus\{A\}$ に等しく、そうでなければ帰納法の仮定により $(\mathrm{Open}(D_i)\setminus\{A,X_i\})\cup(\mathrm{Open}(E)\setminus\{X_i\})$ に含まれる。$\mathrm{Open}(D[E/A])$ はこれらの和なので主張が従う。$r$ が $\mathrm{Open}(E)$ の元を外すこともあるが、そのとき開いた仮定はさらに減るだけである。
2：$D_0=D$ なら明らかである。そうでなければ $D_0$ は最後の規則のある前提の導出 $D_i$ の中にあり、帰納法の仮定により $D_i$ を置き換えた $D_i'$ は同じ結論の導出で $\mathrm{Open}(D_i')\subset\mathrm{Open}(D_i)$ である。最後の規則は同じ形で使え、外す論理式を除いた和をとっても包含は保たれる。$\square$
極大論理式 $F$ が主前提である除去規則の適用と、$F$ を結論とする規則の適用を合わせた部分導出を、次のように置き換える操作を 変換 という（$D_1,D_2,D_3$ は前提の導出）。
- （$\land$）$D_1$（結論 $A$）と $D_2$（結論 $B$）から $\land\mathrm I$ で $A\land B$、$\land\mathrm E$ で $A$ を得る部分を $D_1$ に置き換える。$B$ を取り出す場合は $D_2$ に置き換える。
- （$\to$）$D_1$（仮定 $A$ を外す前の結論 $B$）から $\to\mathrm I$ で $A\to B$、それと $D_2$（結論 $A$）から $\to\mathrm E$ で $B$ を得る部分を $D_1[D_2/A]$ に置き換える。
- （$\lnot$）$D_1$（仮定 $A$ を外す前の結論 $\bot$）から $\lnot\mathrm I$ で $\lnot A$、それと $D_2$（結論 $A$）から $\lnot\mathrm E$ で $\bot$ を得る部分を $D_1[D_2/A]$ に置き換える。
- （$\bot_{\mathrm I}$）$D_3$（結論 $\bot$）から $\bot_{\mathrm I}$ で $F$ を得て、$F$ を主前提とする除去規則で $C$ を得る部分を、$C\ne\bot$ なら $D_3$ から $\bot_{\mathrm I}$ で $C$ を得る導出に、$C=\bot$（$F=\lnot A$ で $\lnot\mathrm E$ の場合のほか、$\land\mathrm E$・$\to\mathrm E$ で $\bot$ を取り出す場合もある）なら $D_3$ に置き換える。副前提の導出は捨てる。
2 の $D_1[D_2/A]$ では、$A$ の導出 $D_2$ が仮定 $A$ の出現の数だけ複製される。lem-nd-subst により、変換の前後で結論は変わらず、開いた仮定の集合は大きくならない。
命題変数 $p$ について、次の導出 $D$ は $\vdash p\to p$ を示している。
$$
\dfrac{\dfrac{[p\to p]^{1}}{(p\to p)\to(p\to p)}\ {\scriptstyle\to\mathrm I^{1}}\qquad\dfrac{[p]^{2}}{p\to p}\ {\scriptstyle\to\mathrm I^{2}}}{p\to p}\ {\scriptstyle\to\mathrm E}
$$
（左の $\to\mathrm I^{1}$ は仮定 $p\to p$ だけからなる導出に当てたもの、右の $\to\mathrm I^{2}$ は仮定 $p$ だけからなる導出に当てたものである。）論理式 $(p\to p)\to(p\to p)$ は $\to\mathrm I$ の結論で $\to\mathrm E$ の主前提なので極大論理式であり、$D$ は正規でない。変換 2 を当てると、仮定 $p\to p$ の場所に右の導出が入り、$\to\mathrm I^{2}$ で $p$ から $p\to p$ を導く正規な導出になる。$D$ には $p\to p$ の部分論理式でない $(p\to p)\to(p\to p)$ が現れるが、変換の後には現れない。
正規化定理
変換を 1 回行うと、取り除いた極大論理式の代わりに新しい極大論理式が生じることがある。2 の変換で $D_2$ の結論が導入規則の結論で、$D_1$ の中で仮定 $A$ が除去規則の主前提だった場合などである。しかし新しく生じる極大論理式の次数は、取り除いたものより真に小さい。このことを使って、変換を行う場所をうまく選べば有限回で終わることを示す。
$\mathbf{NJ}^{-}$ の任意の導出 $D$ は、有限回の変換で正規な導出 $D^*$ に変形できる。$D^*$ の結論は $D$ と同じで、$\mathrm{Open}(D^*)\subset\mathrm{Open}(D)$ である。とくに、$\mathbf{NJ}^{-}$ で $\Gamma\vdash A$ ならば、結論が $A$ で開いた仮定が $\Gamma$ に含まれる正規な導出がある。
極大論理式の次数の最大値 $d$ と、その次数の極大論理式の個数 $m$ の組 $(d,m)$ が、うまく選んだ変換で辞書式に減ることを示す。選ぶのは、次数 $d$ の極大論理式のうち、その上に次数 $d$ の極大論理式をもたないものである。
詳細
導出 $D$ の極大論理式の次数の最大値を $d(D)$（正規なら $0$）、次数 $d(D)$ の極大論理式の出現の個数を $m(D)$ とする。$D$ が正規でないとし、$d:=d(D)\ge1$ とおく。次数 $d$ の極大論理式 $F$ ごとに、$F$ を主前提とする除去規則の結論で終わる部分導出を $D_F$ とする。$F'\ne F$ が次数 $d$ の極大論理式で $D_F$ の中にあれば、$F'$ は $D_F$ の根ではない（根は除去規則の結論で、導入規則や $\bot_{\mathrm I}$ の結論ではない）ので、$F'$ を主前提とする規則も $D_F$ の中にあり、$D_{F'}$ は $D_F$ の真の部分である。よって $D_F$ の頂点の個数が最小の $F$ を選べば、$D_F$ の中に $F$ 以外の次数 $d$ の極大論理式はない。
$D_F$ に変換を当て、置き換えた導出を $R$、全体を $D'$ とする。論理式の出現が極大論理式かどうかは、それを結論とする規則と、それを前提とする規則だけで決まる。$D'$ の極大論理式は次のどれかである。
(i) $D_F$ の外の出現。$D_F$ の根の位置を除けば、両側の規則は変わらないので、極大かどうかも次数も $D$ と同じである。
(ii) $D_F$ の根の位置の出現 $C$（$R$ の結論）。$R$ の最後の規則が変わるので新しく極大になりうるが、$C$ は $F$ の真の部分論理式（変換 1 の $A$ または $B$、変換 2 の $B$、変換 4 で除去規則の結論）であるか、$\bot$（変換 3 と、変換 4 の $C=\bot$）である。前者なら次数は $d$ より小さく、後者なら $\bot$ はどの除去規則の主前提にもならないので極大でない。
(iii) $R$ の内部の出現。$R$ は $D_1$・$D_2$・$D_3$ の出現と、変換 2・3 で $D_2$ を差し込んだ場所の出現からなる。$D_1,D_2,D_3$ の内部の極大論理式は $D_F$ の中にあったので、次数は $d$ より小さい（$D_2$ が複製されても次数 $d$ のものは増えない）。差し込んだ場所の出現は仮定 $A$ の位置にある論理式 $A$ で、$A\to B$ や $\lnot A$ の真の部分論理式なので、極大になっても次数は $d$ より小さい。変換 4 で新しく置いた $\bot_{\mathrm I}$ の結論は (ii) の $C$ である。
$F$ 自身は消える。よって $D'$ の次数 $d$ 以上の極大論理式は、(i) の次数 $d$ のもの $m-1$ 個だけで、$d(D')< d$ であるか、$d(D')=d$ かつ $m(D')=m-1$ である。自然数の組の辞書式順序は整礎なので、この操作は有限回で正規な導出に達する。結論と開いた仮定の主張は、各段で lem-nd-subst による。$\square$
この証明の選び方は、型付きラムダ計算の弱正規化定理（型理論 の定理「弱正規化定理」）の証明と同じで、GLT89 §4.3（pp. 24–26）の方法である。極大論理式を選ぶ順序を指定しない場合、すなわちどの順で変換を行っても必ず有限回で終わるという 強い正規化 も成り立つ。含意だけの部分では、型理論 の定理「Curry–Howard対応」の下で変換 2 は β 簡約にあたり、強正規化定理 がこれを与える。$\lor$ や量化記号を含む体系での強い正規化は GLT89 §10.5（pp. 78–79）が主張を述べている（この記事では証明しない）。
部分論理式性
正規な導出では、除去規則の主前提は導入規則や $\bot_{\mathrm I}$ から来ないので、仮定から下へ除去規則をたどる道は論理式を分解するだけである。この道を 主枝 という。
$D$ を $\mathbf{NJ}^{-}$ の正規な導出とする。
- $D$ に現れる論理式はどれも、$\mathrm{concl}(D)$ か、$\mathrm{Open}(D)$ のある元の部分論理式である。
- $D$ が仮定だけからなるか、最後の規則が除去規則ならば、$\mathrm{concl}(D)$ は $\mathrm{Open}(D)$ のある元の部分論理式である。
- $\mathrm{concl}(D)=\bot$ ならば、$\bot$ は $\mathrm{Open}(D)$ のある元の部分論理式である。
$D$ の組み立てについての帰納法で 1〜3 を同時に示す。正規な導出の部分導出も正規である。
詳細
仮定だけ． $D$ が仮定 $A$ だけなら $\mathrm{Open}(D)=\{A\}$ で、1〜3 は明らかである。
除去規則． 最後の規則が除去規則で、主前提の導出を $D_1$ とする。$D$ は正規なので主前提は導入規則や $\bot_{\mathrm I}$ の結論でなく、$D_1$ は仮定だけか除去規則で終わる。帰納法の仮定の 2 により $\mathrm{concl}(D_1)$ は $\mathrm{Open}(D_1)\subset\mathrm{Open}(D)$ のある元 $G$ の部分論理式であり、1 により $D_1$ の論理式は $\mathrm{concl}(D_1)$ か $\mathrm{Open}(D_1)$ の元の部分論理式、したがって $\mathrm{Open}(D)$ の元の部分論理式である。$\mathrm{concl}(D)$ は主前提 $A\land B$・$A\to B$・$\lnot A$ の部分論理式（$A$・$B$・$\bot$）なので $G$ の部分論理式で、2 と 3 が成り立つ。副前提の導出 $D_2$（結論 $A$）の論理式は $A$ か $\mathrm{Open}(D_2)\subset\mathrm{Open}(D)$ の元の部分論理式で、$A$ は主前提の部分論理式である。除去規則は仮定を外さないので、1 も成り立つ。
導入規則． $\land\mathrm I$ なら前提 $A$・$B$ は結論 $A\land B$ の部分論理式で、前提の導出に帰納法の仮定の 1 を当てればよい。$\to\mathrm I$ なら前提の導出 $D_1$ は結論 $B$、$\mathrm{Open}(D_1)\subset\mathrm{Open}(D)\cup\{A\}$ で、$A$ と $B$ は $A\to B$ の部分論理式である。$\lnot\mathrm I$ なら前提の導出の結論は $\bot$、開いた仮定は $\mathrm{Open}(D)\cup\{A\}$ に含まれ、$\bot$ と $A$ は $\lnot A$ の部分論理式である。いずれも 1 が成り立つ。導入規則の結論は $\bot$ でないので、3 は自明であり、2 は仮定に当たらない。
$\bot_{\mathrm I}$． 前提の導出 $D_0$ の結論は $\bot$ で、$\mathrm{Open}(D_0)=\mathrm{Open}(D)$ である。帰納法の仮定の 3 により $\bot$ は $\mathrm{Open}(D)$ の元の部分論理式であり、1 により $D_0$ の論理式は $\bot$ か $\mathrm{Open}(D)$ の元の部分論理式である。結論 $C$ は $\mathrm{concl}(D)$ そのものなので 1 が成り立つ。$C=\bot$ なら 3 も成り立つ。$\square$
2 の主枝は、GLT89 §10.3.1（p. 75）が $\land,\to,\forall$ の体系で述べる principal branch と同じものである。部分論理式性から、次の帰結が直ちに従う。
- （無矛盾性）$\mathbf{NJ}^{-}$ で $\vdash\bot$ ではない。より一般に、開いた仮定のない正規な導出の最後の規則は導入規則である。
- （保存性）$\Gamma$ と $A$ が $\lnot$ と $\bot$ を含まない論理式からなるとき、$\mathbf{NJ}^{-}$ で $\Gamma\vdash A$ ならば、$\land\mathrm I$・$\land\mathrm E$・$\to\mathrm I$・$\to\mathrm E$ だけを使う導出で $\Gamma\vdash A$ である。
1：$\vdash\bot$ の導出があれば、thm-nd-normalization により開いた仮定のない正規な導出がある。thm-nd-subformula の 3 により $\bot$ は空集合のある元の部分論理式となって矛盾する。開いた仮定のない正規な導出 $D$ が仮定だけか除去規則で終わるなら、同定理の 2 により $\mathrm{Open}(D)$ は空でなく、$\bot_{\mathrm I}$ で終わるなら前提の導出に 3 を当てて同じ矛盾になる。よって最後の規則は導入規則である。2：正規な導出 $D$ をとると、$D$ の論理式はすべて $A$ か $\Gamma$ の元の部分論理式で、$\lnot,\bot$ を含まない（$\lnot$ と $\bot$ を含まない論理式の部分論理式は $\lnot$ も $\bot$ も含まない）。$\lnot\mathrm I$ の結論、$\lnot\mathrm E$ の主前提は $\lnot$ を含み、$\bot_{\mathrm I}$ の前提は $\bot$ なので、これらの規則は $D$ に現れない。$\square$
1 の後半から、たとえば命題変数 $p$ は $\mathbf{NJ}^{-}$ で証明できない（$p$ を結論とする導入規則はない）。2 は、否定や矛盾の規則を使っても、それらを含まない論理式について新しい定理は増えないことを述べている。
選言を加えた体系
$\lor\mathrm E$ を加えると、def-nd-maximal の意味で正規でも部分論理式性が成り立たない導出が現れる。$\lor\mathrm E$ の結論 $C$ は主前提 $A\lor B$ と関係のない論理式で、それが次の除去規則の主前提になると、作ってから壊す遠回りが $\lor\mathrm E$ をはさんで隠れてしまうからである。
命題変数 $p$ について、次の導出は $\{p\lor p\}\vdash p$ を示す（GLT89 §10.3.2、p. 76 の例）。
$$
\dfrac{\dfrac{p\lor p\qquad\dfrac{[p]^{1}\quad[p]^{1}}{p\land p}\ {\scriptstyle\land\mathrm I}\qquad\dfrac{[p]^{1}\quad[p]^{1}}{p\land p}\ {\scriptstyle\land\mathrm I}}{p\land p}\ {\scriptstyle\lor\mathrm E^{1}}}{p}\ {\scriptstyle\land\mathrm E}
$$
$\land\mathrm E$ の主前提 $p\land p$ は $\lor\mathrm E$ の結論で、導入規則の結論ではないので、極大論理式はない。しかし $p\land p$ は結論 $p$ の部分論理式でも、開いた仮定 $p\lor p$ の部分論理式でもない。
この遠回りは、$\lor\mathrm E$ の下にある除去規則を $\lor\mathrm E$ の 2 つの枝の中へ持ち上げる 交換変換（commuting conversion）で取り除ける。上の例では、$\land\mathrm E$ を両方の枝の $p\land p$ の下に移すと、各枝に $\land\mathrm I$ の直後の $\land\mathrm E$ という極大論理式が現れ、変換 1 で消えて、$p\lor p$ と 2 つの仮定 $[p]^{1}$ から $\lor\mathrm E^{1}$ で $p$ を導く導出になる。交換変換を加え、$\lor\mathrm E$ の結論が除去規則の主前提になる場合も遠回りに数えると、選言と量化記号を含む直観主義論理の自然演繹でも正規化定理と部分論理式性が成り立つ（GLT89 §10.4–§10.5、pp. 76–79。詳細は Prawitz による。この記事では証明しない）。
反例：条件を外すと成り立たない
| 外す条件 | 反例 | 成り立たなくなること |
|---|---|---|
| 導出が正規（thm-nd-subformula） | ex-nd-detour の導出 $D$ | 部分論理式性 |
| $\bot_{\mathrm I}$ の結論も極大論理式に数える（def-nd-maximal） | $\bot$ から $\bot_{\mathrm I}$ で $p\land q$、$\land\mathrm E$ で $p$ | 部分論理式性 |
| 体系に $\lor\mathrm E$ がない（変換が 1〜4 だけで足りる） | ex-nd-disjunction の導出 | 部分論理式性 |
どの行も、結論と開いた仮定の部分論理式でない論理式が現れることを確かめればよい。
詳細
1 行目：$D$ の結論は $p\to p$、開いた仮定はない。$(p\to p)\to(p\to p)$ は $p\to p$ の部分論理式（$p\to p$ と $p$）でない。変換 2 で取り除ける極大論理式があるので、$D$ は正規でない。
2 行目：仮定 $\bot$ から $\bot_{\mathrm I}$ で $p\land q$ を導き、$\land\mathrm E$ で $p$ を得る導出の結論は $p$、開いた仮定は $\{\bot\}$ である。$p\land q$ は $p$ の部分論理式でも $\bot$ の部分論理式でもない。$\bot_{\mathrm I}$ の結論を極大論理式に数えなければ、この導出には極大論理式がなく、正規と呼ぶことになってしまう。変換 4 を当てると、$\bot$ から $\bot_{\mathrm I}$ で直接 $p$ を導く導出になる。
3 行目：ex-nd-disjunction のとおりである。$\land$・$\lnot$・$\to$・$\bot_{\mathrm I}$ だけの体系では、除去規則の結論はいつも主前提の部分論理式なので、このような隠れた遠回りは起こらない。
関連項目
- 前提: 自然演繹, 命題論理, 強正規化定理
- 比較: 型理論, シークエント計算, 直観主義論理, Gentzenの無矛盾性証明
- 発展: 線形論理, Martin-Löf型理論
参考文献
Mathpediaは寄付と、参考文献の書籍リンク（Amazonアソシエイト）の紹介料で運営されています。 支援について ／ 寄付する
