§E16.7代入補題

証明. まず、各論理式の自由変数集合、$\operatorname{supp}(\sigma)$、$\operatorname{FV}(\sigma)$は有限である。$\mathrm{Var}$は無限であるから、第二の場合の有限集合$K$の外に変数$z$が存在する。

任意の有限集合$E\subseteq\mathrm{Var}$に対し、論理式$\theta$のすべての束縛変数を$E$の外へ捕獲回避的に改名した$\alpha$同値な論理式が存在することを示す。$\theta$に関する構造帰納法を用いる。原子、否定、含意では直下の論理式へ帰納法の仮定を適用する。$\theta=\forall x\,\eta$の場合、$E\cup\operatorname{Var}_{\mathrm{all}}(\eta)$と、帰納的にすでに選んだ有限個の束縛変数の外から新しい$z$を選ぶ。外側を$z$に改名してから直下の論理式へ帰納法の仮定を適用する。構文木が有限であるから選択を要する変数は有限個である。以上の主張を新変数化補題と呼ぶ。

表示された節に従って論理式の高さに関する再帰を行えば、少なくとも一つの結果を構成することができる。量化の場合も、再帰呼出しは直下の論理式に対して行われるため停止する。ただし、この段階では再帰の途中で選んだ新変数を記録した代表式を出力とし、well-defined 性はまだ仮定しない。

well-defined 性に必要な改名と代入の可換性を先に証明する。$\eta[x\rightsquigarrow z]$により、外側の量化子$\forall x$が束縛する出現だけを$z$へ改名した本体を表す。$z,u$が

の外にあるとき、高さが$\eta$以下である再帰結果について

が成り立つ。これを項と論理式に関する同時構造帰納法で示す。原子式では、外側の$x$に束縛された変数だけが$z$または$u$となり、ほかの変数の代入像には$z,u$が現れない。したがって左辺の外側の$z$を$u$へ改名すると、両本体は項ごとに一致する。否定と含意では直下の帰納法の仮定を用いる。内側が$\forall y\,\xi$の場合は三つに分かれる。$y=x$なら内側の量化子が外側の束縛を遮断するため、その本体では改名しない。$y=z$または$y=u$は新鮮性から改名前の$\eta$には生じない。$y$が$x,z,u$と異なるなら、外側の改名と$y$による遮断は可換であり、直下へ帰納法の仮定を適用する。直下の代入がさらに量化変数を改名するときは、二つの有限な禁止集合の外から同じ変数を選び、同じ議論を一段低い論理式へ適用する。以上は高さの小さい再帰結果だけを用い、証明しようとしている well-defined 性を用いていない。

この可換性から、任意の外側変数$y$に対する次の強化命題を得る。$u$が$\operatorname{Var}_{\mathrm{all}}(\theta)\cup\operatorname{supp}(\sigma) \cup\operatorname{FV}(\sigma)\cup\{y\}$の外にあるなら、表示した再帰規則が$(\forall y\,\theta)\sigma$に対して作る任意の raw 結果は

に$\alpha$同値である。第二規則が新変数$z$を選ぶ場合は (1) を$z,u$に適用する。第一規則が$y$を保つ場合は$y\notin\operatorname{FV}(\sigma\setminus y)$である。したがって$\theta(\sigma\setminus y)$に代入から生じた自由な$y$はなく、外側の$y$を$u$へ捕獲回避的に改名することができる。項、否定、含意、および内側の量化子について上と同じ同時帰納法を用いると、改名後の本体は$(\theta[y\rightsquigarrow u])(\sigma\setminus u)$と$\alpha$同値になる。この場合分けにより、もとの代表元の束縛変数$y$自身が$\operatorname{supp}(\sigma)$に属する場合も強化命題の対象になる。

新変数選択の diamond 性を示す。量化節で$z$と$w$を選んだ二つの結果に対し、両方の禁止集合と$\{z,w\}$の外から$u$を選ぶ。(1) を$z,u$と$w,u$にそれぞれ適用すると、両結果は同じ$u$を外側の束縛変数とする結果へ$\alpha$同値である。したがって二つの選択から得た結果も互いに$\alpha$同値である。

次に代表元からの独立性を示す。$\alpha$同値の一回の生成規則

を考え、両代表元と$\sigma$の禁止集合の外から共通の$u$を選ぶ。左の代表元と右の代表元へ強化命題 (2) を適用すると、両方の raw 結果は、いずれも

に$\alpha$同値である。否定、含意、全称量化の合同規則には直下の論理式に対する帰納法の仮定を適用する。さらに$\alpha$同値の導出について帰納し、反射律、対称律、推移律を順に用いれば、任意の二代表元が同じ出力類を与える。これは生成規則、合同規則、同値閉包をすべて扱っており、単なる新変数選択の独立性だけではない。

最後に一意性を示す。同じ節を満たす二つの操作を取る。原子、否定、含意では構造帰納法により出力類が一致する。量化では両方の出力を強化命題 (2) により共通の新変数へ移し、直下の論理式に対する帰納法の仮定を用いる。ゆえにすべての論理式で出力の$\alpha$同値類が一致する。▨

証明.$x\notin\operatorname{supp}(\sigma)\cup\operatorname{supp}(\tau)$なら$\rho(x)=(x)\tau=x$である。したがって$\operatorname{supp}(\rho)$は二つの有限集合の和に含まれ、有限である。

(2)を$t$に関する構造帰納法で示す。$t=x$の場合は合成の定義そのものである。定数の場合は両辺が同じ定数である。関数適用の場合は各引数に帰納法の仮定を適用する。

(3)を示す。新変数化補題により、$\varphi$の束縛変数を

の外へ改名した代表元を選ぶ。入力代表元と新変数の選択からの独立性は定理 2.2で証明済みであるため、この代表元で比較すれば十分である。

原子の場合は(2)を各項へ適用する。否定と含意の場合は直下の論理式に対する帰納法の仮定を用いる。$\varphi=\forall x\,\psi$の場合、$x$は$E$の外にあるので、三つの代入はいずれも$x$を固定し、代入項に$x$は現れない。したがって量化の定理 2.2 条件 (a)だけが適用され、

ここで、制限した代入の合成が$\rho\setminus x$に等しいことを変数ごとに確認する。$y=x$では

である。$y\ne x$では、$x\notin\operatorname{FV}(\sigma)$であるから$x$は項$\sigma(y)$に現れず、項への代入の定義より

となる。したがって二つの制限代入は実際に等しい。帰納法の仮定により直下は$\psi(\rho\setminus x)$と$\alpha$同値であるから、右辺は$(\forall x\,\psi)\rho$と$\alpha$同値である。この議論は量化節での制限と合成の交換を省略せず、量化が入れ子になった場合にも各段で同じ等式を用いる。▨

証明.$t$に関する構造帰納法を用いる。$t=x$の場合、左辺は$\llbracket\sigma(x)\rrbracket_s^{\mathcal M}=s_\sigma(x)$であり、右辺も同じ値である。定数の場合は両辺が$c^{\mathcal M}$である。関数適用の場合は各引数に帰納法の仮定を適用し、同じ関数$f^{\mathcal M}$を用いる。▨

証明. 任意の変数$x$について、項評価代入補題を$t=\sigma(x)$に適用すると

となる。したがって割当ては等しい。▨

証明. 変数$y$ごとに値を比較する。$y=x$なら左辺は$\llbracket x\rrbracket_{s[x\mapsto a]}^{\mathcal M}=a$であり、右辺も$a$である。$y\ne x$なら$(\sigma\setminus x)(y)=\sigma(y)$である。仮定により$x\notin\operatorname{Var}(\sigma(y))$であるから、項評価の局所性により

右辺の更新も$y\ne x$では$s_\sigma(y)$である。▨

証明. 捕獲回避代入と充足はともに$\alpha$同値で不変である。新変数化補題により、$\varphi$のすべての束縛変数が$\operatorname{FV}(\sigma)\cup\operatorname{supp}(\sigma)$の外にある代表元を選ぶ。この代表元について構造帰納法を用いる。

等号原子と関係原子の場合、補題 4.2を各項へ適用すると両辺の項の値が一致する。否定と含意の場合は充足関係の対応する節と帰納法の仮定から従う。

$\varphi=\forall x\,\psi$とする。代表元の選択により$x\notin\operatorname{FV}(\sigma\setminus x)$であり、

したがって

第二の同値は帰納法の仮定、第三の同値は補題 5.1による。以上で量化の場合も閉じる。▨

証明.$\sigma(x)=t$、$y\ne x$では$\sigma(y)=y$とする。自由代入可能性により$\varphi\sigma\equiv_\alpha\varphi[t/x]$である。実際、捕獲回避代入が、置換される$x$の自由出現を支配しない量化子を新鮮化する場合、通常代入との間に生じる差は束縛変数名だけである。例えば$x$が現れない$\forall y\,R(z)$へ$t=y$を指定すると、通常代入は元の式を保つ一方、捕獲回避代入は代表元として$\forall w\,R(z)$を選ぶことがあるが、両者は$\alpha$同値である。置換される自由出現を支配する量化子では、自由代入可能性により$t$の変数は捕獲されず、直下の式に対する同じ主張を構造帰納的に用いることができる。また

である。§E16.6 定理 5.2で$\varphi[t/x]$から$\varphi\sigma$へ移り、定理 5.2 (充足代入補題)を適用すれば主張を得る。▨