演繹定理

定理5(演繹定理)

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

$${\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$$

で表す。さらにこのとき：

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

が成り立つ。 また，これを繰り返せば

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

$\Box$

演繹定理の証明

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

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

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

$${\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$$

は

$$\vdash_{H^1} \cal B$$

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

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

である。

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

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

(1).

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

(2).

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

(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}_1,{\cal A}_n \Rightarrow {\... ... \Rightarrow {\cal B}_{n-1},{\cal A}_n \Rightarrow {\cal B}_n$$

は$H^2$での ${\cal A}_n \Rightarrow {\cal B}$を含む「証明」になる。これは$k$についての帰納法による。

(1).

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

$$\frac{\cal A }{\cal B \Rightarrow A} \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$が得られる。$\Box$

演繹定理の２，３の応用

$${\cal \lnot A}\vdash_H F$$

のとき

$$\vdash_H \cal A$$

これは，まず

$${\cal \lnot A}\vdash_H F$$

から演繹定理により

$$\vdash_H {\cal \lnot A} \Rightarrow F$$

が得られ，これと公理$(14)$により

$$\vdash_H \cal \lnot A \Rightarrow A$$

となる。さらに公理$(1)$により，

$$\cal A \Rightarrow A$$

と公理$(5)$から

$$\cal (\lnot A \Rightarrow A) \Rightarrow [(A \Rightarrow A) \Rightarrow \{(A \lor \lnot A ) \Rightarrow A\} ]$$

が得られる。また，公理$(15)$により

$$\cal A \lor \lnot A$$

が成り立っている。これらより結局

$$\vdash_H \cal A$$

$\Box$

上の結果を推論規則の形で表現すれば

$$\frac{{\cal \lnot A} \Rightarrow F }{\cal A}$$

また論理式の形で表せば

$$({\cal \lnot A} \Rightarrow F) \Rightarrow {\cal A}$$

である。（いずれも$\vdash_H$が省略されていることに注意）

$$\frac{\cal A \Rightarrow B}{\cal \lnot B \Rightarrow \lnot A} (「対偶」)$$

まず， $\vdash_H {\cal A \Rightarrow B}$ を仮定する。系$H$に ${\cal \lnot B}$を追加して得られる系を$H^1$とする。 さらにこれに$\lnot A$の否定$\lnot \lnot A$を追加した系を$H^2$と すると，２重否定により， $\vdash_{H^ 2} \cal A$が，従って $\vdash_{H^2} \cal B$が得られる。このことから $\vdash_{H^2} F$となり，結局 $\vdash_{H^1} {\cal \lnot B \Rightarrow \lnot A}$が得られる。$\Box$