• • [例]

$\frac{\cal A }{\cal B \Rightarrow A} \qquad (推論法則：添加)$

$\cal A$が証明可能な論理式ならば$\cal B \Rightarrow A$も

証明可能な論理式であることを表す。 (上の「証明」の例に現れている。) $\frac{\cal A,B }{\cal A \land B} \qquad (推論法則：論理積)$ 任意の論理式$\cal C$を用いて「添加」により $\cal (C \lor \lnot C ) \Rightarrow A,(C \lor \lnot C ) \Rightarrow B$ が得られる。また$(8)$であるから $\cal \{ (C \lor \lnot C) \Rightarrow A \} \Rightarrow [ \{ (C \lor \lnot C) \Rightarrow B \} \Rightarrow \{ (C \lor \lnot C) \Rightarrow (A \land B ) \} ]$ 推論規則により、 $\cal (C \lor \lnot C) \Rightarrow (A \land B )$ が得られる。ところで$(15)$により $\cal C \lor \lnot C$ は公理（当然証明可能な論理式であるから） 結局 $\cal A \land B$ は証明可能な論理式である。$\Box$ またこれから直ちに $\frac{\cal A \land B }{\cal B \land A} \qquad (推論法則：交換)$ が得られる。 同様に $\frac{\cal A \lor B }{\cal B \lor A} \qquad (推論法則：交換)$ も得られる。さらに $\cal A \Rightarrow \lnot \lnot A,\lnot \lnot A \Rightarrow A 「２重否定」$ も得られる。 $\frac{ \cal A \Rightarrow B ,B \Rightarrow C } {\cal A \Rightarrow C}(推論法則：推移)$ これは$(2)$より $\cal (A \Rightarrow B) \Rightarrow [(B \Rightarrow C ) \Rightarrow (A \Rightarrow C) ]$ が得られ、これと $\cal A \Rightarrow B$ から推論規則により、 $\cal (B \Rightarrow C ) \Rightarrow (A \Rightarrow C)$ を得る。さらにこれと $\cal B \Rightarrow C$ とから $\cal A \Rightarrow C$ が得られることで示される。$\Box$ %% %% 同様に $\frac{ \cal A \Rightarrow (B \Rightarrow C) ,A \Rightarrow B } {\cal A \Rightarrow C}　(推論法則：復推移)$ が得られる。これはまず、$(8)$から $\cal (A \Rightarrow B) \Rightarrow [ \{ A \Rightarrow (B \Rightarrow C) \} \Rightarrow \{A \Rightarrow B \land (B \Rightarrow C) \} ]$ これと ${\cal A \Rightarrow (B \Rightarrow C) , A \Rightarrow B}$ から ${\cal A \Rightarrow \{ B \land (B \Rightarrow C) \} }$ が得られ さらに$(9)$の ${\cal \{B \land (B \Rightarrow C)\} \Rightarrow C }$ と前述の「推移」により $\cal A \Rightarrow C$ が得られることで示される。$\Box$

 上述の体系を $H$ と呼ぶことにしよう。（$H = 公理系${\bf A}$+ 「推論規則」$）

$\bf L$の論理式 $\cal A$ が証明

 可能であるとは、$H$ において、公理系 $\bf A$ から $\cal A$ が推論規
 則によって導けることであるから、これを
 $\vdash_H \cal A$
 と書く。推論規則
 $\frac{\cal A \quad  A \Rightarrow B}{\cal B}$

はこの表記法を用いると、

 $\frac{\vdash_H \cal A \quad  \vdash_H A \Rightarrow B}{\vdash_H \cal B}$

と書くべきである。しかし、どの系で証明可能なのか明らかな場合は $\vdash_H$は省略することにする。

演繹定理

上の体系$H$についてその公理系${\bf A}$に論理式 ${\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 A}$に論理式 ${\cal A}_1,{\cal A}_2,\cdots,{\cal A}_n$ を追加してできる新たな系を$H^1$で表し、 体系$H$についてその公理系${\bf A}$に論理式 ${\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}_i$は次のいずれかである。

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

ある。

 * ${\cal B}_i$は公理系$H$の各公理の形の論理式である。
 * 論理式 ${\cal B}_i$ の前に論理式 ${\cal B}_j$と${\cal B}_k$

$(j,k<i)$があり、${\cal B}_k$は${\cal B}_j \Rightarrow {\cal B}_i$ の 形をしている。

そして、 ${\cal A}_n \Rightarrow {\cal B}_1,{\cal A}_n \Rightarrow {\cal B}_2, \cdots,{\cal A}_n \Rightarrow {\cal B}_{n-1},{\cal A}_n \Rightarrow {\cal B}_n$ は$H^2$での${\cal A}_n \Rightarrow {\cal B}$を含む「証明」になる。

 * ${\cal B}_i$が${\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}_i$は$H^2$で証明可能な論理式になる。 ${\cal B}_i$が${\cal A}_n$自身ならば、公理$(1)$ により、 ${\cal A}_n \Rightarrow {\cal A}_n$ は$H^2$で証明可能な論理式である。

 * ${\cal B}_i$が公理系$H$の各公理の形の論理式であるとき、

同様に「添加」により、 ${\cal A}_n \Rightarrow {\cal B}_i$は$H^2$で証明可能な論理式である。

 * 論理式 ${\cal B}_i$ の前に論理式 ${\cal B}_j$と${\cal B}_k$

$(j,k<i)$があり、${\cal B}_k$は${\cal B}_j \Rightarrow {\cal B}_i$ の 形をしているときは、 ${\cal A}_n \Rightarrow {\cal B}_i$の前に、 ${\cal A}_n \Rightarrow {\cal B}_j$と${\cal A}_n \Rightarrow ({\cal B}_j \Rightarrow {\cal B}_i)$とがあることになる。 これに「複推移」 $\frac{ \cal A \Rightarrow (B \Rightarrow C) ,A \Rightarrow B } {\cal A \Rightarrow C}　(復推移)$ を適用すると ${\cal A}_n \Rightarrow {\cal B}_i$が得られる。$\Box$

• 「演繹定理」の２、３の応用

${\cal \lnot A}\vdash_H \bot$ のとき $\vdash_H \cal A$ これは、まず ${\cal \lnot A}\vdash_H \bot$ から $\vdash_H \cal \lnot A \Rightarrow A$ となる。さらに$(1)$により、 $\cal A \Rightarrow A$ と$(8)$から $\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 \bot }{\cal A}$ また論理式の形で表せば $\cal (\lnot A \Rightarrow \bot) \Rightarrow A$ である。（いずれも$\vdash_H$が省略されていることに注意）

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

 体系 $H$ については、次の事実が知られている:

%% %%

• [定理8]\mbox{}

 $\cal A$ が恒真論理式であることの必要十分条件は、$\vdash_H \cal A$ 
 が成立することである。$\Box$

 この定理は、命題計算の体系についての{\gt 完全性定理}(completeness 
 theorem)と呼ばれるものである。

• [定理８の証明]\mbox{}

まず、$\vdash_H \cal A$が成立すれば$\cal A$が恒真論理式であることを示そう。

$\vdash_H \cal A$が成り立つとすると； 系$H$の「証明」である論理式の列 ${\cal A}_1,{\cal A}_2, \cdots,{\cal A}_n$ があって、$\cal A$は最後の${\cal A}_n$と一致しているものとしてよい。 各${\cal A}_i$は

 * 公理系の各公理の形の論理式である。この場合、各公理は恒真論理式

であるから${\cal A}_i$は恒真論理式である。

 * 論理式 ${\cal A}_i$ の前に論理式 ${\cal A}_j$と${\cal A}_k$

$(j,k<i)$があり、${\cal A}_k$は${\cal A}_j \Rightarrow {\cal A}_i$ の 形をしている。 $i$より前の論理式は恒真論理式であると仮定すると、 ${\cal A}_j$と${\cal A}_k$は${\cal A}_j \Rightarrow {\cal A}_i$は真理値$\top$しかとらないから真理値表

 $$\begin{tabular}{|c c||c|}
 \hline
 UNIQ4dc8667975f7180c-MathJax-206-QINU & UNIQ4dc8667975f7180c-MathJax-207-QINU & UNIQ4dc8667975f7180c-MathJax-208-QINU \\
 \hline 
 UNIQ4dc8667975f7180c-MathJax-209-QINU & UNIQ4dc8667975f7180c-MathJax-210-QINU & UNIQ4dc8667975f7180c-MathJax-211-QINU \\
 \hline
 UNIQ4dc8667975f7180c-MathJax-212-QINU & UNIQ4dc8667975f7180c-MathJax-213-QINU & UNIQ4dc8667975f7180c-MathJax-214-QINU \\
 \hline
 UNIQ4dc8667975f7180c-MathJax-215-QINU & UNIQ4dc8667975f7180c-MathJax-216-QINU & UNIQ4dc8667975f7180c-MathJax-217-QINU \\
 \hline
 UNIQ4dc8667975f7180c-MathJax-218-QINU & UNIQ4dc8667975f7180c-MathJax-219-QINU & UNIQ4dc8667975f7180c-MathJax-220-QINU \\
 \hline
 \end{tabular}$$ 

から明らかなように${\cal A}_i$の真理値は$\top$しか取り得ない。 すなわち${\cal A}_i$は恒真論理式である。

逆に$\cal A$が恒真論理式であるときに、 $\vdash_H \cal A$が成立することをいうには次の補題１が必要になる。

• [補題１]\mbox{}

$\cal A$が命題変数$X_1,X_2,\cdots,X_n$から構成される論理式とする。 命題変数$X_1,X_2,\cdots,X_n$に真理値$\top,\bot$をふり当て、そのふり当てに対し$\cal A$の真理値が$\top$である場合 $\delta X_1,\delta X_2,\cdots \delta X_n \vdash_H \cal A$ $\cal A$の真理値が$\bot$である場合 $\delta X_1,\delta X_2,\cdots \delta X_n \vdash_H \cal \lnot A$

である。ただし、$\delta X_i$は$X_i$に対する真理値のふり当てが$\top$の場合$X_i$、$\bot$の場合は$\lnot X_i$とする。$\Box$

• [定理８の証明の続き]\mbox{}

恒真論理式$\cal A$が命題変数$X_1,X_2,\cdots,X_n$から構成されるものとする。 する。 命題変数$X_1,X_2,\cdots,X_n$に真理値$\top,\bot$どのようにふり当ても、 $\cal A$の真理値は常に$\top$である。

命題変数$X_1,X_2,\cdots,X_n$に真理値$\top,\bot$どのようにふり当てるしかたは $2^n$通りある。これを辞書式順序で全て列挙し[補題１]を適用すると $X_1,X_2,\cdots , X_n \vdash_H \cal A \\ X_1,X_2,\cdots , \lnot X_n \vdash_H \cal A \\ X_1,X_2,\cdots , \lnot X_{n-1},X_n \vdash_H \cal A \\ X_1,X_2,\cdots , \lnot X_{n-1},\lnot X_n \vdash_H \cal A \\ \cdots \\ \cdots \\ \lnot X_1,\lnot X_2,\cdots , \lnot X_n \vdash_H \cal A \\ $が得られる。最初の２式から演繹定理により $X_1,X_2,\cdots , X_{n-1} \vdash X_n \Rightarrow \cal A \\ X_1,X_2,\cdots , X_{n-1} \vdash \lnot X_n \Rightarrow \cal A \\ $これから $X_1,X_2,\cdots , X_{n-1} \vdash_H \cal A$ が得られる。すなわち$X_n$が消去された。同様にして順次に２式ずつ 同じ手順を繰り返せば、$X_n$が消去された$2^{n-1}$個の式を得る。この $2^{n-1}$個の式から$X_{n-1}$を２式ずつをとり同じ手順を繰り返すと$X_{n-1}$が 消去された$2^{n-2}$個の式を得る。 この手順を繰り返せば変数$X_1,X_2,\cdots,X_n$が全て消去され、結局 $\vdash_H \cal A$ を得る。$\Box$

• [補題１の証明]\mbox{}

 \begin{description}
 * 論理式$\cal A$がただ１つの命題変数$X$からなるとき

　　　　 　　　　$X$に対するふり当てが$\top$のとき

       $X \vdash_H X$

　　　　$\bot$のとき

       $\lnot X \vdash_H \lnot X$

これは公理の$(1)$から容易に示される。

 これ以外の場合は、$\cal A$は$\cal \lnot B,B \land C,B \lor C$の形をして

いる。この場合、部分式$\cal B,C$については この補題１が成り立つものとする。

* $\cal A$ が$\cal \lnot B$である場合 

  $\cal A$の値が$\top$のとき$\cal B$の値は$\bot$であるから
  $\delta X_1,\delta X_2,\cdots,\delta X_n \vdash_H \lnot \cal B$
  $\cal A$の値が$\bot$のとき$\cal B$の値は$\top$であるから
  $\delta X_1,\delta X_2,\cdots,\delta X_n \vdash_H  \cal B$

　$\cal B,\lnot B$はそれぞれ$\cal A$及び$\cal \lnot A$である。

* $\cal A$ が$\cal B \lor C$である場合 

  $\cal A$の値が$\top$のとき$\cal B,C$の少なくともどちらか一方の値は

$\top$であるから、$\cal B$の値が$\top$としても一般性を失わない。このとき

  $\delta X_1,\delta X_2,\cdots,\delta X_n \vdash_H  \cal B$

が成り立っている。これと公理の$(3)$ $\cal B \Rightarrow B \lor C$ により

  $\delta X_1,\delta X_2,\cdots,\delta X_n \vdash_H  \cal B \lor C$

$\cal B \lor C$は$\cal A$に他ならない。

  $\cal A$の値が$\bot$のとき$\cal B,C$の値はともに$\bot$でなければならない。

このとき

  $\delta X_1,\delta X_2,\cdots,\delta X_n \vdash_H  \cal \lnot B$
  $\delta X_1,\delta X_2,\cdots,\delta X_n \vdash_H  \cal \lnot C$

これに推論法則の「論理積」 $\frac{\cal P,Q}{\cal P \land Q}$ を用いて

  $\delta X_1,\delta X_2,\cdots,\delta X_n \vdash_H  
      \cal \lnot B　\land \lnot C$

を得る。 $\cal \lnot B \land \lnot C$は$\cal \lnot A(=\lnot (B \lor C))$に他ならない。

* $\cal A$ が$\cal B \land C$である場合 

  $\cal A$の値が$\top$のとき$\cal B,C$の値はともに$\top$でなければならない。

このとき

  $\delta X_1,\delta X_2,\cdots,\delta X_n \vdash_H  \cal  B$
  $\delta X_1,\delta X_2,\cdots,\delta X_n \vdash_H  \cal  C$

これに推論法則の「論理積」 $\frac{\cal P,Q}{\cal P \land Q}$ を用いて

  $\delta X_1,\delta X_2,\cdots,\delta X_n \vdash_H  
      \cal  B　\land  C$

を得る。 $\cal B \land C$は$\cal A$に他ならない。

  $\cal A$の値が$\bot$のとき$\cal B,C$の少なくともどちらか一方の値は

$\bot$であるから、$\cal B$の値が$\bot$としても一般性を失わない。このとき

  $\delta X_1,\delta X_2,\cdots,\delta X_n \vdash_H  \cal \lnot B$

が成り立っている。これと公理の$(3)$ $\cal P \Rightarrow P \lor Q$ により

  $\delta X_1,\delta X_2,\cdots,\delta X_n \vdash_H  \cal \lnot B \lor \lnot C$