安井邦夫、「現代論理学」、現代思想社 の分からない所メモ 第2弾

p188の$\fbox{15}$が分からない！

$\fbox{15}$ S(x,t,u):｢(x)$_0$は、表現(x)$_1$において、変項uの自由な表れすべてに項tを代入するとき、そこに得られる表現である。｣
S(x,t,u)は次の関係で定義される。

\begin{array}{ll} {VE(u) \amp TM(t) \amp} \{ \\ \quad [(x)_1 \equ u \amp (x)_0 \equ t ] \quad \lor & (1) \\ \quad [(\exi y)_{ y \lt (x)_1}((x)_1 \neq u \amp (x)_1 \equ 2^y \amp (x)_0 \equ (x)_1)] \quad \lor & (2) \\ \quad (\exi z)_{z \lt (x)_1} (\exi y)_{y \lt (x)_1} [ FM(y) \amp (x)_1 \equ 2^{13} * u * y * z \amp & (3.1) \\ \quad \quad (\exi r)_{r \lt (x)_0} ( (x)_0 \equ 2^{13} * u * y * r \amp S(2^r 3^z, t, u) ) \quad \lor & (3.2) \\ \quad [ \neg (\exi z)_{z \lt (x)_1} (\exi y)_{y \lt (x)_1} ( FM(y) \amp (x)_1 \equ 2^{13} * u * y * z ) \amp & (4.1) \\ \quad \quad (\exi p)_{p \lt (x)_0} (\exi r)_{r \lt (x)_0} (\exi y)_{y \lt (x)_1} ( 1 \lt y \amp (x)_1 \equ 2^{((x)_1)_0} * y \amp & (4.2) \\ \quad \quad (x)_0 \equ p * r \amp S(2^p 3^{2^{((x)_1)_0}}, t, u) \amp S(2^r 3^y, t, u) ) ] & (4.3) \\ \} \end{array}

※本来はテキストの表記に従うならば、これらの記号はゴシック体で書かなければならないが、$\TeX$の記述上イタリック体のままにしています。

この数論的関係が求めるべき関係になっていることの理解が難しい…。
(x)$_1$が操作を施す前の表現、(x)$_0$が操作を施した後の表現であり、従って両者$p_0^{\alpha(b_1)}p_1^{\alpha(b_2)} \cdots p_{m-1}^{\alpha(b_m)}$という形が想定されていることは分かる。
表現(x)$_{1}$を左から右へ向かって走査し、$\all u$(論理式)　となっているところはスルーしつつ、そうなっていない自由変項uをtに逐次書き換えて行っているのであろう事は分かる。

以下のように考えてみたのだが、これでいいのだろうか： \begin{array}{cl} (3.1) & \underline{今現在走査中たる}表現(x)_1が、\quad \all u \; 論理式y \; 表現z \quad となっていて、\\ & (この時は、y内の変項uは束縛変項だから置換の必要は無いのでスルー) \\ (3.2) & その表現z部分の自由変項uを項tで書き換えて得られた表現がrで、\\ & それを連接した \quad \all u \; 論理式y \; 表現r \quad が現時点での求める表現(x)_0 \\ (4.1) & 表現(x)_1が、\quad \all u \; 論理式y \; 表現z　\quad とはなっておらず \\ & (\all v \; \cdots \quad でも \quad ～P \quad でも \quad P \supset Q \quad でもOK) \\ (4.2) & (x)_1を、\quad (x)_1の第1文字目 \; 表現y \quad と分解して見ると、\\ & ((4.1)～(4.3)は帰納的走査の部分であるから、(x)_1の2文字目以降の表現が存在していなければならない) \\ (4.3) & その第1文字目を置換したのがp、yを置換したのがrで、pとrを連接したのが(x)_0 \\ \hline (1) & 表現(x)_1は、変項u \; 1文字からなる記号列なので、置換したら(x)_0 \equ t \\ (2) & 表現(x)_1は、変項uではない1文字からなる表現であるが故に置換されず、つまり(x)_0 \equ (x)_1 \\ \end{array}

「(1),(2)で1文字からなる記号列(x)$_1$の置換を考える」という手口を採用しているからこそ、帰納的置換を行う核心部分である(4.2),(4.3)において、「現在走査中の表現の左端1文字　と　それ以外」という分離を行っているのだろう。