§E16.9一階論理の標準形と Skolem 化

証明.$\varphi$の構文木は有限であるから、$\varphi$に現れる変数の集合と量化子の集合は有限である。変数集合は可算無限集合なので、$\varphi$に現れない相異なる変数を、量化子の個数だけ選ぶことができる。

構文木を根からたどり、各量化子$Qx$に、それまでに用いておらず、$\varphi$にも現れない変数$z$を一つ割り当てる。$Qx$が束縛する出現だけを$z$へ変更する。この変更では$z$が新鮮であるため変数捕獲は生じず、$\alpha$同値が保たれる。有限個の量化子について同じ操作を行うと、各量化子が相異なる変数を束縛し、束縛変数が元の自由変数と交わらない論理式$\varphi'$を得る。したがって$\varphi\equiv_\alpha\varphi'$である。▨

証明. 任意の$L$構造$M$と割当て$s$を固定する。第1式は、例えば$Q=\forall$の場合には

と$\exists$の意味から従う。$Q=\exists$の場合も同じ量化の否定から従う。

第2式で$Q=\forall$とする。左辺が偽であることは、$M,s\models\forall x\alpha$かつ$M,s\not\models\beta$と同値である。$x\notin FV(\beta)$と§E16.6 定理 4.1により、後者は任意の$a\in|M|$について$M,s[x\mapsto a]\not\models\beta$と同値である。したがって左辺が偽であることは、任意の$a$について$M,s[x\mapsto a]\models\alpha$であり、かつ$M,s[x\mapsto a]\not\models\beta$であることと同値である。この条件は$M,s\not\models\exists x(\alpha\to\beta)$と同値である。$Q=\exists$の場合には、左辺が偽であることが$M,s[x\mapsto a]\models\alpha$かつ$M,s[x\mapsto a]\not\models\beta$を満たす$a\in|M|$が存在することに等しく、右辺$\forall x(\alpha\to\beta)$の不成立と一致する。

第3式では、$x\notin FV(\beta)$により$\beta$の真理値が$s[x\mapsto a]$の$a$に依存しない。$\beta$が偽なら両辺は真であり、$\beta$が真なら両辺はそれぞれ$Qx\alpha$と同じ真理値をもつ。任意の$M,s$で各同値が成立するため、三つの式は論理的に同値である。▨

証明.補題 1.2により、$\varphi$を束縛変数が標準化された$\alpha$同値な論理式へ置き換える。§E16.6 定理 5.2により、$\alpha$同値な論理式の充足は一致するので、この置換は論理的同値を保つ。また、§E16.5 命題 5.4により自由変数集合も変わらない。以下では、標準化後の論理式とその各部分論理式について、「自由変数集合を保つ論理的に同値な冠頭標準形が存在する」という強化した主張を構造帰納法で証明する。

$\varphi$の構造に関する帰納法を用いる。原子式は量化子接頭部が空の冠頭標準形であり、自由変数集合も変わらない。$\alpha$が、帰納法の仮定により$Q_1x_1\cdots Q_mx_m\theta$と同値であるとする。補題 1.3の第1式を外側から順に用いると、$\neg\alpha$は$\overline Q_1x_1\cdots\overline Q_mx_m\neg\theta$と同値になる。量化子が束縛する変数と行列中の自由変数は変わらないので、変形後の自由変数集合は$FV(\neg\alpha)=FV(\alpha)$に等しい。

次に$\alpha\to\beta$を考える。帰納法の仮定により、$\alpha$と$\beta$をそれぞれ

へ変形することができる。束縛変数は全体で標準化されているため、各$x_i$は$\eta$に自由に現れず、各$y_j$は$\theta$に自由に現れない。第2式を$Q_1x_1,\ldots,Q_mx_m$へ、第3式を$R_1y_1,\ldots,R_ky_k$へ順に適用すると、

を得る。この論理式の行列は量化子を含まない。各量化子移動は、移動する変数が反対側の行列に自由に現れないという条件の下で行われるため、新しい自由変数を導入せず、既存の自由変数も束縛しない。従って、得られた論理式の自由変数集合は$FV(\alpha)\cup FV(\beta)=FV(\alpha\to\beta)$である。

$\forall x\alpha$の場合には、$\alpha$の冠頭標準形の先頭へ$\forall x$を付ければよい。全体の束縛変数は標準化されているため、$x$は$\alpha$の冠頭標準形の接頭部に現れる束縛変数とは異なる。帰納法の仮定から自由変数集合は

のままである。原始結合子$\neg,\to,\forall$のすべての場合を処理したので、構造帰納法により結論が従う。▨

証明.$\varphi$の接頭部を左から読み、全称量化された変数には任意の要素を割り当てる。存在量化された$x_i$に到達した場合には、その変数より左にある全称変数の現在の値を$a_1,\ldots,a_r$とし、$x_i$へ$f_i^N(a_1,\ldots,a_r)$を割り当てる。

すべての全称変数の値を固定すると、以上の規則は各存在変数の値を定める。$N\models\operatorname{Sk}(\varphi)$であるから、得られた値を Skolem 化後の行列へ代入すると行列は真である。§E16.7 定理 5.2により、この行列の真理値は、元の行列で各存在変数へ上記の値を割り当てた場合の真理値と一致する。全称変数の値は任意であり、各存在変数について実際の証人を与えたので、接頭部を右から左へ充足関係の定義に従って戻すと$N\mathbin{\upharpoonright}L\models\varphi^p$を得る。冠頭標準形定理により$\varphi$と$\varphi^p$は同値なので、$N\mathbin{\upharpoonright}L\models\varphi$である。▨

証明.定理 2.2により$M\models\varphi^p$である。接頭部を左から有限回たどる。最初の存在量化子$\exists x_i$に到達するまでの全称変数の値を$\bar a\in|M|^r$とする。それ以前の存在変数については、すでに構成した関数によって値が定まっている。充足関係の定義と、それまでの構成が残りの接尾部を真に保つという帰納法の仮定により、各$\bar a$に対して、残りの接尾部を真にする$x_i$の値の集合$W_{\bar a}$は空でない。

集合族$(W_{\bar a})_{\bar a\in|M|^r}$に選択公理を適用し、各$\bar a$に証人$b_{\bar a}\in W_{\bar a}$を選ぶ。$f_i^{M^{\mathrm{Sk}}}(\bar a)=b_{\bar a}$と定める。$r=0$の場合には添字集合が一元集合なので、同じ選択は一つの証人を選び、新しい定数の値とする操作である。この定義により、任意の先行全称変数の値について、残りの接尾部を真にする選択が固定される。

存在量化子は有限個なので、この操作を左から順に有限回反復することができる。後の存在変数を処理するとき、先行する存在変数の値は、すでに定めた Skolem 関数を先行全称変数へ適用した値である。したがって、後の Skolem 関数の外部引数には、先行する全称変数だけを用いればよい。

すべての新関数記号を以上の関数で解釈した拡大を$M^{\mathrm{Sk}}$とする。任意の全称変数の値に対して、構成した各関数は元の存在量化子の証人を与えるため、$M^{\mathrm{Sk}}$は Skolem 化後の量化子を含まない行列を満たす。ゆえに$M^{\mathrm{Sk}}\models\operatorname{Sk}(\varphi)$である。▨

証明.$\varphi$のモデルには定理 3.4を適用し、$\operatorname{Sk}(\varphi)$のモデルには定理 3.3を適用する。▨

証明. 各文の構文木は有限なので、各$\sigma$の存在量化子の出現集合は有限である。したがって、すべての出現の集合は$T$で添字付けられた有限集合の合併であり、集合である。各出現へ一つの有限項数の記号を割り当てても、新記号全体は集合である。

$N\models\operatorname{Sk}(T)$ならば、各$\sigma\in T$について定理 3.3を適用することができるので、$N\mathbin{\upharpoonright}L\models T$である。

逆に$M\models T$とする。各$\sigma\in T$について、定理 3.4の証明が与える Skolem 関数解釈の集合は空でない。異なる文には異なる新記号を割り当てたので、文ごとの解釈は互いに衝突しない。文ごとの空でない解釈候補からなる集合族に選択公理を適用し、すべての$\sigma$について解釈を同時に一つずつ選ぶ。選んだ解釈を合わせると$M$の一つの$L^{\mathrm{Sk}}$拡大$M^{\mathrm{Sk}}$が定まり、各$\operatorname{Sk}(\sigma)$を満たす。したがって$M^{\mathrm{Sk}}\models\operatorname{Sk}(T)$である。▨