冠頭標準形

ド・モルガンなどを用いれば，限定記号 $\forall \quad \exists$が 他の論理記号より，左側にあるように変形できる。これを冠頭標準形 $prenex \ normal \ form$ という。この節では冠頭標準形の導出法について述べる。

ここで簡単のため${\bf D}$を有限集合

$${\bf D}=\{a_1,a_2,a_3,\cdots,a_n \}$$

としておく。以下の結果は${\bf D}$が無限集合でも成り立つ。

$\lnot$の右側への移動

定理8.1

定義と定理$1.2$のド・モルガン則によれば，

$$\lnot (\forall x)({\bf P}(x)) = \lnot ({\bf P}(a_1) \land \cdots \land {\bf P}(a_n) )$$

$$= \lnot {\bf P}(a_1) \lor \lnot {\bf P}(a_1) \cdots \lor \lnot {\bf P}(a_n)$$

$$= (\exists x)(\lnot {\bf P}(x))$$ (3.50)

$$\lnot (\exists x)({\bf P}(x)) = \lnot ({\bf P}(a_1) \lor \cdots \lor {\bf P}(a_n) )$$

$$= \lnot {\bf P}(a_1) \land \lnot {\bf P}(a_1) \cdots \land \lnot {\bf P}(a_n)$$

$$= (\forall x)(\lnot {\bf P}(x))$$ (3.51)

を得る。

限定記号 $\forall,\exists$の左側への移動
${\bf P}(x)$と$x$を含まない$\cal B$について 定義と定理$1.2$によれば，定理$8.2$が成り立つ。

定理8.2

$${\cal B} \land (\forall x)({\bf P}(x)) = {\cal B} \land ({\bf P}(a_1) \land \cdots \land {\bf P}(a_n) )$$

$$= ({\cal B} \land {\bf P}(a_1)) \land \cdots \land ({\cal B} \land {\bf P}(a_n) )$$

$$=(\forall x)({\cal B} \land {\bf P}(x))$$ (3.52)

$${\cal B} \lor (\forall x)({\bf P}(x)) = {\cal B} \lor ({\bf P}(a_1) \land \cdots \land {\bf P}(a_n) )$$

$$= ({\cal B} \lor {\bf P}(a_1)) \land \cdots \land ({\cal B} \lor {\bf P}(a_n) )$$

$$=(\forall x)({\cal B} \lor {\bf P}(x))$$ (3.53)

$${\cal B} \land (\exists x)({\bf P}(x)) = {\cal B} \land ({\bf P}(a_1) \lor \cdots \lor {\bf P}(a_n) )$$

$$= ({\cal B} \land {\bf P}(a_1)) \lor \cdots \lor ({\cal B} \land {\bf P}(a_n) )$$

$$=(\exists x)({\cal B} \land {\bf P}(x))$$ (3.54)

$${\cal B} \lor (\exists x)({\bf P}(x)) = {\cal B} \lor ({\bf P}(a_1) \lor \cdots \lor {\bf P}(a_n) )$$

$$= ({\cal B} \lor {\bf P}(a_1)) \lor \cdots \lor ({\cal B} \lor {\bf P}(a_n) )$$

$$=(\exists x)({\cal B} \lor {\bf P}(x))$$ (3.55)

$${\cal B} \Rightarrow (\forall x)({\bf P}(x)) =\lnot {\cal B} \lor (\forall x)({\bf P}(x))$$

$$= \lnot {\cal B} \lor ({\bf P}(a_1) \land \cdots \land {\bf P}(a_n) )$$

$$= (\lnot {\cal B} \lor {\bf P}(a_1)) \land \cdots \land (\lnot {\cal B} \lor {\bf P}(a_n) )$$

$$=(\forall x)(\lnot {\cal B} \lor {\bf P}(x))$$

$$=(\forall x)( {\cal B} \Rightarrow {\bf P}(x))$$ (3.56)

$${\cal B} \Rightarrow (\exists x)({\bf P}(x)) =\lnot {\cal B} \lor (\exists x)({\bf P}(x))$$

$$= \lnot {\cal B} \lor ({\bf P}(a_1) \lor \cdots \lor {\bf P}(a_n) )$$

$$= (\lnot {\cal B} \lor {\bf P}(a_1)) \lor \cdots \lor (\lnot {\cal B} \lor {\bf P}(a_n) )$$

$$=(\exists x)(\lnot {\cal B} \lor {\bf P}(x))$$

$$=(\exists x)({\cal B} \Rightarrow {\bf P}(x))$$ (3.57)

$$(\forall x)({\bf P}(x)) \Rightarrow {\cal B} =\lnot (\forall x)({\bf P}(x)) \lor {\cal B}$$

$$= \lnot ({\bf P}(a_1) \land \cdots \land {\bf P}(a_n) ) \lor {\cal B}$$

$$= \lnot {\bf P}(a_1) \lor \lnot {\bf P}(a_1) \cdots \lor \lnot {\bf P}(a_n) \lor {\cal B}$$

$$= (\lnot {\bf P}(a_1) \lor {\cal B}) \lor (\lnot {\bf P}(a_1) \lor {\cal B}) \cdots \lor (\lnot {\bf P}(a_n) \lor {\cal B})$$

$$= (\exists x)(\lnot {\bf P}(x) \lor {\cal B})$$

$$= (\exists x)({\bf P}(x) \Rightarrow {\cal B})$$ (3.58)

$$(\exists x)({\bf P}(x)) \Rightarrow {\cal B} =\lnot (\exists x)({\bf P}(x)) \lor {\cal B}$$

$$= \lnot ({\bf P}(a_1) \lor \cdots \lor {\bf P}(a_n) ) \lor {\cal B}$$

$$= (\lnot {\bf P}(a_1) \land \lnot {\bf P}(a_1) \cdots \land \lnot {\bf P}(a_n) ) \lor {\cal B}$$

$$= (\lnot {\bf P}(a_1) \lor {\cal B}) \land (\lnot {\bf P}(a_1) \land {\cal B}) \cdots \land (\lnot {\bf P}(a_n) \lor {\cal B})$$

$$= (\forall x)(\lnot {\bf P}(x) \lor {\cal B})$$

$$= (\forall x)({\bf P}(x) \Rightarrow {\cal B})$$

冠頭標準形の導出法　
定理$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))$$
   
   

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 )$$
   
   
   の形の変形を繰り返し行う。

さらに以上の手順と主$\lor$標準形(主$\land$標準形)への変換アルゴリズム を併用することもできる。