スコーレム標準形

次のステップは

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

をスコーレム標準形と呼ばれる特殊な形の論理式に同値変形する。
この同値変形について以下に述べる。

1. 先ず，定理$7$と$8.1,8.2$により以下の手順で冠頭標準形を 導出する。
   1. 同じ変数名で自由変数と束縛変数が混在する場合は変数名を変更する。
      例えば
      

      $$(\exists x)({\bf P}(x,y)) \land (\forall y) ({\bf Q}(y,z)) =(\exists x)({\bf P}(x,y)) \land (\forall w) ({\bf Q}(w,z))$$ (5.13)

      
      

   2. $\lnot$の右側への移動
      定理$8.1$(ド・モルガン則)により
      
      $$\lnot \exists ( \cdots ) = \forall \lnot ( \cdots )$$
      
      
      
      
      $$\lnot \forall ( \cdots ) = \exists \lnot ( \cdots )$$
      
      
      の形の変形を行う。
   3. 限定記号 $\forall,\quad \exists$の左側への移動
      定理$8.2$により
      
      $$(\cdots \exists \cdots ) = \exists ( \cdots )$$
      
      
      
      
      $$(\cdots \forall \cdots ) = \forall ( \cdots )$$
      
      
      の形の変形を繰り返し行う。
   4. (主$\land$標準形)への変換アルゴリズム を併用する

2. スコーレム関数の導入
   上の手順で，限定記号全てが左側に移され，内側の論理式は (主$\land$標準形)への変換されている。
   

   ここで，限定記号のうち存在記号$\exists$を除去する スコーレム関数を導入する。この関数の構成原理は以下のものである。
   

   1. 対象領域${\bf D}$上で定義された$2$変数述語${\bf P}(x,y)$について 恒真論理式
      
      

      $$(\forall x \in {\bf D})(\exists y \in {\bf D}){\bf P}(x,y)$$ (5.14)

      
      
      が与えられたする。この論理式の意味するところは，

      「対象領域${\bf D}$上の任意の$x$に対して関係${\bf P}(x,y)$を充たす ${\bf D}$の元$y$が存在する。」
      である。各$x \in {\bf D}$についてそのような$y \in {\bf D}$ は複数あるもしれないが，その中から一つを選び，$f(x)$と名づければ

      
      

      $$(\forall x \in {\bf D})({\bf P}(x,f(x)))$$ (5.15)

      
      
      を充たす関数
      

      $$f: x \in {\bf D} \mapsto f(x) \in {\bf D}$$ (5.16)

      
      
      が定義されたことになる。

   2. 同様に対象領域${\bf D}$上で定義された$2$変数述語${\bf P}(x,y)$について 恒真論理式
      
      

      $$(\exists y \in {\bf D})(\forall x \in {\bf D}){\bf P}(x,y)$$ (5.17)

      
      
      が与えられたとする。これは
      

      $$(\forall x \in {\bf D}){\bf P}(x,c)$$ (5.18)

      
      
      を充たす${\bf D}$の要素$c$が存在することを示すものであるから， そのような要素$c$が一つ選択されたとして，値として$c$をとる$0$変数定数値関数 $f$を導入して，上の論理式を
      

      $$(\forall x \in {\bf D}){\bf P}(x,f)$$ (5.19)

      
      
      と書き換える。
   以上の操作によって論理式中から存在記号$\exists$を除去することが可能である。 ここで導入された$f$をスコーレム関数という。