推論規則と証明

前節の公理から何らかの記号的な操作によって証明可能な論理式が得られるの であるがその操作の規則を推論規則とよぶ。 命題論理での推論規則は，次の三段論法(modus ponens)のみである。 横線の上の論 理式から下の論理式が導かれることを表す。

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

証明可能性を定義する。すなわち，${\bf L_g}$ の要素である論理式のうち， 証明可能な論理式(provable formula)を次のように定める:

(1).

公理系の各公理の形の論理式は証明可能である。

(2).

論理式 $\cal A$ と論理式 $\cal A \Rightarrow B$ が証明可能なら ば，(推論規則によって，)論理式 $\cal B$ は証明可能である。

証明可能な論理式の列を「証明」という。「証明可能性」の定義に従えば

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

が「証明」のとき，各${\cal A}_k$は

(1).

公理系の各公理の形の論理式である。

(2).

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

例えば，

$$\cal B \land \cal A \Rightarrow A , \quad (\cal B \land \c... ...cal A)), \quad \cal A \Rightarrow (\cal B \Rightarrow \cal A)$$

もっと具体的には

$$\begin{eqnarray*} &&1=2 \land 2> 6 \Rightarrow 2>6 \\ &&( 1=2 \land 2>6 \Righ... ...\Rightarrow 2>6)) \\ &&2>6 \Rightarrow ( 1=2 \Rightarrow 2>6) \end{eqnarray*}$$

は証明である。（証明可能な論理式を「定理」とか「命題」と呼ぶこともある。）

「証明」の中で推論規則と公理を何回か適用する共通した手順を「推論法則」 と呼ぶ。（これ自身は公理系を定義するのに必須ではないが，それを操作する 上で便利な手続きをまとめたもの。） 以下に推論法則の例を述べる。

［例］

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

$\cal A$が証明可能な論理式ならば $\cal B \Rightarrow A$も 証明可能な論理式であることを表す。
実際，上の「証明」の例の最後に注目すれば

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

は証明可能であり，$\cal A$が証明可能なら推論規則（三段論法） により， $\cal B \Rightarrow A$も証明可能なことがわかる。$\Box$

$$\frac{\cal A,B }{\cal A \land B} \qquad ({\bf 推論法則：論理積})$$

任意の論理式$\cal C$を用いて「添加」により

$$\cal (C \lor \lnot C ) \Rightarrow A,(C \lor \lnot C ) \Rightarrow B$$

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

$$\cal \{ (C \lor \lnot C) \Rightarrow A \} \Rightarrow [ ... ...ightarrow \{ (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 ({\bf 推論法則：交換})$$

が得られる。 同様に

$$\frac{\cal A \lor B }{\cal B \lor A} \qquad ({\bf 推論法則：交換})$$

も得られる。さらに

$$\cal A \Rightarrow \lnot \lnot A,\lnot \lnot A \Rightarrow A {\bf 推論法則：２重否定}$$

も得られる。

$$\frac{ \cal A \Rightarrow B ,B \Rightarrow C } {\cal A \Rightarrow C}({\bf 推論法則：推移})$$

これは公理$(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}　({\bf 推論法則：復推移})$$

が証明可能である。これはまず，公理$(8)$から

$$\cal (A \Rightarrow B) \Rightarrow [ \{ A \Rightarrow (B \R... ...} \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\alpha} + 「推論規則」$）

${\bf L_g}$の論理式 $\cal A$ が証明可能であるとは， $H$ において，公理系 ${\bf\alpha}$ から $\cal A$ が推論規 則によって導けることであるから，これを

$$\vdash_H \cal A$$

と書く。推論規則

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

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

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

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