演繹定理

定理10(演繹定理1)

既述の体系$H$についてその公理系${\bf\beta}$に論理式

$${\cal A}_1,{\cal A}_2, \cdots,{\cal A}_n$$

を追加してできる新たな系で 論理式$\cal B$が証明可能であるとき，このことを

$${\cal A}_1,{\cal A}_2,\cdots,{\cal A}_n \vdash_H \cal B$$ (4.5)

で表す。このとき：

$${\cal A}_1,{\cal A}_2,\cdots,{\cal A} _{n-1} \vdash_H (\for... ...rall a_2) \cdots (\forall a_l){\cal A}_n \Rightarrow {\cal B}$$ (4.6)

が成り立つ。 $a_1,a_2 \cdots a_l$は${\cal A} _{n}$に現れる総ての自由変数記号 とする。 $\Box$

演繹定理の証明

体系$H$についてその公理系に論理式

$${\cal A}_1,{\cal A}_2, \cdots,{\cal A}_n$$

を追加してできる新たな系を$H^1$で表し， 体系$H$についてその公理系に論理式

$${\cal A}_1,{\cal A}_2,\cdots,{\cal A}_{n-1}$$

を追加してできる系を$H^2$で表す。

$${\cal A}_1,{\cal A}_2,\cdots,{\cal A}_n \vdash_H \cal B$$ (4.7)

は

$$\vdash_{H^1} \cal B$$ (4.8)

であることを表している。示すべきことは

$$\vdash_{H^2} (\forall a_1)(\forall a_2) \cdots (\forall a_l) {\cal A}_n \Rightarrow \cal B$$ (4.9)

である。 $a_1,a_2 \cdots a_l$は${\cal A} _{n}$に現れる総ての自由変数 である。

$${\cal B}_1,{\cal B}_2, \cdots,{\cal B}_{n-1},{\cal B}_n(={\cal B})$$ (4.10)

が$H^1$での「証明」とするとき，定義より 各${\cal B}_k$は次のいずれかである。

(1).

${\cal B}_k$は ${\cal A}_1,{\cal A}_2,\cdots,{\cal A}_n$のうち１つで ある。

(2).

${\cal B}_k$は$H$の各公理の形の論理式である。

(3).

論理式 ${\cal B}_k$ の前に論理式 ${\cal B}_i$と${\cal B}_j$ $(i,j<k)$があり，${\cal B}_j$は ${\cal B}_i \Rightarrow {\cal B}_k$ の 形をしている。

(4).

論理式 ${\cal B}_k$ の前に論理式 ${\cal B}_j$ $(j<k)$があり，${\cal B}_j$は

$${\cal C} \Rightarrow {\cal D}(b)$$ (4.11)

であり，${\cal B}_k$は

$${\cal C} \Rightarrow (\forall b)({\cal D}(b))$$ (4.12)

の形をしている。 ただし$b$は自由変数記号で$\cal C$には現れないものとする。

(5).

論理式 ${\cal B}_k$ の前に論理式 ${\cal B}_j$ $(j<k)$があり，${\cal B}_j$は

$${\cal C}(b) \Rightarrow {\cal D}$$ (4.13)

であり，${\cal B}_k$は

$$(\exists b)({\cal C}(b)) \Rightarrow {\cal D}$$ (4.14)

の形をしている。 ただし$b$は自由変数記号で$\cal D$には現れないものとする。

ここで，

$$(\forall a_1)(\forall a_2) \cdots (\forall a_l){\cal A}_n$$ (4.15)

を簡単に

$$\bar{{\cal A}}_n$$ (4.16)

で表す。 このとき，

$$\bar{{\cal A}}_n \Rightarrow {\cal B}_1,\bar{{\cal A}}_n \R... ...tarrow {\cal B}_{n-1},\bar{{\cal A}}_n \Rightarrow {\cal B}_n$$ (4.17)

は$H^2$での $\bar{{\cal A}}_n \Rightarrow {\cal B}$を含む「証明」になる。
実際，

(1).

${\cal B}_k$が ${\cal A}_1,{\cal A}_2,\cdots,{\cal A}_{n-1}$のうち１つであれば， ${\cal A}_1,{\cal A}_2,\cdots,{\cal A}_{n-1}$は$H^2$では公理であるから 証明可能な論理式ゆえ推論規則「添加」

$$\frac{\cal C }{\cal D \Rightarrow C} \qquad (添加)$$

により， $\bar{{\cal A}}_n \Rightarrow {\cal B}_k$は$H^2$で証明可能な論理式になる。 ${\cal B}_k$が${\cal A}_n$自身ならば，公理$(16)$を$l$回適用して

$$\begin{eqnarray*} &&(\forall a_1)(\forall a_2) \cdots (\forall a_l){\cal A}_n \... ...l a_3) \cdots (\forall a_l){\cal A}_n (a_1,a_2,a_3,\cdots,a_l) \end{eqnarray*}$$

$$(\forall a_3) \cdots (\forall a_l){\cal A}_n \Rightarrow (\forall a_4) \cdots (\forall a_l){\cal A}_n (a_1,a_2,a_3,a_4,\cdots,a_l)$$

$$\cdots$$

$$(\forall a_l){\cal A}_n \Rightarrow {\cal A}_n (a_1,a_2,\cdots,a_l)$$

により，

$$\bar{{\cal A}}_n \Rightarrow {\cal A}_n$$ (4.18)

は$H^2$で証明可能な論理式である。

(2).

${\cal B}_k$が$H$の各公理の形の論理式であるとき， 同様に「添加」により， $\bar{{\cal A}}_n \Rightarrow {\cal B}_k$は$H^2$で証明可能な論理式である。

(3).

論理式 ${\cal B}_k$ の前に論理式 ${\cal B}_i$と${\cal B}_j$ $(i,j<k)$があり，${\cal B}_j$は ${\cal B}_i \Rightarrow {\cal B}_k$ の 形をしているときは， $\bar{{\cal A}}_n \Rightarrow {\cal B}_k$の前に， $\bar{{\cal A}}_n \Rightarrow {\cal B}_i$と $\bar{{\cal A}}_n \Rightarrow ({\cal B}_i \Rightarrow {\cal B}_k)$とがあることになる。 これに「複推移」

$$\frac{ \cal A \Rightarrow (B \Rightarrow C) ,A \Rightarrow B } {\cal A \Rightarrow C}　(複推移)$$

を適用すると $\bar{{\cal A}}_n \Rightarrow {\cal B}_k$が証明可能であることが 示される。

(4).

論理式 ${\cal B}_k$ の前に論理式 ${\cal B}_j$ $(j<k)$があり，${\cal B}_j$は]

$${\cal C} \Rightarrow {\cal D}(b)$$ (4.19)

であり，${\cal B}_k$は

$${\cal C} \Rightarrow (\forall b)({\cal D}(b))$$ (4.20)

の形をしている場合。 ただし$b$は自由変数記号で$\cal C$には現れないものとする。 この場合， $\bar{{\cal A}}_n \Rightarrow {\cal B}_k$の前に， $\bar{{\cal A}}_n \Rightarrow ({\cal C} \Rightarrow {\cal D}(b))$ があり， $\bar{{\cal A}}_n \Rightarrow {\cal B}_k$は

$$\bar{{\cal A}}_n \Rightarrow {\cal C} \Rightarrow (\forall b)({\cal D}(b))$$ (4.21)

の形をしている。 ここで $\bar{{\cal A}}_n \Rightarrow ({\cal C} \Rightarrow {\cal D}(b))$ に全称化の推論規則

$$\frac{{\cal E} \Rightarrow {\cal F}(c)} {{\cal E} \Rightarrow (\forall c)({\cal F}(c))}$$

を適用して

$$\bar{{\cal A}}_n \Rightarrow (\forall b)({\cal C} \Rightarrow {\cal D}(b))$$ (4.22)

が証明可能である。また公理$(16)$から

$$(\forall b)({\cal C} \Rightarrow {\cal D}(b))　 \Rightarrow ({\cal C} \Rightarrow {\cal D}(b))$$ (4.23)

が証明可能である。　全称化の推論規則によれば

$$({\cal C} \Rightarrow {\cal D}(b)) \Rightarrow ({\cal C} \Rightarrow (\forall b)({\cal D}(b)))$$ (4.24)

が証明可能である。以上を連鎖させれば，

$$\bar{{\cal A}}_n \Rightarrow {\cal B}_k$$ (4.25)

が証明可能であることが わかる。
最後に，

(5).

論理式 ${\cal B}_k$ の前に論理式 ${\cal B}_j$ $(j<k)$があり，${\cal B}_j$は

$${\cal C}(b) \Rightarrow {\cal D}$$ (4.26)

であり，${\cal B}_k$は

$$(\exists b)({\cal C}(b)) \Rightarrow {\cal D}$$ (4.27)

の形をしている場合を考えよう。 ただし$b$は自由変数記号で$\cal D$には現れないものとする。

この場合， $\bar{{\cal A}}_n \Rightarrow {\cal B}_k$の前に， $\bar{{\cal A}}_n \Rightarrow ({\cal C}(b) \Rightarrow {\cal D})$ があり， $\bar{{\cal A}}_n \Rightarrow {\cal B}_k$は

$$\bar{{\cal A}}_n \Rightarrow ((\exists b)({\cal C}(b)) \Rightarrow {\cal D})$$ (4.28)

の形である。

先ず，公理$(17)$ によれば

$$({\cal C}(b) \Rightarrow {\cal D}) \Rightarrow ((\exists b)({\cal C}(b)) \Rightarrow {\cal D})$$ (4.29)

が証明可能である。これと既に証明可能なことが分かっている $\bar{{\cal A}}_n \Rightarrow ({\cal C}(b) \Rightarrow {\cal D})$ を連鎖させれば，

$$\bar{{\cal A}}_n \Rightarrow ((\exists b)({\cal C}(b)) \Rightarrow {\cal D})$$ (4.30)

が証明可能なことが分かる。 $\Box$

定理10の系(演繹定理2)

$a_1,a_2 \cdots a_l$は${\cal A} _{n}$に現れる総ての自由変数記号 とする。

特に $a_1,a_2 \cdots a_l$についての全称化を行わずに

$${\cal A}_1,{\cal A}_2,\cdots,{\cal A}_n \vdash_H \cal B$$ (4.31)

ならば：

$${\cal A}_1,{\cal A}_2,\cdots,{\cal A} _{n-1} \vdash_H {\cal A}_n \Rightarrow {\cal B}$$ (4.32)

が成り立つ。 $\Box$

系の証明

定理$(10)$と同様に 体系$H$についてその公理系に論理式

$${\cal A}_1,{\cal A}_2, \cdots,{\cal A}_n$$

を追加してできる新たな系を$H^1$で表し， 体系$H$についてその公理系に論理式

$${\cal A}_1,{\cal A}_2,\cdots,{\cal A}_{n-1}$$

を追加してできる系を$H^2$で表す。

$${\cal A}_1,{\cal A}_2,\cdots,{\cal A}_n \vdash_H \cal B$$ (4.33)

は

$$\vdash_{H^1} \cal B$$ (4.34)

であることを表している。示すべきことは

$$\vdash_{H^2} {\cal A}_n \Rightarrow \cal B$$ (4.35)

である。

$${\cal B}_1,{\cal B}_2, \cdots,{\cal B}_{n-1},{\cal B}_n(={\cal B})$$

が$H^1$での「証明」とするとき，定義と $a_1,a_2 \cdots a_l$についての制限から 各${\cal B}_k$は次のいずれかである。

(1).

${\cal B}_k$は ${\cal A}_1,{\cal A}_2,\cdots,{\cal A}_n$のうち１つで ある。

(2).

${\cal B}_k$は$H$の各公理の形の論理式である。

(3).

論理式 ${\cal B}_k$ の前に論理式 ${\cal B}_i$と${\cal B}_j$ $(i,j<k)$があり，${\cal B}_j$は ${\cal B}_i \Rightarrow {\cal B}_k$ の 形をしている。

(4).

論理式 ${\cal B}_k$ の前に論理式 ${\cal B}_j$ $(j<k)$があり，${\cal B}_j$は

$${\cal C}(b) \Rightarrow {\cal D}$$ (4.36)

であり，${\cal B}_k$は

$$(\exists b)({\cal C}(b)) \Rightarrow {\cal D}$$ (4.37)

の形をしている。 ただし$b$は自由変数記号で$\cal D$には現れないものとする。

このとき，

$${\cal A}_n \Rightarrow {\cal B}_1,{\cal A}_2 \Rightarrow {\... ... \Rightarrow {\cal B}_{n-1},{\cal A}_n \Rightarrow {\cal B}_n$$ (4.38)

は$H^2$での ${\cal A}_n \Rightarrow {\cal B}$を含む「証明」になる。
実際，

(1).

${\cal B}_k$が ${\cal A}_1,{\cal A}_2,\cdots,{\cal A}_{n-1}$のうち１つであれば，

${\cal A}_1,{\cal A}_2,\cdots,{\cal A}_{n-1}$は$H^2$では公理であるから 証明可能な論理式ゆえ推論規則「添加」

$$\frac{\cal C }{\cal D \Rightarrow C} \qquad (添加)$$

により， ${\cal A}_n \Rightarrow {\cal B}_k$は$H^2$で証明可能な論理式になる。 ${\cal B}_k$が${\cal A}_n$自身ならば，公理$(1)$ により，

$${\cal A}_n \Rightarrow {\cal A}_n$$

は$H^2$で証明可能な論理式である。

(2).

${\cal B}_k$が$H$の各公理の形の論理式であるとき， 同様に「添加」により， ${\cal A}_n \Rightarrow {\cal B}_k$は$H^2$で証明可能な論理式である。

(3).

論理式 ${\cal B}_k$ の前に論理式 ${\cal B}_i$と${\cal B}_j$ $(i,j<k)$があり，${\cal B}_j$は ${\cal B}_i \Rightarrow {\cal B}_k$ の 形をしているときは， ${\cal A}_n \Rightarrow {\cal B}_k$の前に， ${\cal A}_n \Rightarrow {\cal B}_i$と ${\cal A}_n \Rightarrow ({\cal B}_i \Rightarrow {\cal B}_k)$とがあることになる。 これに「複推移」

$$\frac{ \cal A \Rightarrow (B \Rightarrow C) ,A \Rightarrow B } {\cal A \Rightarrow C}　(複推移)$$

を適用すると ${\cal A}_n \Rightarrow {\cal B}_k$が証明可能であることが 示される。

最後に，

(4).

論理式 ${\cal B}_k$ の前に論理式 ${\cal B}_j$ $(j<k)$があり，${\cal B}_j$は

$${\cal C}(b) \Rightarrow {\cal D}$$ (4.39)

であり，${\cal B}_k$は

$$(\exists b)({\cal C}(b)) \Rightarrow {\cal D}$$ (4.40)

の形をしている場合を考えよう。 ただし$b$は自由変数記号で$\cal D$には現れないものとする。

この場合， ${\cal A}_n \Rightarrow {\cal B}_k$の前に， ${\cal A}_n \Rightarrow ({\cal C}(b) \Rightarrow {\cal D})$ があり， ${\cal A}_n \Rightarrow {\cal B}_k$は

$${\cal A}_n \Rightarrow ((\exists b)({\cal C}(b)) \Rightarrow {\cal D})$$ (4.41)

の形である。

先ず，公理$(17)$ によれば

$$({\cal C}(b) \Rightarrow {\cal D}) \Rightarrow ((\exists b)({\cal C}(b)) \Rightarrow {\cal D})$$ (4.42)

が証明可能である。これと既に証明可能なことが分かっている ${\cal A}_n \Rightarrow ({\cal C}(b) \Rightarrow {\cal D})$ を連鎖させれば，

$${\cal A}_n \Rightarrow ((\exists b)({\cal C}(b)) \Rightarrow {\cal D})$$ (4.43)

が証明可能なことが分かる。 $\Box$