演繹定理

同義語：deduction theorem構文論的演繹定理

概要

前提知識: 一階論理の証明体系, 命題論理, 含意

演繹定理（deduction theorem）とは、Hilbert 流の証明体系について、論理式の集合 $\Gamma$ と論理式 $\alpha,\beta$ に対し
$$ \Gamma\cup\{\alpha\}\vdash\beta\quad\Longleftrightarrow\quad\Gamma\vdash\alpha\to\beta $$
が成り立つという定理である。推論規則が前件肯定（modus ponens）だけで、公理に $\alpha\to(\beta\to\alpha)$ と $(\alpha\to(\beta\to\gamma))\to((\alpha\to\beta)\to(\alpha\to\gamma))$ の形の論理式がすべて含まれていれば成り立つ。
数学で「$\alpha$ ならば $\beta$」を示すときは、ふつう「$\alpha$ を仮定して $\beta$ を導く」。Hilbert 流の体系には「仮定を置いて、あとで外す」という規則がないので、この普通の証明の形がそのまま使えるかどうかは自明ではない。演繹定理は、仮定 $\alpha$ を使った導出を、仮定を使わずに $\alpha\to\beta$ を導く導出へ機械的に書き換えられることを保証する。これは体系の中の定理ではなく、導出という有限の列についての定理（メタ定理）であり、証明は導出の長さに関する帰納法である。一方、真理値や構造による論理的帰結 $\models$ についての同じ形の主張は 意味論的な演繹定理 とよばれ、含意の記事で真理値表から証明されている。

結果	内容	仮定
thm-deduction-main	$\Gamma\cup\{\alpha\}\vdash\beta\iff\Gamma\vdash\alpha\to\beta$	規則は前件肯定だけ、公理に (A1)・(A2)
cor-deduction-finite	有限個の仮定をまとめて外す	同上
thm-deduction-gen	一般化規則がある体系での制限つきの形	一般化を $\alpha$ の自由変数に使わない

設定

証明体系と導出

証明体系は、論理式の集合 $\Lambda$（公理）と有限個の 推論規則 の組である。論理式の集合 $\Gamma$ からの導出とは、論理式の有限列 $\varphi_1,\dots,\varphi_n$ で、各 $\varphi_k$ が公理であるか、$\Gamma$ の元（前提）であるか、それ以前の行から推論規則で得られるものをいう。最後の行が $\varphi$ である $\Gamma$ からの導出があるとき $\Gamma\vdash\varphi$ と書き、$\emptyset\vdash\varphi$ を $\vdash\varphi$ と書く（一階論理の証明体系の記事の定義「証明体系・導出・証明可能性」）。$n$ を導出の長さ（行数）という。
導出が前の行だけを参照する有限列であることから、どの証明体系でも次が成り立つ（同記事の命題「導出可能性の基本性質」）。$\varphi\in\Gamma$ または $\varphi\in\Lambda$ なら $\Gamma\vdash\varphi$（反射性）。$\Gamma\subset\Delta$ かつ $\Gamma\vdash\varphi$ なら $\Delta\vdash\varphi$（単調性）。$\Gamma\vdash\varphi$ なら有限部分集合 $\Gamma_0\subset\Gamma$ で $\Gamma_0\vdash\varphi$（有限性）。$\Delta$ の各元が $\Gamma$ から導出でき $\Delta\vdash\psi$ なら $\Gamma\vdash\psi$（推移性）。以下、2 つの導出を並べてつなぐことを、推移性によって断らずに行う。

前件肯定と 2 つの公理図式

前件肯定（modus ponens、MP）は、$\psi$ と $\psi\to\chi$ から $\chi$ を導く推論規則である。$\alpha,\beta,\gamma$ を任意の論理式として、次の形の論理式を考える。

(A1) $\alpha\to(\beta\to\alpha)$
(A2) $(\alpha\to(\beta\to\gamma))\to((\alpha\to\beta)\to(\alpha\to\gamma))$
この記事では、次の条件を満たす証明体系を考える。

条件 (D)：推論規則は MP だけであり、公理の集合 $\Lambda$ は (A1)・(A2) の形の論理式をすべて含む。
次の体系はどれも条件 (D) を満たす。

一階述語論理の体系 $\mathbf H$（一階論理の証明体系の記事の定義「体系 H」）。公理は (A1)〜(A8) の実例の全称化の全体で、全称化しない実例そのものも含む。
命題論理の体系 $\mathbf H_0$ と $\mathbf H_0'$（Hilbert流の証明体系の記事の定義「体系 H₀ と H₀′」）。
直観主義命題論理の公理系（直観主義論理の記事の定義「直観主義命題論理の公理系」の公理 1・2 が (A1)・(A2) である）。
公理を追加しても条件 (D) は保たれるので、これらに公理を加えた体系も条件 (D) を満たす。

主張と証明

恒等式の導出

条件 (D) を満たす体系で、任意の論理式 $\alpha$ について $\vdash\alpha\to\alpha$ である。この導出は 5 行でとれる。

次の列が導出である。

$\alpha\to((\alpha\to\alpha)\to\alpha)$ ——(A1) で $\beta:=\alpha\to\alpha$
$(\alpha\to((\alpha\to\alpha)\to\alpha))\to((\alpha\to(\alpha\to\alpha))\to(\alpha\to\alpha))$ ——(A2) で $\beta:=\alpha\to\alpha$、$\gamma:=\alpha$
$(\alpha\to(\alpha\to\alpha))\to(\alpha\to\alpha)$ ——1、2 から MP
$\alpha\to(\alpha\to\alpha)$ ——(A1) で $\beta:=\alpha$
$\alpha\to\alpha$ ——4、3 から MP $\square$

演繹定理

条件 (D) を満たす証明体系で、論理式の集合 $\Gamma$ と論理式 $\alpha,\beta$ について
$$ \Gamma\cup\{\alpha\}\vdash\beta\quad\Longleftrightarrow\quad\Gamma\vdash\alpha\to\beta $$
が成り立つ。さらに、$\Gamma\cup\{\alpha\}$ からの $\beta$ の長さ $n$ の導出から、$\Gamma$ からの $\alpha\to\beta$ の長さ $5n$ 以下の導出が機械的に作れる。

導出の各行に「α→」を付ける

$\Leftarrow$：$\Gamma$ からの $\alpha\to\beta$ の導出の後ろに、前提 $\alpha$ と、MP で得た $\beta$ の 2 行を付け加えれば、$\Gamma\cup\{\alpha\}$ からの $\beta$ の導出になる。この向きは MP があれば成り立ち、公理は使わない。
$\Rightarrow$：$\Gamma\cup\{\alpha\}$ からの導出 $\beta_1,\dots,\beta_n=\beta$ をとる。$k=1,\dots,n$ の順に、$\Gamma$ からの導出 $D_k$ で、$D_{k-1}$ の後ろに高々 5 行を付け足したものであり、行 $\alpha\to\beta_1,\dots,\alpha\to\beta_k$ をすべて含むものを作る（$D_0$ は空の列とする）。$\beta_k$ の正当化に応じて場合を分ける。

$\beta_k$ が公理か $\Gamma$ の元の場合：$D_{k-1}$ の後ろに次の 3 行を付ける。$\beta_k$（公理または前提）、$\beta_k\to(\alpha\to\beta_k)$（(A1)）、$\alpha\to\beta_k$（MP）。
$\beta_k=\alpha$ の場合：$D_{k-1}$ の後ろに lem-deduction-identity の 5 行を付ける。最後の行は $\alpha\to\alpha=\alpha\to\beta_k$ である。
$\beta_k$ が $\beta_j$ と $\beta_l=(\beta_j\to\beta_k)$（$j,l< k$）から MP で得られた場合：$D_{k-1}$ はすでに行 $\alpha\to\beta_j$ と $\alpha\to(\beta_j\to\beta_k)$ を含む。その後ろに次の 3 行を付ける。
$$ (\alpha\to(\beta_j\to\beta_k))\to((\alpha\to\beta_j)\to(\alpha\to\beta_k))\ \text{（(A2)）},\quad(\alpha\to\beta_j)\to(\alpha\to\beta_k)\ \text{（MP）},\quad\alpha\to\beta_k\ \text{（MP）}. $$
推論規則は MP だけなので、場合はこれで尽きる。付け足した各行は公理、$\Gamma$ の元、またはそれ以前の行からの MP なので、$D_k$ は $\Gamma$ からの導出である。$D_n$ は $\alpha\to\beta_n=\alpha\to\beta$ を含み、その行で切れば $\Gamma$ からの $\alpha\to\beta$ の導出になる。各段で高々 5 行しか付け足さないので、長さは $5n$ 以下である。$\square$

証明が使ったのは、MP が唯一の規則であることと、(A1)・(A2) の実例と恒等式の導出だけである。(A1) は「すでに導出できるものは、どんな仮定のもとでも導出できる」を、(A2) は「仮定 $\alpha$ のもとでの MP」を、それぞれ体系の中に写したものである。(A1)・(A2) は、ちょうどこの証明が通るように選ばれている（OLT26 Chapter 22, Theorem 22.23 の証明の後の注意, p. 341）。命題論理の体系での主張は Bil03 Theorem 3.8（p. 13）、一階述語論理の体系 $\mathbf H$ での主張は同書 Theorem 7.10（p. 44）にあり、同書は証明を演習にしている。

有限個の仮定

条件 (D) を満たす体系で、論理式 $\alpha_1,\dots,\alpha_m,\beta$ について
$$ \Gamma\cup\{\alpha_1,\dots,\alpha_m\}\vdash\beta\iff\Gamma\vdash\alpha_1\to(\alpha_2\to(\cdots\to(\alpha_m\to\beta)\cdots)). $$
とくに $\Gamma\vdash\beta$ であることと、ある $\alpha_1,\dots,\alpha_m\in\Gamma$ で $\vdash\alpha_1\to(\cdots\to(\alpha_m\to\beta)\cdots)$ となることは同値である。

前半は、thm-deduction-main を $\Gamma\cup\{\alpha_1,\dots,\alpha_{m-1}\}$ と $\alpha_m$、次に $\Gamma\cup\{\alpha_1,\dots,\alpha_{m-2}\}$ と $\alpha_{m-1}$、… と $m$ 回使えばよい。後半：$\Gamma\vdash\beta$ なら、有限性により有限部分集合 $\{\alpha_1,\dots,\alpha_m\}\subset\Gamma$ から $\beta$ が導出でき、前半を $\Gamma:=\emptyset$ で使う。逆は、前半の右から左（$\Gamma:=\emptyset$）と単調性による。$\square$

この系により、前提つきの導出可能性 $\Gamma\vdash\beta$ は、前提なしの定理だけで言い表せる。

例：導出を書かずに導出の存在を示す

演繹定理を使うと、仮定を置いて MP を並べるだけで、含意の形の定理が導出できることを示せる。証明の後半で導出を書き換える手順をたどれば、実際の導出も得られる。

仮定の入れ替え

条件 (D) を満たす体系で $\vdash(\alpha\to(\beta\to\gamma))\to(\beta\to(\alpha\to\gamma))$ である。cor-deduction-finite により、$\{\alpha\to(\beta\to\gamma),\ \beta,\ \alpha\}\vdash\gamma$ を示せばよい。前提 $\alpha$ と $\alpha\to(\beta\to\gamma)$ から MP で $\beta\to\gamma$、それと前提 $\beta$ から MP で $\gamma$ を得る。この 5 行の導出に thm-deduction-main の書き換えを 3 回施すと、前提なしの導出になる。

矛盾からは何でも導出できる

体系 $\mathbf H_0$（公理図式 (A1)・(A2) と (A3) $(\lnot\beta\to\lnot\alpha)\to((\lnot\beta\to\alpha)\to\beta)$、規則 MP）で $\vdash\lnot\alpha\to(\alpha\to\beta)$ である。cor-deduction-finite により $\{\lnot\alpha,\alpha\}\vdash\beta$ を示せばよい。

$\lnot\alpha$ ——前提
$\lnot\alpha\to(\lnot\beta\to\lnot\alpha)$ ——(A1)
$\lnot\beta\to\lnot\alpha$ ——1、2 から MP
$\alpha$ ——前提
$\alpha\to(\lnot\beta\to\alpha)$ ——(A1)
$\lnot\beta\to\alpha$ ——4、5 から MP
$(\lnot\beta\to\lnot\alpha)\to((\lnot\beta\to\alpha)\to\beta)$ ——(A3)
$(\lnot\beta\to\alpha)\to\beta$ ——3、7 から MP
$\beta$ ——6、8 から MP
同じ議論で、$\Gamma\cup\{\lnot\beta\}$ から $\alpha$ と $\lnot\alpha$ の両方が導出できるなら $\Gamma\vdash\beta$ である（背理法の規則）。実際、演繹定理により $\Gamma\vdash\lnot\beta\to\alpha$ と $\Gamma\vdash\lnot\beta\to\lnot\alpha$ であり、(A3) と MP 2 回で $\beta$ を得る。

一般化規則がある体系

一階述語論理の体系 $\mathbf H$ は、「$x$ について一般化してよい」という推論を規則として置かず、公理を全称化で閉じている。これに対し、一般化規則「$\psi$ から $\forall x\,\psi$ を導く」（$x$ は任意の変数）を推論規則として加えた体系 $\mathbf H^+$ では、条件 (D) が成り立たず、演繹定理には制限が要る。

一般化規則があるときの演繹定理

体系 $\mathbf H^+$ で、$\Gamma\cup\{\alpha\}$ からの $\beta$ の導出であって、一般化規則を $\alpha$ に自由に現れる変数には適用していないものがあれば、$\Gamma\vdash_{\mathbf H^+}\alpha\to\beta$ である。逆向き $\Gamma\vdash_{\mathbf H^+}\alpha\to\beta\Rightarrow\Gamma\cup\{\alpha\}\vdash_{\mathbf H^+}\beta$ は制限なしに成り立つ。

一般化の段を (A5)・(A6) で処理する

逆向きは thm-deduction-main の証明の $\Leftarrow$ と同じである。
導出 $\beta_1,\dots,\beta_n=\beta$ の各 $k$ について $\Gamma\vdash_{\mathbf H^+}\alpha\to\beta_k$ を $k$ に関する帰納法で示す。まず、$\Gamma\vdash\varphi\to\psi$ と $\Gamma\vdash\psi\to\chi$ から $\Gamma\vdash\varphi\to\chi$ が従う。実際、(A1) の $(\psi\to\chi)\to(\varphi\to(\psi\to\chi))$ と MP で $\varphi\to(\psi\to\chi)$、(A2) の $(\varphi\to(\psi\to\chi))\to((\varphi\to\psi)\to(\varphi\to\chi))$ と MP 2 回で $\varphi\to\chi$ を得る。
$\beta_k$ が公理、$\Gamma$ の元、$\alpha$ 自身、または MP で得られた場合は、thm-deduction-main の証明と同じである（$\mathbf H^+$ も (A1)・(A2) の実例を公理にもつ）。残るのは、$\beta_k=\forall x\,\beta_j$（$j< k$）が一般化規則で得られた場合で、仮定から $x$ は $\alpha$ に自由に現れない。帰納法の仮定で $\Gamma\vdash\alpha\to\beta_j$ であり、一般化規則で $\Gamma\vdash\forall x\,(\alpha\to\beta_j)$ を得る。(A5) の実例 $\forall x\,(\alpha\to\beta_j)\to(\forall x\,\alpha\to\forall x\,\beta_j)$ と MP で $\Gamma\vdash\forall x\,\alpha\to\forall x\,\beta_j$ である。$x\notin\operatorname{FV}(\alpha)$ なので $\alpha\to\forall x\,\alpha$ は (A6) の実例である。この 2 つを最初に示したことでつなげば、$\Gamma\vdash\alpha\to\forall x\,\beta_j$、すなわち $\Gamma\vdash\alpha\to\beta_k$ である。$\square$

一般化の段で使った (A6) $\alpha\to\forall x\,\alpha$ は、$x$ が $\alpha$ に自由に現れないときにしか公理でない。条件を外すと結論が成り立たないことは、次の反例の 3 行目で確かめる。体系 $\mathbf H$ で演繹定理に制限が要らないのは、一般化を規則として置かず、前提に自由に現れない変数についての汎化定理（一階論理の証明体系の記事の定理「汎化定理」）として得ているからである。

反例：条件を外すと成り立たない

外す条件	反例	成り立たなくなること
公理に (A1) を含む	(A2)・(A3) と MP だけの体系	$\{p,q\}\vdash p$ だが $\vdash p\to(q\to p)$ でない
公理に (A2) を含む	(A1)・(A3) と MP だけの体系	$\{p\to(q\to r),\,p\to q,\,p\}\vdash r$ だが (A2) の実例が定理でない
推論規則は MP だけ	一般化規則を加えた $\mathbf H^+$	$\{P(x)\}\vdash\forall x\,P(x)$ だが $\vdash P(x)\to\forall x\,P(x)$ でない

反例の確認

$p,q,r$ は異なる命題変数、$P$ は 1 項関係記号とする。
1 行目：1 行の列 $p$ は $\{p,q\}$ からの導出である。この体系で演繹定理の形の同値が成り立つなら、それを 2 回使って $\{p\}\vdash q\to p$、$\vdash p\to(q\to p)$ となる。しかしこの式は (A2)・(A3) と MP から導出できない（Hilbert流の証明体系の記事の定理「H₀ の公理の独立性」の 1）。
2 行目：前提 $p$ と $p\to q$ から MP で $q$、前提 $p$ と $p\to(q\to r)$ から MP で $q\to r$、この 2 つから MP で $r$ を得る。この体系で演繹定理の形の同値が成り立つなら、それを 3 回使って $\vdash(p\to(q\to r))\to((p\to q)\to(p\to r))$ となるが、この式は (A1)・(A3) と MP から導出できない（同定理の 2）。
3 行目：2 行の列 $P(x),\ \forall x\,P(x)$ は $\mathbf H^+$ での $\{P(x)\}$ からの導出である。$\vdash_{\mathbf H^+}P(x)\to\forall x\,P(x)$ だとすると、$\mathbf H^+$ の定理はすべて妥当なので（健全性定理の記事の命題「一般化規則を加えた体系の健全性」の 1）、この式も妥当のはずである。ところが台集合 $\{0,1\}$、$P$ の解釈 $\{0\}$、$x$ への割り当て $0$ では、$P(x)$ が真で $\forall x\,P(x)$ が偽なので、この式は偽になる。よって制限のない演繹定理は $\mathbf H^+$ では成り立たない。この導出は一般化規則を $\alpha=P(x)$ に自由に現れる変数 $x$ に適用しており、thm-deduction-gen の制限に反している。

補足

意味論的な演繹定理との違い。 命題論理の論理的帰結 $\models$（付値による帰結）については、$\Sigma\cup\{\varphi\}\models\psi\iff\Sigma\models\varphi\to\psi$ が真理値表から直接示される（含意の記事の定理「意味論的な演繹定理」）。演繹定理は同じ形の主張を導出可能性 $\vdash$ について述べたもので、証明は導出の書き換えである。健全性定理と完全性定理によって $\vdash$ と $\models$ が一致する場面では、一方から他方が従う。しかし演繹定理は完全性定理を使わずに導出の操作だけで示せるので、完全性定理の証明（Gödelの完全性定理）の中で道具として使える。例えば OLT26 Proposition 22.27（p. 343）は、「$\Gamma\vdash\varphi$ であることと $\Gamma\cup\{\lnot\varphi\}$ が矛盾することは同値」を演繹定理から導き、完全性定理の証明に用いている。
自然演繹との関係。 自然演繹では、仮定 $\alpha$ から $\beta$ を導いたあと、仮定を外して $\alpha\to\beta$ を結論する規則（含意の導入規則）が最初から推論規則として置かれている。演繹定理は、Hilbert 流の体系でこの規則が許されること（許容規則であること）を示す定理だと言える。