演繹定理,全称化,特称化

前節のような公理と推論規則の対は公理系と呼ばれます。 前節の系を${\bf H}$ で表すことにします。

関係式 $\cal A$ が証明可能であるとは， ${\bf 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$は省略することにします。

1. 演繹定理は「推論規則」同様,有用な道具を提供します。
   

   演繹定理　
   公理系$H$の公理に関係式
   

   $${\cal A}$$
   
   
   を追加してできる新たな系で 関係式$\cal B$が証明可能であるとき，このことを
   
   $${\cal A} \vdash_H \cal B$$
   
   
   で表します。このとき：
   
   $$\vdash_H (\forall a_1)(\forall a_2) \cdots (\forall a_l){\cal A} \Rightarrow {\cal B}$$
   
   
   が成り立ちます。 $a_1,a_2 \cdots a_l$は${\cal A} _{n}$に現われる総ての自由変数記号 とします。
   特に,関係式${\cal B}$の中で, $a_1,a_2 \cdots a_l$が$\forall$で束縛されていない 自由変数[$(\forall a_i)$のような記号がないという意味です。] ならば
   
   $$\vdash_H {\cal A} \Rightarrow {\cal B}$$
   
   
   $\Box$
   これから，背理法として知らる有用な道具が得られます。
   背理法
   ある関係式${\cal B}$が存在して，
   
   $$\lnot {\cal A} \vdash_H {\cal B} \land \lnot {\cal B}$$
   
   
   ならば
   
   $$\vdash_H {\cal A}$$
   
   
   $\Box$
   特に限定記号のある関係式については
   
   $$(\exists x)(\lnot {\cal A}(x)) \vdash_H {\cal B} \land \lnot {\cal B}$$
   
   
   ならば
   
   $$\vdash_H (\forall x)({\cal A} (x))$$
   
   

   
   

   $$(\forall x)(\lnot {\cal A}(x)) \vdash_H {\cal B} \land \lnot {\cal B}$$
   
   
   ならば
   
   $$\vdash_H (\exists x)({\cal A} (x))$$
   
   

   また以下の推論規則も有用です。

2. 全称化　
   $x$が${\cal A }(x)$の自由変数であれば,
   
   $$\frac{{\cal A }(x) } {(\forall x){\cal A}(x)} \qquad （ {\bf 推論法則：全称化})$$
   
   

3. 特称化
   $c$が特定の対象を表す対象定数記号とするとき,
   
   $$\frac{{\cal A }(c) } {(\exists x){\cal A}(x)} \qquad （ {\bf 推論法則：特称化})$$
   
   

   定理　
   以上の，公理，推論法則を使えば次の諸定理を得ます。「定理」とは証明可能な 関係式のことです。

   ((a))

   関係式 ${\bf P}$ について 　

   1. 任意の対象 $a$ に対し
      
      $$(\forall x)({\bf P}(x)) \Rightarrow {\bf P}(a)$$
      
      
      　は定理です。

   2. 任意の自由変数 $a$ に対し $A\Rightarrow {\bf P}(a)$ が定理ならば
      $$\begin{eqnarray*} && A \Rightarrow (\forall x)({\bf P}(x)) \\ && (ただしA は任意の関係式) \end{eqnarray*}$$
      
      
      も定理です。
   3. 任意の対象 $a$ に対し
      
      $${\bf P}(a) \Rightarrow (\exists x)({\bf P}(x))$$
      
      
      は定理です。
   4. ある対象 $a$ に対し
      
      $${\bf P}(a) \Rightarrow A$$
      
      
      が定理ならば
      $$\begin{eqnarray*} && (\exists x)({\bf P}(x)) \Rightarrow A \\ && (ただしA は任意の関係式) \end{eqnarray*}$$
      
      
      も定理です。

   ((b))

   関係式 ${\bf P}$ と ${\bf Q}$ について

   1. 
      
      $$(\forall x)[{\bf P}(x) \land {\bf Q}(x)] \Leftrightarrow (\forall x)({\bf P}(x)) \land (\forall x)({\bf Q}(x))$$
      
      
      は定理です。
   2. 
      
      $$(\exists x)[{\bf P}(x) \lor {\bf Q}(x)] \Leftrightarrow (\exists x)({\bf P}(x)) \lor (\exists x)({\bf Q}(x))$$
      
      
      は定理です。

   ((c))

   1. 束縛変数を含む関係式 ${\bf Q}$ において，その束縛変数記号を ${\bf Q}$ に含 まれない他の束縛変数記号でおきかえて得られます関係式を ${\bf G}$ とすれば，
      
      $${\bf Q} \Leftrightarrow {\bf G}$$
      
      
      は定理です。 たとえば，
      
      $$(\forall x)({\bf P}(x)) \Leftrightarrow (\forall y)({\bf P}(y))$$
      
      
      
      
      $$(\exists x)({\bf P}(x)) \Leftrightarrow (\exists y)({\bf P}(y))$$
      
      
      は定理です。
   2. 関係式 ${\bf Q}$ において，ひき続いて現れる同種の限定記号の順序を変 更して得らる関係式を ${\bf G}$ とすれば，
      
      $${\bf Q} \Leftrightarrow {\bf G}$$
      
      
      は定理です。

      たとえば，
      

      $$(\forall x)( \forall y)({\bf P}(x,y)) \Leftrightarrow (\forall y)( \forall x)({\bf P}(x,y)),$$
      
      
      
      
      $$(\exists x)(\exists y)({\bf P}(x,y)) \Leftrightarrow (\exists y)(\exists x)({\bf P}(x,y))$$
      
      
      は定理です。
   3. 
      
      $$(\forall x)({\bf P}(x)) \Rightarrow (\exists x)({\bf P}(x))$$
      
      
      は定理です。

   4. 
      
      $$(\exists y)( \forall x)({\bf P}(x,y)) \Rightarrow (\forall x)( \exists y)({\bf P}(x,y))$$
      
      
      は定理です。

   ((d))

   関係式 ${\bf P},{\bf Q}$ について，以下は 定理です。

   1. 
      

      $$(\forall x)[{\bf P}(x) \Rightarrow {\bf Q}(x)] \Rightarr... ...(\forall x)({\bf P}(x)) \Rightarrow (\forall x)({\bf Q}(x))]$$
      
      

   2. 
      

      $$(\exists x)[{\bf P}(x) \Rightarrow {\bf Q}(x)] \Rightar... ...(\exists x)({\bf P}(x)) \Rightarrow (\exists x)({\bf Q}(x))]$$