導出原理

この章では個体閉論理式

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

から 論理式$\cal B$を導出原理を用いて証明する方法を説明する。

体系$H$の公理系に論理式

$${\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$$ (5.1)

で表した。このとき演繹定理によれば，

$${\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}$$ (5.2)

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

特に

$${\cal A}_1,{\cal A}_2, \cdots,{\cal A}_n$$ (5.3)

が自由変数を持たない個体閉論理式の集合であれば，全称記号$\forall$の作用は 無効になるから

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

であり，これと公理$(6),(7)$

$$\cal (A \land B) \Rightarrow A$$ (5.5)

$$\cal (A \land B) \Rightarrow B$$ (5.6)

を繰り返し用いて，

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

上の議論の逆を辿れば，結局，

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

が成立つのは

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

が成立つとき，かつそのときに限る。
完全性定理によれば，後者は，

$${\cal A}_1 \land {\cal A}_2 \land \cdots \land{\cal A} _{n-1} \land {\cal A}_n \Rightarrow {\cal B}$$ (5.10)

が恒真論理式であることに等しい。
これはこの論理式の否定

$${\cal A}_1 \land {\cal A}_2 \land \cdots \land{\cal A} _{n-1} \land {\cal A}_n \land \lnot {\cal B}$$ (5.11)

が恒偽論理式であること，すなわち充足不能であることと同じである。