構文操作の原始再帰性 | 数理論理

1 構文木のタグ

変数を $v_0,v_1,\ldots$ と列挙する。次の相異なる標準自然数をタグとして固定する。

\begin{array}{c|cccccccccc} \text{タグ}&1&2&3&4&5&6&7&8&9\\ \hline \text{構成子}&\mathrm{Var}&\mathrm{Zero}&\mathrm{Succ}&\mathrm{Add}&\mathrm{Mul} &\mathrm{Eq}&\mathrm{Neg}&\mathrm{Imp}&\mathrm{All} \end{array}

定義 1.1.§E19.17 定義 2.1の有限列符号を用いて、構成子を次の全域関数で表す。

\begin{aligned} \operatorname{Var}(i)&=\operatorname{SeqCode}(1,i),\\ \operatorname{Zero}&=\operatorname{SeqCode}(2),\\ \operatorname{Succ}(t)&=\operatorname{SeqCode}(3,t),\\ \operatorname{Add}(t,u)&=\operatorname{SeqCode}(4,t,u),\\ \operatorname{Mul}(t,u)&=\operatorname{SeqCode}(5,t,u),\\ \operatorname{Eq}(t,u)&=\operatorname{SeqCode}(6,t,u),\\ \operatorname{NegRaw}(y)&=\operatorname{SeqCode}(7,y),\\ \operatorname{ImpRaw}(y,z)&=\operatorname{SeqCode}(8,y,z),\\ \operatorname{AllRaw}(i,y)&=\operatorname{SeqCode}(9,i,y). \end{aligned}

自然数 $y$ が項符号 (term code) であるとは、Var、Zero、Succ、Add、Mul の規則から有限回で作られることをいう。自然数 $y$ が論理式符号 (formula code) であるとは、項符号 $t,u$ に対する Eq $(t,u)$ から始め、NegRaw、ImpRaw、AllRaw により有限回で作られることをいう。

各構成子は Cons、固定長の有限列、および定数との合成なので原始再帰的である。定数タグを関数として用いる箇所では、単項ダミー定数関数 $C_c(x)=c$ を用いる。零項の自然数関数を初期関数へ追加したわけではない。

補題 1.2. 次の二つが成り立つ。

構文符号 $y$ の直下に現れる項または論理式の符号 $u$ は $u<y$ を満たす。変数添字も、それを含む Var 符号より小さい。
項符号または論理式符号 $y$ に自由に現れる変数の添字 $i$ は $i<y$ を満たす。これは $y$ の直下に現れる添字だけでなく、入れ子の任意の深さに現れる自由な添字について成り立つ。

証明.主張 (1)を示す。 $u$ は $y$ を表す右入れ子の Cons 列の成分である。 $\operatorname{Cons}(a,t)=1+\operatorname{pair}(a,t)$ であり、 $\operatorname{pair}(a,t)\ge a,t$ なので、各成分と各尾は Cons 全体より小さい。外側のタグを含む Cons について同じ評価を行えば $u<y$ を得る。Var の添字についても同じである。

主張 (2)を、 $y$ の構成に関する帰納法で示す。主張 (1)では直下の一段しか述べられていないので、入れ子の深さについての帰納法をここで別に行う。 $y=\operatorname{Var}(j)$ では、自由に現れる添字は $j$ だけであり、主張 (1)により $j<y$ である。 $y=\operatorname{Zero}$ では自由に現れる添字が無い。 Succ、Add、Mul、Eq、NegRaw、ImpRaw では、 $y$ に自由に現れる添字 $i$ は直下の対象 $u$ のいずれかに自由に現れるので、帰納法の仮定により $i<u$ であり、主張 (1)の $u<y$ と合わせて $i<y$ である。 $y=\operatorname{AllRaw}(j,z)$ では、 $y$ に自由に現れる添字 $i$ は $i\ne j$ を満たし $z$ に自由に現れるので、同じく $i<z<y$ である。▨

2 項、論理式、文の判定

定義 2.1. $\operatorname{Term}(y)$ (term-code predicate) は、 $y$ の長さと各成分を調べ、次のいずれかが成り立つことを表す。

$y=\operatorname{Var}(i)$ である。
$y=\operatorname{Zero}$ である。
$y=\operatorname{Succ}(t)$ かつ $\operatorname{Term}(t)$ である。
$y=\operatorname{Add}(t,u)$ または $y=\operatorname{Mul}(t,u)$ であり、 $\operatorname{Term}(t)$ かつ $\operatorname{Term}(u)$ である。

$\operatorname{Formula}(y)$ (formula-code predicate) は次のいずれかが成り立つことを表す。

$y=\operatorname{Eq}(t,u)$ かつ $\operatorname{Term}(t)$ かつ $\operatorname{Term}(u)$ である。
$y=\operatorname{NegRaw}(z)$ かつ $\operatorname{Formula}(z)$ である。
$y=\operatorname{ImpRaw}(z,w)$ かつ $\operatorname{Formula}(z)$ かつ $\operatorname{Formula}(w)$ である。
$y=\operatorname{AllRaw}(i,z)$ かつ $\operatorname{Formula}(z)$ である。

$\operatorname{Free}(y,i)$ (free-variable predicate) は、論理式または項 $y$ に変数 $v_i$ が自由に現れることを表す。 $\operatorname{Sentence}(y)$ (sentence-code predicate) は

\operatorname{Formula}(y)\land \forall i\le y\,\neg\operatorname{Free}(y,i)

と定める。

Free の再帰節は通常の構文定義そのものである。Var $(j)$ では $i=j$ 、Zero では偽、関数構成子と Eq、NegRaw、ImpRaw では直下の対象の選言を取る。 AllRaw $(j,z)$ では $i=j$ なら偽、 $i\ne j$ なら Free $(z,i)$ とする。 $v_i$ が $y$ に自由に現れるなら補題 1.2 (2)により $i<y$ なので、Sentence の有界全称量化の範囲 $i\le y$ は、 $y$ に自由に現れる変数の添字をすべて含む。

定理 2.2. Term、Formula、Free、Sentence は正のアリティをもつ原始再帰関係である。

証明. Len、Entry、等号、有限の場合分けは原始再帰的である。 Term、Formula、Free を一つの有限分岐評価へ具体化する。要求の種類を

\operatorname{Req}_{\rm T}(y),\qquad \operatorname{Req}_{\rm F}(y),\qquad \operatorname{Req}_{\rm free}(y,i)

の三つとし、階数をいずれも $y$ とする。Term 要求では Succ に一つ、Add と Mul に二つの Term 要求を子として割り当てる。Formula 要求では Eq に二つの Term 要求、NegRaw に一つの Formula 要求、 ImpRaw に二つの Formula 要求、AllRaw に一つの Formula 要求を割り当てる。Free 要求では、Var と Zero は子をもたず、各一項構成子に一つ、各二項構成子に二つの同じ添字 $i$ をもつ Free 要求を割り当てる。 AllRaw $(j,z)$ では $i=j$ なら子をもたず偽を返し、 $i\ne j$ なら Req $_{\rm free}(z,i)$ を唯一の子とする。親の結合関数はタグに応じて、子の特性値の連言または選言を取る。不正なタグでは子をもたず偽を返す。

子の個数は高々 $2$ であり、すべての子の第1成分は補題 1.2 (1)により $y$ より小さい。要求の生成と親での結合は Len、Entry、等号、および有限の場合分けから原始再帰的である。したがって§E19.17 補題 3.2を $K=2$ で適用することができる。この適用では、 Eq の二つの Term 値、Add、Mul、ImpRaw の左右二つの値を同じ親が実際に受け取るため、一つの子の値だけを読む再帰に置き換えてはいない。

Sentence は Formula、Free、および $i\le y$ の有界全称量化の合成である。原始再帰関係は有界量化について閉じているため Sentence も原始再帰的である。▨

3 数詞と捕獲回避代入

定義 3.1 (数詞符号).

\operatorname{Num}(0)=\operatorname{Zero}, \qquad \operatorname{Num}(n+1)=\operatorname{Succ}(\operatorname{Num}(n))

と定める。 $\operatorname{Num}$ を数詞符号関数 (numeral-code function) という。Num $(n)$ は数詞 $\overline n$ の項符号である。

Num はパラメータ列が空の原始再帰である。基底は自然数 Zero であり、再帰引数 $n$ が残るため Num は一変数関数である。

捕獲を避けるため、束縛変数の改名を記録する環境を用いる。環境 $E$ は $\operatorname{pair}(i,j)$ の有限列である。 $E$ の最も左にある $\operatorname{pair}(i,j)$ を、現在有効な束縛 $v_i$ の新しい名前 $v_j$ と読む。第1成分が $i$ である成分が一つも無ければ、 $v_i$ を未束縛とする。環境を先頭から調べて $v_i$ の新しい名前を求める関数を $\operatorname{Look}$ と書き、その原始再帰的定義列を次の一つに固定する。後続の記事では、原始再帰性だけでなく、この定義列が満たす等式を対象理論の内部で用いるからである。

定義 3.2 (環境の走査). 環境検索関数 (environment-lookup function) $\operatorname{Look}(E,i)$ を、第2引数 $i$ をパラメータとし、第1引数 $E$ を再帰引数とする次のコース再帰で定める。

\operatorname{Look}(0,i)=0, \qquad \operatorname{Look}(E,i)= \begin{cases} S\operatorname{right}(\operatorname{Head}(E)) &\operatorname{left}(\operatorname{Head}(E))=i,\\ \operatorname{Look}(\operatorname{Tail}(E),i)&\text{それ以外} \end{cases} \quad(0<E)

ここで $\operatorname{left}$ と $\operatorname{right}$ は§E19.17 補題 1.2の対関数の逆、 $\operatorname{Head}$ と $\operatorname{Tail}$ は§E19.17 定義 2.1の先頭と尾である。

§E19.17 補題 1.2の $\operatorname{left}(\operatorname{pair}(i,j))=i$ と $\operatorname{right}(\operatorname{pair}(i,j))=j$ により、 $\operatorname{Look}(E,i)$ は、 $E$ の成分を先頭から順に調べ、第1成分が $i$ に一致する最初の成分 $\operatorname{pair}(i,j)$ についてその第2成分 $j$ の後続者 $Sj$ を返し、一致する成分が一つも無ければ $0$ を返す。したがって「 $E$ が $i$ の対応先をもつ」ことは $\operatorname{Look}(E,i)\ne0$ と同値であり、そのときの対応先は $\operatorname{Look}(E,i)=Sj$ を満たす $j$ である。とくに $\operatorname{Look}(0,i)=0$ であり、 $\operatorname{Cons}(p,E)$ の先頭と尾が $p$ と $E$ であることから、 $\operatorname{Look}\bigl(\operatorname{Cons}(\operatorname{pair}(i',j),E),i\bigr)$ は $i'=i$ のとき $Sj$ 、 $i'\ne i$ のとき $\operatorname{Look}(E,i)$ に等しい。§E19.17 命題 2.2により $0<E$ のとき $\operatorname{Tail}(E)<E$ が成り立つので、この再帰は§E19.17 補題 3.1の形であり、 $\operatorname{Look}$ は正のアリティをもつ原始再帰全関数である。

定義 3.3. $\operatorname{WalkTerm}(y,v,t,E)$ と $\operatorname{WalkFormula}(y,v,t,E)$ (capture-avoiding substitution functions) を次の構文再帰で定める。

Var $(i)$ では、 $\operatorname{Look}(E,i)\ne0$ ならば $\operatorname{Look}(E,i)=Sj$ を満たす $j$ について Var $(j)$ を返す。 $\operatorname{Look}(E,i)=0$ かつ $i=v$ なら $t$ 、 $\operatorname{Look}(E,i)=0$ かつ $i\ne v$ なら Var $(i)$ を返す。
Zero は Zero を返し、Succ、Add、Mul、Eq、NegRaw、ImpRaw は直下の対象へ同じ操作を適用して再構成する。
AllRaw $(i,z)$ では、次の三つがすべて成り立つときに限り
$j=1+y+t+E+v+i$
とし、それ以外の場合は $j=i$ とする。
1. $\operatorname{Look}(E,v)=0$ であること、すなわちこの量化子より外側に $v_v$ を束縛する量化子が無いことである。
2. $i\ne v$ であることである。
3. $v_i$ が $t$ に自由に現れ、かつ $v_v$ が $z$ に自由に現れることである。
改名を発動する場合と発動しない場合のいずれにおいても、pair $(i,j)$ を $E$ の先頭へ追加し、元の真部分符号 $z$ を一度だけ再帰的に処理して AllRaw $(j,-)$ を返す。

一般の項符号 $t$ による代入を

\operatorname{SubTermCode}(y,v,t)= \begin{cases} \operatorname{WalkTerm}(y,v,t,0)&\operatorname{Term}(y)\land\operatorname{Term}(t),\\ \operatorname{WalkFormula}(y,v,t,0)&\operatorname{Formula}(y)\land\operatorname{Term}(t),\\ 0&\text{それ以外} \end{cases}

とする。下流で用いる数詞代入 API は

\operatorname{Sub}(y,v,n) =\operatorname{SubTermCode}(y,v,\operatorname{Num}(n))

である。

選んだ $j$ は $y,t,E,v,i$ より大きい。構文中のすべての変数添字はその構文符号より小さいので、 $v_j$ は対象 $y$ と代入項 $t$ のいずれにも現れない。環境 $E$ については、 $\operatorname{pair}$ が両引数以上の値を返し、 $\operatorname{Cons}$ が両引数より大きい値を返すことを用いる。 $E$ は右入れ子の Cons 列であるから、その各成分 $p$ は $p<E$ を満たす。成分 $p=\operatorname{pair}(k,k')$ に現れる添字は $k,k'\le p$ を満たすので、 $k,k'<E<j$ である。よって $v_j$ は対象、代入項、現在の環境のいずれにも現れない新鮮変数である。 $\operatorname{Look}$ は環境を先頭から調べるので、同名の量化子が入れ子になった場合には最も内側の束縛が優先される。

改名の条件に条件 (3-a)と条件 (3-b)を置くのは、その量化子の下で実際に代入が起こる場合に限って改名するためである。条件 (3-b)が破れる場合、すなわち $i=v$ の場合、 $v_v$ は AllRaw $(i,z)$ に自由に現れず、この部分符号のどこにも $t$ は入らない。条件 (3-a)が破れる場合、すなわち外側にすでに $v_v$ の束縛がある場合も、 $z$ に現れる $v_v$ はその束縛に属するので $t$ は入らない。どちらの場合にも捕獲は起こり得ないので、改名は不要である。これらの場合にも pair $(i,j)$ を $j=i$ として環境へ追加するため、 $i=v$ のときは更新後の環境 $E'=\operatorname{Cons}(\operatorname{pair}(i,i),E)$ について $\operatorname{Look}(E',v)$ が $Si$ を返す。そのため、 $z$ の中の $v_v$ は代入対象ではなく束縛出現として扱われる。 $i=v$ のときに改名を発動させると、 $\operatorname{AllRaw}(i,z)$ を返すべき場合に $\operatorname{AllRaw}(j,-)$ （ $j\ne i$ ）を返すことになる。そのため、代入対象が自由に現れない論理式を代入が変えないという性質が破れる。

定理 3.4. Num、SubTermCode、および Sub は正のアリティをもつ原始再帰全関数である。整形式入力では SubTermCode が名前付き構文に対する捕獲回避代入の符号を返し、Sub $(y,v,n)$ は自由な $v_v$ へ数詞 $\overline n$ を代入した符号を返す。

証明. Num は表示した通常の原始再帰で得る。環境の走査 $\operatorname{Look}$ は、定義 3.2が固定したとおり、 $0<E$ について $\operatorname{Tail}(E)<E$ を減少量とするコース再帰であり、§E19.17 補題 3.1により原始再帰的である。親節で用いる $\operatorname{Head}$ 、 $\operatorname{left}$ 、 $\operatorname{right}$ 、等号判定、および有限の場合分けはいずれも原始再帰的である。新鮮変数 $j$ の計算、環境への Cons、Free の判定、および各構成子も原始再帰的である。

WalkTerm と WalkFormula を

\operatorname{Req}_{\rm WT}(y,v,t,E),\qquad \operatorname{Req}_{\rm WF}(y,v,t,E)

という二種類の要求として、階数 $y$ 、最大子数 $K=2$ の有限分岐評価へ移す。 Succ、NegRaw、AllRaw は一つ、Add、Mul、Eq、ImpRaw は左右二つの要求を子にもつ。二項構成子の左右の子は同じ $v,t,E$ を受け取り、親の結合関数は返った二つの値から構成子を再構成する。 AllRaw $(i,z)$ では、表示した原始再帰的な場合分けで $j$ を計算する。改名を発動させる三条件は、 $\operatorname{Look}(E,v)=0$ という零判定、 $i\ne v$ という等号判定、および Free の二つの判定の連言である。 $\operatorname{Look}$ は上で見たとおり原始再帰的であり、等号判定と零判定は原始再帰的で、Free は定理 2.2により原始再帰的である。したがって、この場合分けを加えても親節は原始再帰関数の合成のままであり、原始再帰性は壊れない。この $j$ から

E'=\operatorname{Cons}(\operatorname{pair}(i,j),E)

を作り、Req $_{\rm WF}(z,v,t,E')$ を唯一の子とする。親はその子の値 $b$ から AllRaw $(j,b)$ を返す。したがって、再帰的に呼び出される第1成分は常に元の構文 $y$ の真部分符号である一方、補助環境は親の $E$ ではなく更新済みの $E'$ でよい。改名後の構文全体を再帰引数にしないため、 $z<y$ という階数の減少も保たれる。

要求の生成と親の結合は原始再帰的であるから、§E19.17 補題 3.2を適用すると、有限スタックの接頭トレースを長さに関する通常の原始再帰で作ることができる。これにより、二つの子の値と再帰呼出しごとの環境変更をともに扱った WalkTerm と WalkFormula が原始再帰的になる。不正入力を零判定と場合分けで $0$ へ送れば全域性も保たれる。

正しさは元の構文 $y$ に関する構造帰納法で示す。変数の場合、環境にある変数は束縛出現として改名され、環境にない $v_v$ だけが $t$ へ置き換わる。各関数・論理結合子では帰納法の仮定を各直下の対象へ適用する。例えば Add と ImpRaw では、左右二つの子要求がそれぞれの変換値を返し、親がその二値を同じ構成子へ戻す。量化子 $\forall v_i\,\theta$ では、改名の三条件のいずれかが破れる場合に名前を保つ。外側にすでに $v_v$ の束縛がある場合（定義 3.3 条件 (3-a)が破れる場合）と $i=v$ の場合（定義 3.3 条件 (3-b)が破れる場合）には、 $\theta$ の中の $v_v$ の出現がすべて束縛出現であり $t$ が入らないので、捕獲は起こり得ない。束縛変数が $t$ に自由に現れない場合、または置換対象が本体に自由に現れない場合（定義 3.3 条件 (3-c)が破れる場合）も同様である。捕獲が実際に起こり得る場合だけ、どこにも現れない $v_j$ へ束縛とその束縛出現を同時に改名するため、 $t$ の自由変数は捕獲されない。同名の量化子 $\forall v_i\forall v_i\,\theta$ では、内側で追加した pair $(i,j')$ が環境の先頭にあり、外側の pair $(i,j)$ を遮断する。さらに $\operatorname{Look}(E,v)=0$ 、 $i\ne v$ 、 $v_i$ が $t$ に自由に現れ、 $v_v$ が $\theta$ に自由に現れる $\forall v_i\,\theta$ では、子要求だけが $E'$ を受け取るため、結果は $\forall v_j\,\theta'$ となり、 $t$ に由来する自由な $v_i$ は束縛されない。よって得た符号は捕獲回避代入の結果である。▨

4 否定、含意、公理例

定義 4.1 (全域構文操作 Neg と Imp).

\begin{aligned} \operatorname{Neg}(y)&= \begin{cases}\operatorname{NegRaw}(y)&\operatorname{Formula}(y),\\0&\text{それ以外},\end{cases}\\ \operatorname{Imp}(y,z)&= \begin{cases}\operatorname{ImpRaw}(y,z)&\operatorname{Formula}(y)\land\operatorname{Formula}(z),\\0&\text{それ以外}.\end{cases} \end{aligned}

$\operatorname{Neg}$ を全域否定符号関数 (total negation-code function)、 $\operatorname{Imp}$ を全域含意符号関数 (total implication-code function) という。

Neg と Imp は構成子、構文判定、および有限の場合分けの合成なので原始再帰全関数である。

算術言語 $L_A$ の Hilbert 型体系をここで局所的に固定する。論理式符号 $a,b,c$ に対する命題公理は、次の三つの構文木パターンである。

\begin{aligned} \mathrm{H1}(a,b)&=\operatorname{ImpRaw}(a,\operatorname{ImpRaw}(b,a)),\\ \mathrm{H2}(a,b,c)&=\operatorname{ImpRaw}\bigl( \operatorname{ImpRaw}(a,\operatorname{ImpRaw}(b,c)), \operatorname{ImpRaw}(\operatorname{ImpRaw}(a,b),\operatorname{ImpRaw}(a,c))\bigr),\\ \mathrm{H3}(a,b)&=\operatorname{ImpRaw}\bigl( \operatorname{ImpRaw}(\operatorname{NegRaw}(b),\operatorname{NegRaw}(a)), \operatorname{ImpRaw}(a,b)\bigr). \end{aligned}

連言と双条件を原始構成子へ展開した符号を

\begin{aligned} \operatorname{AndCode}(a,b) &=\operatorname{NegRaw}(\operatorname{ImpRaw}(a,\operatorname{NegRaw}(b))),\\ \operatorname{IffCode}(a,b) &=\operatorname{AndCode}(\operatorname{ImpRaw}(a,b),\operatorname{ImpRaw}(b,a)) \end{aligned}

と定める。また $e_0=\operatorname{Eq}(\operatorname{Zero},\operatorname{Zero})$ と置き、空連言の符号を

\operatorname{Top}_A=\operatorname{ImpRaw}(e_0,e_0)

に固定する。したがって、零項関数 $0$ の合同公理でも空連言を省略せず、この一つの符号を前件として用いる。

項 $t$ が論理式 $\varphi$ の変数 $v_i$ へ自由に代入可能であることを FreeFor $(t,i,\varphi)$ と書く。原子式では真とし、否定と含意では直下の論理式の条件を取る。 $\forall v_j\psi$ では、 $j=i$ なら真、 $j\ne i$ なら

\operatorname{FreeFor}(t,i,\psi)\land \bigl(\neg\operatorname{Free}(\psi,i)\lor\neg\operatorname{Free}(t,j)\bigr)

とする。この判定を Req $_{\rm ff}(t,i,\varphi)$ という要求で表し、階数を $\varphi$ の符号とする。否定と量化には高々一つ、含意には左右二つの子要求を割り当て、親で表示した連言を取る。子の論理式符号は真部分符号であり、その階数は親の階数より真に小さいので、§E19.17 補題 3.2を $K=2$ で適用することができる。したがって FreeFor も原始再帰的である。

以下で§E19.10 定義 1.1 (H1)–§E19.10 定義 1.1 (H3)、§E19.10 定義 1.1 (Q1)、§E19.10 定義 1.1 (Q2)と書くのは§E19.10 定義 1.1で定められた一階 Hilbert 系の論理公理スキーマであり、Robinson 算術 $Q$ の公理§E19.15 定義 2.1 (Q1)–§E19.15 定義 2.1 (Q7)とは別のものである。名前が重なるのは量化子の二つの公理スキーマだけなので、以下ではこの二つの公理スキーマを全称具体化の公理§E19.10 定義 1.1 (Q1)と全称分配の公理§E19.10 定義 1.1 (Q2)と呼び、どちらの体系の公理であるかを明示する。

定義 4.2. $\operatorname{LogAx}(y)$ (logical-axiom instance predicate) は、以下の有限個のコードパターンのいずれかへ一致することを表す。表示する小文字の式符号には Formula、項符号には Term を要求し、同じ文字を置いた位置では同じ自然数符号を要求する。

$y=\mathrm{H1}(a,b)$ 、 $y=\mathrm{H2}(a,b,c)$ 、または $y=\mathrm{H3}(a,b)$ である。
次の三つをすべて満たす $i,t,a,b\le y$ が存在する。 $y=\operatorname{ImpRaw}(\operatorname{AllRaw}(i,a),b), \quad \operatorname{FreeFor}(t,i,a), \quad b=\operatorname{SubTermCode}(a,i,t)$ これは全称具体化の公理§E19.10 定義 1.1 (Q1)の $\forall v_i\varphi\to\varphi[v_i:=t]$ を表す。
次の等式と $\neg\operatorname{Free}(a,i)$ をともに満たす $i,a,b\le y$ が存在する。 $y=\operatorname{ImpRaw}\bigl( \operatorname{AllRaw}(i,\operatorname{ImpRaw}(a,b)), \operatorname{ImpRaw}(a,\operatorname{AllRaw}(i,b))\bigr)$ これは全称分配の公理§E19.10 定義 1.1 (Q2)を表す。
$y=\operatorname{Eq}(t,t)$ を満たす項符号 $t$ が存在する。
$0,S,+,\times$ の合同公理として、次のいずれかである。 $\begin{aligned} y={}&\operatorname{ImpRaw}(\operatorname{Top}_A, \operatorname{Eq}(\operatorname{Zero},\operatorname{Zero})),\\ y={}&\operatorname{ImpRaw}(\operatorname{Eq}(t,u), \operatorname{Eq}(\operatorname{Succ}(t),\operatorname{Succ}(u))),\\ y={}&\operatorname{ImpRaw}\bigl( \operatorname{AndCode}(\operatorname{Eq}(t_1,u_1),\operatorname{Eq}(t_2,u_2)), \operatorname{Eq}(\operatorname{Add}(t_1,t_2),\operatorname{Add}(u_1,u_2))\bigr),\\ y={}&\operatorname{ImpRaw}\bigl( \operatorname{AndCode}(\operatorname{Eq}(t_1,u_1),\operatorname{Eq}(t_2,u_2)), \operatorname{Eq}(\operatorname{Mul}(t_1,t_2),\operatorname{Mul}(u_1,u_2))\bigr). \end{aligned}$
等号を二項関係として扱う合同公理 $y=\operatorname{ImpRaw}\bigl( \operatorname{AndCode}(\operatorname{Eq}(t_1,u_1),\operatorname{Eq}(t_2,u_2)), \operatorname{IffCode}(\operatorname{Eq}(t_1,t_2),\operatorname{Eq}(u_1,u_2))\bigr)$ である。

(2)では Term $(t)$ 、(4)から(6)では表示したすべての項符号に Term を要求する。各場合で最外タグ、有限列の長さ、各成分、および必要な同一性を照合するので、ここに表示していない公理スキーマは LogAx に含めない。

命題 4.3. LogAx は原始再帰関係である。

証明.§E19.10 定義 1.1 (H1)–§E19.10 定義 1.1 (H3)は三つ、全称分配の公理§E19.10 定義 1.1 (Q2)は一つの構文木パターンであり、構成子タグ、固定された有限列の長さ、および繰り返し現れる成分符号の等号を有限回検査すればよい。全称分配の公理§E19.10 定義 1.1 (Q2)の変数条件は、原始再帰関係 Free の否定である。

全称具体化の公理§E19.10 定義 1.1 (Q1)では $i,a,b$ を $y$ の成分から取得し、候補項 $t\le y$ を有界探索する。 $v_i$ が $a$ に自由に現れる場合、置換結果 $b$ に $t$ が部分項として現れるので $t<y$ である。 $v_i$ が自由に現れない場合は置換結果が $a$ と一致する。この場合、 $a$ の原子部分式に現れる任意の項を候補に取ることができ、その項符号は $a$ の真部分符号なので $y$ より小さい。したがって有界探索はすべての場合を含む。各候補について Term $(t)$ 、FreeFor $(t,i,a)$ 、および $b=\operatorname{SubTermCode}(a,i,t)$ を検査する。FreeFor は、最大二個の真部分式へ進む直前の有限分岐コース再帰で構成されており、Formula、Free、および有限の場合分けだけを親節で用いるため原始再帰的である。

$L_A$ の非論理記号は $0,S,+,\times$ の四個で、項数はそれぞれ $0,1,2,2$ に固定されている。反射律、四つの関数合同、および一つの等号関係合同は、定義に列挙した有限個のパターンだけである。AndCode、IffCode、Top $_A$ は固定構成子の合成であり、零項の場合にも追加の探索を要しない。各項位置の Term と構文上の等号を検査すればよい。

原始再帰関係は有限選言、有限連言、否定、および有界存在量化について閉じている。以上の全場合を有限選言で結ぶと LogAx が原始再帰的になる。▨

上の証明で与えた構成を、 $\operatorname{LogAx}$ の原始再帰的定義列として次の一つに固定する。後続の記事では、原始再帰性だけでなく、この定義列が満たす等式を対象理論の内部で用いるからである。

定義 4.4 (論理公理例の判定の原始再帰的定義列).定義 4.2で並べた6節のそれぞれについて、命題 4.3の証明で挙げた検査、すなわち構成子タグと有限列の長さと各成分の照合、繰り返し現れる成分符号の等号、 $\operatorname{Formula}$ 、 $\operatorname{Term}$ 、 $\operatorname{Free}$ 、 $\operatorname{FreeFor}$ 、 $\operatorname{SubTermCode}$ の値による条件、および $y$ で押さえた有界探索の合成として、その節への一致を表す関係の特性関数を定める。 $\operatorname{Formula}$ は、同定義で冒頭に表示される小文字の式符号へ課す検査であり、定義 4.2 (1)から定義 4.2 (3)の $a,b,c$ がこれにあたる。定義列は、これら6個の特性関数の定義列を節の番号の順に並べ、最終段でそれらの有限選言を取るものとする。この定義列を論理公理例判定の原始再帰的定義列 (primitive-recursive definition sequence for logical-axiom instances) という。

定義列の最終段では、6節のいずれかへの一致から $\operatorname{LogAx}(y)$ を導く合成の等式を定める。個別に与えた符号について $\operatorname{LogAx}$ の成立を対象理論の内部で示すときは、当該の節の条件を確かめたうえで、この最終段の等式を用いる。

5 導出と証明列

証明の一行を

\operatorname{Line}(k,y,p,q,i)=\operatorname{SeqCode}(k,y,p,q,i)

と符号化する。 $k$ は規則タグ、 $y$ はその行の論理式、 $p,q$ は先行行の添字、 $i$ は一般化する変数の添字である。規則タグを $1=$ LogAx、 $2=$ 理論公理、 $3=$ modus ponens、 $4=$ 一般化と固定する。未使用欄には $0$ を入れる。Line の各成分取得は原始再帰的である。

定義 5.1. $A(y)$ を原始再帰的な述語とし、 $A(y)\to\operatorname{Sentence}(y)$ をすべての $y$ について仮定する。有限列 $P$ の第 $r$ 成分 $\ell_r$ が長さ $5$ の Line 符号であることを要求し、その五成分を

\ell_r=\operatorname{Line}(k_r,y_r,p_r,q_r,i_r)

とする。一般化行の変数条件を表す有界述語を

\operatorname{GenOK}_A(P,r,i)\quad\Longleftrightarrow\quad \forall s<r\,(k_s=2\to\neg\operatorname{Free}(y_s,i))

と定める。 $\operatorname{ProofSeq}_A(P)$ (proof-sequence predicate) は、各 $r<\operatorname{Len}(P)$ について Formula $(y_r)$ かつ、行 $\ell_r$ が次のいずれかのタグ付きパターンへ一致することを表す。

$k_r=1$ 、LogAx $(y_r)$ 、 $p_r=q_r=i_r=0$ である。
$k_r=2$ 、 $A(y_r)$ 、 $p_r=q_r=i_r=0$ である。
$k_r=3$ 、 $p_r,q_r<r$ 、 $i_r=0$ であり、次の二つの等式をともに満たす論理式符号 $a$ が存在する。 $y_{p_r}=\operatorname{ImpRaw}(a,y_r), \qquad y_{q_r}=a$
$k_r=4$ 、 $p_r<r$ 、 $q_r=0$ 、 $y_r=\operatorname{AllRaw}(i_r,y_{p_r})$ 、および GenOK $_A(P,r,i_r)$ が成り立つ。

末尾関数を

\operatorname{End}(P)= \begin{cases} y_{\operatorname{Len}(P)-1}&\operatorname{Len}(P)>0,\\ 0&\operatorname{Len}(P)=0 \end{cases}

とする。 $\operatorname{Deriv}_A(P,y)$ (derivation predicate) は $\operatorname{ProofSeq}_A(P)\land\operatorname{End}(P)=y$ と定める。

LogAx の行は論理公理であり、一般化規則の前提依存条件へ入らない。タグ $2$ の行だけが理論 $A$ に由来するが、 $A(y)\to\operatorname{Sentence}(y)$ なので、任意の $i$ について $\neg\operatorname{Free}(y,i)$ である。したがって GenOK $_A$ は本記事の対象では常に成り立つ。この有界条件を第4のタグパターンに明示したことにより、一般化条件を省略したのではなく、文公理だけからなる理論証明へ特殊化したことをコード上でも確認することができる。

本記事の ProofSeq $_A$ は、文公理をもつ理論における定理証明だけを扱う。自由変数を含む任意の仮定からの導出には、各行の依存前提集合を符号化する別の API が必要である。本記事では、その拡張を定義しない。

定理 5.2. Term、Formula、Sentence、Free、FreeFor、Sub、Neg、Imp、LogAx、GenOK $_A$ 、および End は原始再帰的である。さらに $A$ が原始再帰的な文符号の述語なら ProofSeq $_A$ と Deriv $_A$ も原始再帰的である。不正な自然数に対して、構文述語は偽、構文を返す関数と End は $0$ を返す。

証明. Term、Formula、Sentence、Free は定理 2.2、FreeFor はその直前のコース再帰、 Sub は定理 3.4、Neg と Imp は構成子と場合分け、LogAx は命題 4.3により原始再帰的である。

End は Len、切捨て減法、Entry、行の固定成分取得、および零判定の合成である。 GenOK $_A$ は、 $s<r$ の有界全称量化、規則タグの等号、および Free の否定からなるので原始再帰的である。 ProofSeq $_A$ の各行条件は $k_r\in\{1,2,3,4\}$ の有限場合分けである。タグ $1$ と $2$ では LogAx または $A$ と未使用欄の零を検査する。タグ $3$ では $p_r,q_r<r$ と先行行の式符号を取得し、ImpRaw の固定タグ、長さ、左右成分を照合する。タグ $4$ では $p_r<r$ 、AllRaw の固定タグと成分、および GenOK $_A$ を照合する。各検査は原始再帰的であり、 $r<\operatorname{Len}(P)$ の有界全称量化も原始再帰性を保つ。 Deriv $_A$ は ProofSeq $_A$ と End の等式の連言である。

この証明は「構文を符号化することができる」という存在主張だけに依存していない。各述語のタグ照合、各再帰で参照する真部分符号の減少、代入時の環境更新、各証明行の先行添字検査を具体的に構成した。▨

注意 5.3 (帰納的可算な公理集合との境界). 任意の帰納的可算理論 $T$ について、所属述語 $y\in\operatorname{Ax}(T)$ 自体が原始再帰的であるとは限らない。その場合は、公理列挙プログラムの有限計算証人を証明行へ添え、証人を含む行の検査を原始再帰的にする必要がある。本記事の LogAx と証明列 API は、その後続構成の構文部分だけを供給する。

例 5.4. 空列の符号 $0$ は項でも論理式でもないので Term $(0)$ と Formula $(0)$ は偽である。したがって Neg $(0)=0$ 、Sub $(0,v,n)=0$ である。一方、有限列そのものには bad code がなく、 $0$ は正しい空列である。「列として復号可能であること」と「算術構文として整形式であること」は異なる判定である。

6 演習

問題 6.1.

項符号の最小値と論理式符号の最小値を求めよ。
$z=\operatorname{Eq}(\operatorname{Var}(0),\operatorname{Var}(1))$ 、 $y=\operatorname{AllRaw}(1,z)$ 、 $t=\operatorname{Var}(1)$ とする。 $\operatorname{WalkFormula}(y,0,t,0)$ と $\operatorname{WalkFormula}(y,1,t,0)$ を、 $y$ を用いた式で求めよ。ここで $\operatorname{Var}(1)=9$ である。
$\operatorname{Sentence}(y)$ ならば、すべての $v,n$ について $\operatorname{Sub}(y,v,n)=y$ であることを証明せよ。
$e$ を一変数の原始再帰関数とし、すべての $n$ について $\operatorname{Sentence}(e(n))$ が成り立つとする。 $\operatorname{And}(x,w)=\operatorname{Neg}(\operatorname{Imp}(x,\operatorname{Neg}(w)))$ とおき、 $C(a,0)=a$ 、 $C(a,n+1)=\operatorname{And}(C(a,n),a)$ と定める。述語 $A'(y)$ を「ある $n$ について $y=C(e(n),n)$ 」と定めると、 $A'$ が原始再帰的であることを示せ。さらに、符号 $e(n)$ が表す文の全体を公理とする理論と、 $A'$ を満たす符号が表す文の全体を公理とする理論について、同じ文が導出されることを示せ。

解答 (確認問題の解答).

$\operatorname{pair}(a,b)=T_{a+b}+b$ は各引数について狭義単調増加であるから、 $\operatorname{Cons}$ と $\operatorname{SeqCode}$ も各成分について狭義単調増加である。 $\operatorname{Zero}=\operatorname{Cons}(2,0)=1+\operatorname{pair}(2,0)=4$ であり、 $\operatorname{Var}(i)\geq\operatorname{Var}(0)=\operatorname{Cons}(1,\operatorname{Cons}(0,0))=\operatorname{Cons}(1,1)=1+\operatorname{pair}(1,1)=5$ である。Succ、Add、Mul の値は補題 1.2 (1)により直下の項符号より大きい。したがって、項符号の構成に関する帰納法により、すべての項符号は $4$ 以上であり、 $4=\operatorname{Zero}$ は項符号であるから、項符号の最小値は $4$ である。

論理式符号は Eq $(t,u)$ から始めて NegRaw、ImpRaw、AllRaw で作られ、これらの値は直下の論理式符号より大きい。Eq $(t,u)=\operatorname{SeqCode}(6,t,u)$ は $t,u\geq4$ について単調であるから、Eq $(t,u)\geq\operatorname{Eq}(4,4)$ である。 $\operatorname{Cons}(4,0)=1+\operatorname{pair}(4,0)=11$ 、 $\operatorname{Cons}(4,11)=1+\operatorname{pair}(4,11)=1+120+11=132$ 、 $\operatorname{Cons}(6,132)=1+\operatorname{pair}(6,132)=1+9591+132=9724$ である。よって論理式符号の最小値は $\operatorname{Eq}(\operatorname{Zero},\operatorname{Zero})=9724$ である。
まず $v=0$ の場合を計算する。量化子の節で、 $\operatorname{Look}(0,0)=0$ 、 $i=1\neq0$ 、 $v_1$ は $t$ に自由に現れ、 $v_0$ は $z$ に自由に現れるので、改名の三条件がすべて成り立つ。よって $j=1+y+t+0+0+1=y+11$ であり、 $E'=\operatorname{Cons}(\operatorname{pair}(1,y+11),0)$ のもとで $z$ を処理する。Eq の二つの子のうち、 $\operatorname{Var}(0)$ では $E'$ の唯一の成分の第1成分が $1\neq0$ であるから $\operatorname{Look}(E',0)=\operatorname{Look}(0,0)=0$ であり、 $0=v$ なので $t=\operatorname{Var}(1)$ を返す。 $\operatorname{Var}(1)$ では $\operatorname{Look}(E',1)=S(y+11)$ であるから $\operatorname{Var}(y+11)$ を返す。したがって
$\operatorname{WalkFormula}(y,0,t,0)=\operatorname{AllRaw}\bigl(y+11,\operatorname{Eq}(\operatorname{Var}(1),\operatorname{Var}(y+11))\bigr)$
であり、これは $\forall v_{y+11}\,(v_1=v_{y+11})$ の符号である。改名しなければ結果は $\forall v_1\,(v_1=v_1)$ となり、代入した $v_1$ が捕獲される。

次に $v=1$ の場合、 $i=v$ であるから改名せず $j=1$ とし、 $E''=\operatorname{Cons}(\operatorname{pair}(1,1),0)$ のもとで $z$ を処理する。 $\operatorname{Var}(0)$ では $\operatorname{Look}(E'',0)=0$ かつ $0\neq v$ であるから $\operatorname{Var}(0)$ を返す。 $\operatorname{Var}(1)$ では $\operatorname{Look}(E'',1)=S1$ であるから $\operatorname{Var}(1)$ を返す。よって $\operatorname{WalkFormula}(y,1,t,0)=\operatorname{AllRaw}(1,z)=y$ である。
すべての成分が $\operatorname{pair}(k,k)$ の形の環境を恒等環境と呼ぶ。 $0$ は恒等環境である。項符号または論理式符号 $y$ について、次の主張を構文の構成に関する帰納法で示す。「恒等環境 $E$ が、 $\operatorname{Look}(E,v)=0$ ならば $\neg\operatorname{Free}(y,v)$ を満たすとき、WalkTerm $(y,v,t,E)$ または WalkFormula $(y,v,t,E)$ は $y$ に等しい。」

$y=\operatorname{Var}(i)$ とする。 $\operatorname{Look}(E,i)\neq0$ ならば、最初に一致する成分は $\operatorname{pair}(i,i)$ であるから $\operatorname{Var}(i)$ を返す。 $\operatorname{Look}(E,i)=0$ のとき、 $i=v$ ならば $\operatorname{Look}(E,v)=0$ であるのに $v_v$ が $\operatorname{Var}(v)$ に自由に現れ、仮定に反する。よって $i\neq v$ であり、 $\operatorname{Var}(i)$ を返す。Zero は Zero を返す。Succ、Add、Mul、Eq、NegRaw、ImpRaw では、直下の対象 $u$ について $\operatorname{Free}(u,v)$ ならば $\operatorname{Free}(y,v)$ であるから、仮定が $u$ と同じ $E$ へ継承され、帰納法の仮定により各子は変わらず、 $y$ が再構成される。

$y=\operatorname{AllRaw}(i,z)$ とする。改名の三条件が成り立つと仮定すると、 $\operatorname{Look}(E,v)=0$ により $\neg\operatorname{Free}(y,v)$ であり、 $i\neq v$ と合わせて $\neg\operatorname{Free}(z,v)$ となり、第三条件に反する。よって $j=i$ であり、 $E'=\operatorname{Cons}(\operatorname{pair}(i,i),E)$ は恒等環境である。 $\operatorname{Look}(E',v)=0$ ならば $i\neq v$ かつ $\operatorname{Look}(E,v)=0$ であるから、 $\neg\operatorname{Free}(y,v)$ と $i\neq v$ により $\neg\operatorname{Free}(z,v)$ である。帰納法の仮定により $z$ の処理は $z$ を返し、結果は $\operatorname{AllRaw}(i,z)=y$ である。

$\operatorname{Sentence}(y)$ とする。 $i\leq y$ ならば定義により $\neg\operatorname{Free}(y,i)$ であり、 $i>y$ ならば補題 1.2 (2)により $\neg\operatorname{Free}(y,i)$ である。よってすべての $v$ について $\neg\operatorname{Free}(y,v)$ であり、 $E=0$ について主張の仮定が成り立つ。 $\operatorname{Formula}(y)$ と $\operatorname{Term}(\operatorname{Num}(n))$ から $\operatorname{Sub}(y,v,n)=\operatorname{WalkFormula}(y,v,\operatorname{Num}(n),0)=y$ である。
文符号 $a$ について、 $\operatorname{Neg}$ と $\operatorname{Imp}$ は論理式符号に構成子を適用するだけであるから、 $n$ についての帰納法により $C(a,n)$ は文符号である。補題 1.2 (1)により $\operatorname{And}(x,a)=\operatorname{NegRaw}(\operatorname{ImpRaw}(x,\operatorname{NegRaw}(a)))>x$ であるから $C(a,n+1)>C(a,n)$ であり、 $C(a,n)\geq a+n\geq n$ である。 $C$ は第二引数についての原始再帰であり原始再帰的である。 $y=C(e(n),n)$ ならば $n\leq y$ であるから
$A'(y)\iff\exists n\leq y\,\bigl(y=C(e(n),n)\bigr)$
であり、原始再帰関数の合成と有界存在量化により $A'$ は原始再帰的である。

$\sigma_n$ を $e(n)$ が表す文とし、 $\sigma_n^{(k)}$ を $C(e(n),k)$ が表す文とする。 $\sigma_n^{(0)}=\sigma_n$ 、 $\sigma_n^{(k+1)}=\sigma_n^{(k)}\land\sigma_n$ である。§E19.10 補題 2.1 (2)の連言の除去と導入により、 $k$ についての帰納法で $\{\sigma_n^{(k)}\}\vdash\sigma_n$ かつ $\{\sigma_n\}\vdash\sigma_n^{(k)}$ である。 $T=\{\sigma_n\mid n\in\N\}$ 、 $T'=\{\sigma_n^{(n)}\mid n\in\N\}$ とおくと、 $T$ の各公理は $T'$ から、 $T'$ の各公理は $T$ から導出される。前提がすべて文であるから、一方の導出の前提の行を他方からの導出で置き換えても一般化の条件は保たれ、 $T\vdash\varphi$ と $T'\vdash\varphi$ は同値である。したがって、公理集合が原始再帰関数の値域として与えられる理論は、同じ定理をもち原始再帰的な所属判定をもつ公理集合で置き換えることができる。

▨

§E19.18構文操作の原始再帰性