算術化の PA 内での形式化 | 数理論理

1 1. PA の内部で用いる初等的な数論

以下、 $L_A=\{0,S,+,\times\}$ とし、順序は§E16.15 定義 1.1の略記

x<y:\!\!\Longleftrightarrow\exists z\,(y=x+Sz), \qquad x\le y:\!\!\Longleftrightarrow\exists z\,(y=x+z)

に従う。 $PA$ は§E16.15 定義 3.1の理論であり、帰納法公理スキーマはすべての $L_A$ 論理式について成り立つ。以下の帰納法は、いずれもこの図式の一つの例であって、論理式の複雑さによる制限を受けない。

補題 1.1. $PA$ は次を証明する。

加法と乗法の結合律と交換律、および分配律 $x\times(y+z)=x\times y+x\times z$ 。
加法の消約律 $x+z=y+z\to x=y$ 、および $z\ne0$ のときの乗法の消約律 $x\times z=y\times z\to x=y$ 。
$x\le y\lor y\le x$ 、 $\le$ の反射律・推移律・反対称律、および $x<y\leftrightarrow Sx\le y$ 。
$x\ne0\to\exists u\,(x=Su)$ 、 $y\le0\to y=0$ 、 $y\le Sx\to(y\le x\lor y=Sx)$ 、 $y<Sx\to y\le x$ 。
加法と乗法の単調性 $x\le y\to x+z\le y+z$ および $x\le y\to x\times z\le y\times z$ 。
乗法の単調性の逆 $0<z\land x\times z\le y\times z\to x\le y$ 。

証明.(1)を示す。 $0+x=x$ は $x$ に関する帰納法による。 $x=0$ では (Q4)、 $x$ から $Sx$ へは (Q5) により $0+Sx=S(0+x)=Sx$ である。 $Sx+y=S(x+y)$ も $y$ に関する帰納法で得る。この二つから、 $y$ に関する帰納法で $x+y=y+x$ を得る。結合律 $(x+y)+z=x+(y+z)$ は $z$ に関する帰納法により、(Q4) と (Q5) だけから従う。

分配律 $x\times(y+z)=x\times y+x\times z$ は $z$ に関する帰納法による。 $z=0$ では (Q4) と (Q6)、 $z$ から $Sz$ へは (Q5) と (Q7) および加法の結合律・交換律を用いる。 $0\times x=0$ は $x$ に関する帰納法で、 $Sx\times y=x\times y+y$ は $y$ に関する帰納法で示し、これらから $y$ に関する帰納法で $x\times y=y\times x$ を得る。乗法の結合律は $z$ に関する帰納法と分配律による。

(2)の加法の消約律は $z$ に関する帰納法による。 $z=0$ では (Q4)、 $z$ から $Sz$ へは (Q5) と (Q2) を用いる。乗法の消約律は(3)の後に示す。

(3)を示す。 $\forall y\,(x\le y\lor y\le x)$ を $x$ に関する帰納法で示す。 $x=0$ では $y=0+y$ より $0\le y$ である。 $x$ から $Sx$ へ進む段で $y$ を取る。 $y\le x$ ならば $x=y+d$ と書くことができ、 $Sx=y+Sd$ より $y\le Sx$ である。 $x\le y$ ならば $y=x+d$ と書くことができる。 $d=0$ なら $y=x\le Sx$ である。 $d=Su$ なら $y=x+Su=Sx+u$ より $Sx\le y$ である。反射律と推移律は加法の結合律から従う。反対称律は、 $y=x+d$ と $x=y+e$ から $x=x+(d+e)$ を得て、消約律により $d+e=0$ 、(Q1) と (Q5) により $d=e=0$ となることによる。 $x<y\leftrightarrow Sx\le y$ は $x+Sz=Sx+z$ から従う。

(4)の第1式は (Q3) である。 $y\le0$ は $0=y+d$ を与え、 $y=Su$ なら $y+d=S(u+d)$ が (Q1) に反するので $y=0$ である。 $y\le Sx$ は $Sx=y+d$ を与え、 $d=0$ なら $y=Sx$ 、 $d=Se$ なら $Sx=S(y+e)$ と (Q2) から $x=y+e$ 、すなわち $y\le x$ である。 $y<Sx$ は $Sx=y+Sz=S(y+z)$ を与え、(Q2) から $x=y+z$ 、すなわち $y\le x$ である。

(5)の加法の単調性は結合律から直ちに従う。乗法の単調性は分配律から従う。

(2)の乗法の消約律を示す。 $z\ne0$ とし $x\times z=y\times z$ とする。(3)により $x\le y$ としてよい。 $x\ne y$ ならば $y=x+Sd$ と書くことができ、分配律により $y\times z=x\times z+Sd\times z$ である。消約律により $Sd\times z=0$ である。一方 $Sd\times z=d\times z+z$ であり、 $z\ne0$ から $Sd\times z\ne0$ である。これは矛盾なので $x=y$ である。

(6)を示す。 $0<z$ とし $x\times z\le y\times z$ とする。(3)により $x\le y$ または $y\le x$ である。前者ならば示すことがない。後者で $x\ne y$ とすると、 $x=y+Sd$ を満たす $d$ が存在し、分配律により $x\times z=y\times z+Sd\times z$ である。一方 $x\times z\le y\times z$ から $y\times z=x\times z+w$ を満たす $w$ が存在するので、 $y\times z=y\times z+Sd\times z+w$ となり、加法の消約律により $Sd\times z+w=0$ であり、 $Sd\times z\le0$ と(4)により $Sd\times z=0$ である。 $Sd\times z=d\times z+z$ と $0<z$ からこれは矛盾である。よって $x=y$ であり、いずれにせよ $x\le y$ である。▨

補題 1.2. $\varphi(x,\vec z)$ を任意の $L_A$ 論理式とする。 $PA$ は

\exists x\,\varphi(x,\vec z) \to \exists x\,\bigl(\varphi(x,\vec z)\land\forall y<x\,\neg\varphi(y,\vec z)\bigr)

を証明する。

証明. 対偶を示す。 $\forall x\,\bigl(\varphi(x,\vec z)\to\exists y<x\,\varphi(y,\vec z)\bigr)$ を仮定する。論理式 $\psi(x):\!\!\Longleftrightarrow\forall y\le x\,\neg\varphi(y,\vec z)$ に $PA$ の帰納法を適用する。

$x=0$ の場合、補題 1.1 (4)により $y\le0$ は $y=0$ を与えるので、 $\neg\varphi(0,\vec z)$ を示せばよい。 $\varphi(0,\vec z)$ を仮定すると、仮定から $y<0$ を満たす $y$ が存在することになる。しかし $0=y+Sd=S(y+d)$ は (Q1) に反する。よって $\neg\varphi(0,\vec z)$ である。

$x$ から $Sx$ へ進む段では、 $\psi(x)$ を仮定する。 $\varphi(Sx,\vec z)$ とすると、 $y<Sx$ かつ $\varphi(y,\vec z)$ を満たす $y$ が存在する。補題 1.1 (4)により $y\le x$ であり、 $\psi(x)$ に反する。よって $\neg\varphi(Sx,\vec z)$ であり、補題 1.1 (4)の $y\le Sx\to(y\le x\lor y=Sx)$ と合わせて $\psi(Sx)$ を得る。

従って $\forall x\,\psi(x)$ であり、とくに $\forall x\,\neg\varphi(x,\vec z)$ である。▨

補題 1.3. $PA$ は次を証明する。 $0<b$ とすると、

a=q\times b+r,\qquad r<b

を満たす $q,r$ がちょうど一組存在する。

証明. 存在を $a$ に関する帰納法で示す。 $a=0$ では $q=r=0$ とすればよい。 $a$ から $Sa$ へ進む段では、 $a=q\times b+r$ 、 $r<b$ とする。 $Sa=q\times b+Sr$ である。 $Sr<b$ ならばこの組でよい。そうでなければ補題 1.1 (3)と補題 1.1 (4)により $Sr=b$ であるから、 $Sa=q\times b+b=Sq\times b+0$ となり、 $0<b$ よりこの組でよい。

一意性を示す。 $q\times b+r=q'\times b+r'$ 、 $r<b$ 、 $r'<b$ とする。補題 1.1 (3)により $q\le q'$ としてよく、 $q'=q+e$ と書く。分配律により $q\times b+r=q\times b+e\times b+r'$ であり、加法の消約律により $r=e\times b+r'$ である。 $e\ne0$ ならば $e\times b\ge b$ であるから $r\ge b$ となり、 $r<b$ に反する。よって $e=0$ 、すなわち $q=q'$ であり、消約律から $r=r'$ である。▨

定義 1.4 (PA 内の整除式と合同式). $L_A$ 論理式の略記を

d\mid a \quad:\!\!\Longleftrightarrow\quad \exists q\,(a=q\times d), \qquad a\equiv b\ (\mathrm{mod}\ m) \quad:\!\!\Longleftrightarrow\quad \exists s\,\exists t\,(a+m\times s=b+m\times t)

と定める。左の略記を PA 内の整除式 (divisibility formula in PA)、右の略記を PA 内の合同式 (congruence formula in PA) という。合同の定義に自然数の引き算を用いていないので、右辺はそのまま $L_A$ 論理式である。

補題 1.5. $PA$ は次を証明する。

$\equiv\ (\mathrm{mod}\ m)$ は反射的、対称的、推移的であり、 $a\equiv b$ かつ $c\equiv d$ ならば $a+c\equiv b+d$ かつ $a\times c\equiv b\times d$ である。
$0<d$ 、 $d\mid a$ 、 $a+r=a'$ 、 $d\mid a'$ ならば $d\mid r$ である。
$m\mid M$ かつ $a\equiv b\ (\mathrm{mod}\ M)$ ならば $a\equiv b\ (\mathrm{mod}\ m)$ である。
$0<m$ とする。 $a\equiv b\ (\mathrm{mod}\ m)$ であることと、 $a$ と $b$ を $m$ で割った余りが等しいこととは同値である。とくに $b<m$ ならば、 $a\equiv b\ (\mathrm{mod}\ m)$ は $a$ を $m$ で割った余りが $b$ であることと同値である。

証明.(1)の反射律と対称律は定義から直ちに従う。推移律は、 $a+ms=b+mt$ と $b+ms'=c+mt'$ から $a+m(s+s')=c+m(t+t')$ を得ることによる。加法との両立は二つの等式を辺ごとに加えることによる。乗法との両立は、まず $a+ms=b+mt$ の両辺に $c$ を掛けて $ac+m(sc)=bc+m(tc)$ を得て $ac\equiv bc$ とし、同様に $bc\equiv bd$ を得て推移律を用いることによる。

(2)を示す。 $a=qd$ 、 $a'=q'd$ とすると $qd+r=q'd$ であり、とくに $q\times d\le q'\times d$ である。 $0<d$ であるから補題 1.1 (6)により $q\le q'$ であり、 $q'=q+w$ と書くことができる。分配律と加法の消約律により $r=wd$ 、すなわち $d\mid r$ である。

(3)は、 $M=m\times k$ と $a+Ms=b+Mt$ から $a+m(ks)=b+m(kt)$ を得ることによる。

(4)を示す。補題 1.3により $a=q\times m+\rho$ 、 $b=q'\times m+\rho'$ 、 $\rho,\rho'<m$ と書くことができる。 $\rho=\rho'$ ならば $a+m q'=b+m q$ となり $a\equiv b$ である。逆に $a+ms=b+mt$ とすると、 $\rho+m(q+s)=\rho'+m(q'+t)$ である。補題 1.1 (3)により $q+s\le q'+t$ としてよく、 $q'+t=(q+s)+e$ と書くと、消約律により $\rho=\rho'+m\times e$ を得る。 $e\ne0$ ならば $\rho\ge m$ となり $\rho<m$ に反するので $e=0$ 、すなわち $\rho=\rho'$ である。最後の主張は、 $b<m$ のとき $b$ を $m$ で割った余りが $b$ 自身であることによる。▨

2 2. Bézout の等式と中国剰余定理

有限族の表符号は、二つずつ互いに素な法に対する合同式の同時可解性から得る。§E16.19 補題 4.2は同じ事実をメタ理論で証明しているが、そこでは整数と可変長の積を用いており、 $PA$ の内部の主張ではない。ここでは自然数だけを用いて $PA$ 内の版を証明する。

$0<a$ かつ $0<b$ のとき、 $a$ と $b$ が互いに素であるとは、 $e\mid a$ かつ $e\mid b$ を満たす任意の $e$ について $e=1$ であることをいう。

補題 2.1 (PA における Bézout の等式). $PA$ は次を証明する。 $0<a$ かつ $0<b$ とし、 $L_A$ 論理式

\sigma_{a,b}(z):\!\!\Longleftrightarrow 0<z\land\exists u\,\exists v\,(z+b\times v=a\times u)

を満たす最小の $z$ を $d$ とする。このとき $d$ は存在し、 $d\mid a$ かつ $d\mid b$ である。さらに、 $e\mid a$ かつ $e\mid b$ を満たす任意の $e$ について $e\mid d$ である。

証明. $u=1$ 、 $v=0$ と取ると $a+b\times0=a\times1$ であるから、 $0<a$ と合わせて $\sigma_{a,b}(a)$ が成り立つ。補題 1.2を $\sigma_{a,b}$ へ適用して、 $\sigma_{a,b}$ を満たす最小の $d$ を取る。 $d+b v_0=a u_0$ を満たす $u_0,v_0$ を固定する。

$d\mid b$ を示す。補題 1.3により $b=q\times d+r$ 、 $r<d$ と書く。 $r=0$ でないと仮定する。 $A:=q u_0$ 、 $B:=1+q v_0$ 、 $s:=A+B$ と置く。 $0<b$ より $b s\ge s\ge A$ であるから、 $U+A=b s$ を満たす $U$ が存在する。 $0<a$ より $a s\ge s\ge B$ であるから、 $V+B=a s$ を満たす $V$ が存在する。

$U+A=bs$ の両辺に $a$ を掛けて $aU+aA=abs$ 、 $V+B=as$ の両辺に $b$ を掛けて $bV+bB=abs$ を得る。従って

aU+a q u_0=bV+b+b q v_0

である。 $d+bv_0=au_0$ の両辺に $q$ を掛けると $qd+q b v_0=q a u_0$ であり、左辺の $aqu_0$ をこれで置き換えると

aU+qd+q b v_0=bV+b+b q v_0

となる。加法の消約律により $aU+qd=bV+b$ である。 $b=qd+r$ を代入して再び消約すると $aU=bV+r$ 、すなわち $r+bV=aU$ を得る。 $0<r$ であるから $\sigma_{a,b}(r)$ が成り立ち、 $r<d$ は $d$ の最小性に反する。よって $r=0$ 、すなわち $d\mid b$ である。

$d\mid a$ を示す。補題 1.3により $a=q\times d+r$ 、 $r<d$ と書き、 $r=0$ でないと仮定する。 $0<b$ より $b\times q u_0\ge q u_0$ であるから、 $U+q u_0=1+b\times q u_0$ を満たす $U$ が存在する。また $d+bv_0=au_0$ から $b v_0\le a u_0$ であり、 $0<b$ より $v_0\le b v_0\le a u_0$ であるから $q v_0\le a\times q u_0$ であり、 $V+q v_0=a\times q u_0$ を満たす $V$ が存在する。

$U+qu_0=1+b q u_0$ の両辺に $a$ を掛けて $aU+a q u_0=a+ab q u_0$ 、 $V+qv_0=a q u_0$ の両辺に $b$ を掛けて $bV+b q v_0=ab q u_0$ を得る。従って

aU+a q u_0=a+bV+b q v_0

である。上と同じく $aqu_0=qd+qbv_0$ を代入し、消約すると $aU+qd=a+bV$ となる。 $a=qd+r$ を代入して消約すると $aU=r+bV$ を得る。 $0<r$ であるから $\sigma_{a,b}(r)$ が成り立ち、 $r<d$ は最小性に反する。よって $r=0$ 、すなわち $d\mid a$ である。

共通の約数が $d$ を割ることを示す。 $a=e a'$ 、 $b=e b'$ とする。 $0<a$ より $e\ne0$ である。 $d+e b' v_0=e a' u_0$ から $e b' v_0\le e a' u_0$ であり、 $0<e$ と補題 1.1 (6)により $b' v_0\le a' u_0$ である。 $b' v_0+w=a' u_0$ と書くと $d+e b' v_0=e b' v_0+e w$ となり、消約により $d=e w$ 、すなわち $e\mid d$ である。▨

系 2.2. $PA$ は次を証明する。 $0<d$ 、 $0<C$ とし、 $d$ と $C$ が互いに素であるとする。このとき $d\mid e\times C$ ならば $d\mid e$ である。

証明.補題 2.1を $a:=d$ 、 $b:=C$ へ適用する。 $\sigma_{d,C}$ を満たす最小の数 $d_0$ は $d$ と $C$ の共通の約数であるから、互いに素という仮定により $d_0=1$ である。従って $1+C v=d u$ を満たす $u,v$ が存在する。両辺に $e$ を掛けて

e+e C v=e d u

を得る。 $e C=d k$ と書くと $e+d k v=d\times e u$ である。とくに $d\times(k v)\le d\times(e u)$ であり、 $0<d$ と補題 1.1 (6)により $k v\le e u$ であるから、 $k v+w=e u$ を満たす $w$ が存在する。これを代入すると $e+d k v=d k v+d w$ となり、消約により $e=d w$ 、すなわち $d\mid e$ である。▨

補題 2.3 (二つの法に対する中国剰余定理). $PA$ は次を証明する。 $0<m$ 、 $0<n$ とし、 $m$ と $n$ が互いに素であるとする。このとき、 $x<m$ と $y<n$ を満たす任意の $x,y$ に対して

c<m\times n, \qquad c\equiv x\ (\mathrm{mod}\ m), \qquad c\equiv y\ (\mathrm{mod}\ n)

を満たす $c$ が存在する。

証明.補題 2.1を $a:=m$ 、 $b:=n$ へ適用する。 $\sigma_{m,n}$ を満たす最小の数 $d_0$ は $m$ と $n$ の共通の約数であるから、互いに素という仮定により $d_0=1$ である。従って

1+n v=m u \tag{1}

を満たす $u,v$ が存在する。 $0<m$ より $m=Sm'$ を満たす $m'$ が存在する。(1) の両辺に $m'$ を掛けると $m'+n v m'=m u m'$ であり、両辺に $1$ を加えると

m+n\times(v m')=m\times(u m')+1 \tag{2}

を得る。ここで $E_m:=n\times(v m')$ 、 $E_n:=m u$ と置く。

(2) は $E_m+m\times1=1+m\times(um')$ を意味するので $E_m\equiv1\ (\mathrm{mod}\ m)$ であり、 $E_m$ は $n$ の倍数なので $E_m\equiv0\ (\mathrm{mod}\ n)$ である。(1) は $E_n=1+n v$ を意味するので $E_n\equiv1\ (\mathrm{mod}\ n)$ であり、 $E_n$ は $m$ の倍数なので $E_n\equiv0\ (\mathrm{mod}\ m)$ である。

$c_0:=x\times E_m+y\times E_n$ と置く。補題 1.5 (1)により

c_0\equiv x\times1+y\times0=x\ (\mathrm{mod}\ m), \qquad c_0\equiv x\times0+y\times1=y\ (\mathrm{mod}\ n)

である。 $0<m\times n$ であるから補題 1.3により $c_0$ を $m\times n$ で割った余り $c$ を取ることができ、 $c<m\times n$ かつ $c\equiv c_0\ (\mathrm{mod}\ m\times n)$ である。 $m\mid m\times n$ と $n\mid m\times n$ に補題 1.5 (3)を適用し、推移律を用いると、 $c\equiv x\ (\mathrm{mod}\ m)$ かつ $c\equiv y\ (\mathrm{mod}\ n)$ を得る。▨

3 3. 表符号の存在

§E16.19 定義 4.1は、可変長の復号履歴を一つの対 $(B,C)$ へ収める式として

M(i,C):=S((Si)\times C), \qquad \operatorname{Tab}^{0}_Q(B,C,i,x) :\!\!\Longleftrightarrow x<M(i,C)\land\exists q\,\bigl(q\le B\land B=(q\times M(i,C))+x\bigr)

と、その一意性節を加えた $\operatorname{Cell}_Q(B,C,i,x)$ を固定している。 $M(i,C)$ は $L_A$ の項である。

補題 3.1. $PA$ は次を証明する。

任意の $B,C,i$ について $\operatorname{Cell}_Q(B,C,i,x)$ を満たす $x$ がちょうど一つ存在する。
$\operatorname{Cell}_Q(B,C,i,x)$ が成り立つことと、 $x<M(i,C)$ かつ $B\equiv x\ (\mathrm{mod}\ M(i,C))$ が成り立つこととは同値である。

証明. $M(i,C)=S((Si)\times C)$ は後続者の値なので (Q1) により $0<M(i,C)$ である。補題 1.3により、 $B=q\times M(i,C)+x$ かつ $x<M(i,C)$ を満たす $q,x$ がちょうど一組存在する。 $0<M(i,C)$ と乗法の単調性により $q\le q\times M(i,C)\le B$ であるから、 $\operatorname{Tab}^{0}_Q(B,C,i,x)$ が成り立つ。逆に $\operatorname{Tab}^{0}_Q(B,C,i,z)$ ならば、 $z$ は同じ除法の余りであるから一意性により $z=x$ である。従って $\operatorname{Cell}_Q(B,C,i,x)$ が成り立ち、他の値では第2連言が破れるので $x$ は一意である。これが(1)である。

(2)は、補題 1.5 (4)により、 $x<M(i,C)$ の下で「 $B\equiv x$ 」と「 $B$ を $M(i,C)$ で割った余りが $x$ である」が同値であることによる。▨

補題 3.2. $\varphi(i,y,\vec z)$ を任意の $L_A$ 論理式とする。 $PA$ は次を証明する。 $k$ と $\vec z$ を固定し、 $i<k$ の各 $i$ に対して $\varphi(i,y,\vec z)$ を満たす $y$ が一意に存在するとする。このとき、

\forall i<k\;\forall y\,\bigl(\varphi(i,y,\vec z)\to\operatorname{Cell}_Q(B,C,i,y)\bigr)

を満たす $B,C$ が存在する。

証明. 以下はすべて $PA$ の内部の議論である。

法を定める $C$ を選ぶ。 $k$ に関する帰納法により、 $0<P$ かつ $1\le t\le k$ を満たすすべての $t$ について $t\mid P$ となる $P$ が存在する。 $k=0$ では $P=1$ とし、 $k$ から $Sk$ へ進む段では前段の $P$ に $Sk$ を掛ける。次に、 $i<k$ の各 $i$ の値を上から抑える $b$ を取る。補題の仮定が値の一意な存在を与えるのは $i<k$ の範囲だけであるから、 $k$ 自身へ帰納法を行うことはできない。そこで、 $k$ を固定したまま $l$ に関する帰納法を行い、 $l\le k$ を満たすすべての $l$ について

\Theta_0(l):\quad \exists b\,\forall i<l\,\forall y\,\bigl(\varphi(i,y,\vec z)\to y\le b\bigr)

を示す。 $l=0$ では $b:=0$ とすればよく、 $i<0$ を満たす $i$ が無いので全称条件は空虚に成り立つ。 $l$ から $Sl$ へ進む段では $Sl\le k$ とする。このとき $l<k$ であるから、補題の仮定を $i:=l$ について用いることができ、 $\varphi(l,y_l,\vec z)$ を満たす $y_l$ が一意に存在する。 $\Theta_0(l)$ の証人 $b_l$ を取り、補題 1.1 (3)により $b_l$ と $y_l$ の大きいほうを $b_{Sl}$ とすれば、 $i<Sl$ のすべての値が $b_{Sl}$ 以下である。 $l=k$ における $\Theta_0(k)$ の証人を $b$ とする。ここで $C:=P\times Sb$ と置く。 $0<P$ より $b<C$ であり、 $1\le t\le k$ を満たすすべての $t$ が $C$ を割る。

法が二つずつ互いに素であることを示す。 $i<j<k$ とし、 $e\mid M(i,C)$ かつ $e\mid M(j,C)$ とする。 $j=i+f$ と書くと $1\le f\le k$ であり、

M(j,C)=S((Sj)\times C)=S((Si)\times C)+f\times C=M(i,C)+f\times C

である。 $e=0$ とすると $M(i,C)=0$ となり (Q1) に反するので $0<e$ である。補題 1.5 (2)により $e\mid f\times C$ である。次に $e$ と $C$ が互いに素であることを示す。 $t\mid e$ かつ $t\mid C$ とする。 $t=0$ とすると $e=0$ となるので $0<t$ である。 $t\mid M(i,C)=S((Si)\times C)$ かつ $t\mid(Si)\times C$ であるから、補題 1.5 (2)により $t\mid1$ 、すなわち $t=1$ である。従って系 2.2により $e\mid f$ である。 $1\le f\le k$ より $f\mid C$ であるから $e\mid C$ である。 $e$ は $e$ と $C$ の共通の約数であるから、互いに素であることにより $e=1$ である。

表符号を作る。 $N:=k$ と置き、 $\Psi(P,l):\!\!\Longleftrightarrow\forall e\,\forall j\,\bigl(l\le j\land j<N\land e\mid P\land e\mid M(j,C)\to e=1\bigr)$ とする。 $l$ に関する帰納法により、 $l\le N$ を満たすすべての $l$ について次の主張 $\Theta(l)$ を示す。

\Theta(l):\quad \exists B\,\exists P\,\Bigl( 0<P\land B<P\land \forall i<l\,\bigl(M(i,C)\mid P\bigr)\land \Psi(P,l)\land \forall i<l\,\forall y\,\bigl(\varphi(i,y,\vec z)\to B\equiv y\ (\mathrm{mod}\ M(i,C))\bigr)\Bigr)

積 $P$ を証人として持ち回るので、法の積を $L_A$ の項として書く必要はない。

$l=0$ では $B:=0$ 、 $P:=1$ とする。 $0<P$ と $B<P$ はいずれも $0<1$ から従い、二つの全称条件は空虚に成り立つ。 $\Psi(1,0)$ は $e\mid1\to e=1$ から従う。

$l$ から $Sl$ へ進む段では $Sl\le N$ とし、 $\Theta(l)$ の証人 $B_l,P_l$ を取る。 $m_l:=M(l,C)$ と置くと $0<m_l$ である。 $\Psi(P_l,l)$ を $j:=l$ について用いると、 $P_l$ と $m_l$ は互いに素である。仮定により $\varphi(l,y_l,\vec z)$ を満たす $y_l$ が一意に存在し、 $m_l=S((Sl)\times C)\ge SC$ であるから $y_l\le b<C<m_l$ である。補題 2.3を法 $P_l$ と $m_l$ 、剰余 $B_l<P_l$ と $y_l<m_l$ へ適用すると、

B_{Sl}<P_l\times m_l, \qquad B_{Sl}\equiv B_l\ (\mathrm{mod}\ P_l), \qquad B_{Sl}\equiv y_l\ (\mathrm{mod}\ m_l)

を満たす $B_{Sl}$ を得る。 $P_{Sl}:=P_l\times m_l$ と置く。 $0<P_{Sl}$ と $B_{Sl}<P_{Sl}$ は明らかである。 $i<Sl$ について $M(i,C)\mid P_{Sl}$ であることは、 $i<l$ では $M(i,C)\mid P_l\mid P_{Sl}$ から、 $i=l$ では $m_l\mid P_{Sl}$ から従う。

剰余の条件を確かめる。 $i=l$ の場合は上で得た合同式そのものである。 $i<l$ の場合、 $M(i,C)\mid P_l$ と $B_{Sl}\equiv B_l\ (\mathrm{mod}\ P_l)$ に補題 1.5 (3)を適用すると $B_{Sl}\equiv B_l\ (\mathrm{mod}\ M(i,C))$ である。 $\Theta(l)$ が与える $B_l\equiv y_i\ (\mathrm{mod}\ M(i,C))$ と推移律を合わせて $B_{Sl}\equiv y_i\ (\mathrm{mod}\ M(i,C))$ を得る。

$\Psi(P_{Sl},Sl)$ を示す。 $Sl\le j<N$ とし、 $e\mid P_l\times m_l$ かつ $e\mid M(j,C)$ とする。 $e=0$ とすると $M(j,C)=0$ となり (Q1) に反するので $0<e$ である。 $t\mid e$ かつ $t\mid m_l$ とすると $t$ は $M(j,C)$ と $M(l,C)$ の共通の約数であり、 $l<j<N$ であるから、上で示した二つずつの互いに素性により $t=1$ である。従って $e$ と $m_l$ は互いに素であり、系 2.2により $e\mid P_l$ である。 $\Psi(P_l,l)$ を同じ $j$ について用いると $e=1$ を得る。

$l=N=k$ における $\Theta(k)$ の証人を $B,P$ とする。各 $i<k$ について $B\equiv y_i\ (\mathrm{mod}\ M(i,C))$ かつ $y_i<M(i,C)$ であるから、補題 3.1 (2)により $\operatorname{Cell}_Q(B,C,i,y_i)$ である。▨

4 4. 対関数と Cons 符号の PA 内での法則

§E16.17 補題 1.2は対関数の全単射性をメタ理論で証明している。自由変数を残した議論では同じ事実を $PA$ の内部で証明し直さなければならない。ここでは§E16.19 定義 4.1が固定した raw 式

\operatorname{Pair}^{0}_Q(a,b,c) :\!\!\Longleftrightarrow \exists w\,\bigl(w=a+b\land c\le(w\times Sw)+(b+b)\land c+c=(w\times Sw)+(b+b)\bigr)

の定義そのものへ戻って証明する。

補題 4.1. $PA$ は次を証明する。

任意の $a,b$ について $\operatorname{Pair}_Q(a,b,c)$ を満たす $c$ がちょうど一つ存在する。この $c$ を $\operatorname{pair}(a,b)$ と書く。
$a\le\operatorname{pair}(a,b)$ かつ $b\le\operatorname{pair}(a,b)$ である。
$\operatorname{pair}(a,b)=\operatorname{pair}(a',b')$ ならば $a=a'$ かつ $b=b'$ である。
任意の $p$ について $\operatorname{pair}(a,b)=p$ を満たす $a,b$ が存在する。
任意の $a,t$ について $\operatorname{Cons}_Q(a,t,c)$ を満たす $c$ がちょうど一つ存在する。この $c$ を $\operatorname{Cons}(a,t)$ と書き、 $\operatorname{Cons}(a,t)=S\operatorname{pair}(a,t)$ である。とくに $0<\operatorname{Cons}(a,t)$ 、 $a<\operatorname{Cons}(a,t)$ 、 $t<\operatorname{Cons}(a,t)$ である。
$0<s$ ならば $\operatorname{Dec}_Q(s,a,t)$ を満たす対 $(a,t)$ がちょうど一つ存在する。この $a,t$ を $\operatorname{Head}(s)$ 、 $\operatorname{Tail}(s)$ と書き、 $s=0$ のときは $\operatorname{Head}(0)=\operatorname{Tail}(0)=0$ と定める。 $\operatorname{Dec}_Q(0,a,t)$ を満たす $a,t$ は存在しない。
任意の $s$ について $\operatorname{Head}^{0}_Q(s,a)$ を満たす $a$ がちょうど一つ存在し、その値は $\operatorname{Head}(s)$ である。

証明.(1)を示す。 $w$ に関する帰納法により、 $w\times Sw=h+h$ を満たす $h$ が存在する。 $w=0$ では $h=0$ である。 $w$ から $Sw$ へ進む段では、(Q7) と補題 1.1 (1)により

Sw\times S(Sw)=Sw\times Sw+Sw=(w\times Sw+Sw)+Sw=(h+Sw)+(h+Sw)

であるから $h+Sw$ を取ればよい。 $w:=a+b$ に対する $h$ を取り、 $c:=h+b$ と置くと $c+c=(w\times Sw)+(b+b)$ であり、 $c\le c+c$ であるから $\operatorname{Pair}^{0}_Q(a,b,c)$ が成り立つ。逆に $c'+c'=c+c$ ならば、補題 1.1 (3)と加法の単調性により $c'=c$ である。従って raw 式の出力は一意であり、 $\operatorname{Unique}$ を加えた $\operatorname{Pair}_Q$ についても存在と一意性が成り立つ。

(2)を示す。 $2\operatorname{pair}(a,b)=w\times Sw+(b+b)\ge b+b$ より $b\le\operatorname{pair}(a,b)$ である。 $a=0$ ならば $a\le\operatorname{pair}(a,b)$ は明らかである。 $0<a$ ならば $0<w$ であるから $Sw\ge S1$ であり、 $w\times Sw\ge w+w\ge a+a$ である。従って $2\operatorname{pair}(a,b)\ge a+a$ であり $a\le\operatorname{pair}(a,b)$ である。

(3)を示す。 $w:=a+b$ 、 $w':=a'+b'$ とする。 $w<w'$ と仮定すると $Sw\le w'$ であり、乗法の単調性から

w'\times Sw'\ge Sw\times S(Sw)=w\times Sw+(Sw+Sw)

である。一方 $b\le w$ より $b+b<Sw+Sw$ であるから

2\operatorname{pair}(a,b)=w\times Sw+(b+b)<w\times Sw+(Sw+Sw)\le w'\times Sw'\le 2\operatorname{pair}(a',b')

となり、 $\operatorname{pair}(a,b)=\operatorname{pair}(a',b')$ に反する。 $w'<w$ の場合も同様である。従って $w=w'$ であり、消約律から $b=b'$ 、さらに $a+b=a'+b'$ と消約律から $a=a'$ である。

(4)を示す。 $p$ を取る。 $w:=p+p$ は $p+p<(Sw)\times S(Sw)$ を満たすので、この条件を満たす $w$ は存在する。補題 1.2により最小の $w$ を取る。 $w=0$ ならば $w\times Sw=0\le p+p$ である。 $w=Sw_0$ ならば、 $w$ の最小性により $w_0$ は条件を満たさないので $Sw_0\times S(Sw_0)\le p+p$ 、すなわち $w\times Sw\le p+p$ である。いずれにせよ

w\times Sw\le p+p<w\times Sw+(Sw+Sw)

である。 $w\times Sw=h+h$ を満たす $h$ を取ると $h+h\le p+p$ であるから $h\le p$ であり、 $h+b=p$ を満たす $b$ が存在する。このとき $b+b<Sw+Sw$ より $b\le w$ であり、 $a+b=w$ を満たす $a$ が存在する。 $2\operatorname{pair}(a,b)=w\times Sw+(b+b)=(h+h)+(b+b)=p+p$ であるから $\operatorname{pair}(a,b)=p$ である。

(5)は $\operatorname{Cons}^{0}_Q(a,t,c):\!\!\Longleftrightarrow\exists p\,(\operatorname{Pair}^{0}_Q(a,t,p)\land c=Sp)$ と(1)から従う。(Q1) により $0<S\operatorname{pair}(a,t)$ であり、(2)により $a,t\le\operatorname{pair}(a,t)<\operatorname{Cons}(a,t)$ である。

(6)を示す。 $0<s$ とすると $s=Sp$ を満たす $p$ が存在する。(4)により $p=\operatorname{pair}(a,t)$ を満たす $a,t$ が存在し、(5)により $\operatorname{Cons}_Q(a,t,s)$ である。(2)により $a<s$ かつ $t<s$ であるから $\operatorname{Dec}_Q(s,a,t)$ が成り立つ。一意性は(3)と (Q2) による。 $s=0$ の場合は $\operatorname{Cons}_Q(a,t,0)$ が $0=Sp$ を要求し、(Q1) に反する。

(7)は $\operatorname{Head}^{0}_Q$ の定義と(6)による。▨

5 5. 有限列符号の法則を PA 内で証明する

§E16.19 定義 4.1の $\operatorname{At}^{0}_Q(s,i,t)$ は、 $s$ から $\operatorname{Dec}_Q$ を $i$ 回たどった反復尾が $t$ であることを表す。第 $i$ 成分はこれとは別で、 $\operatorname{Entry}^{0}_Q(s,i,a)$ が与える反復尾の先頭である。以下ではこの区別を保つ。

記法：一意に定まる値を項のように書く記法 $R(\vec x,y)$ を $L_A$ 論理式とし、 $PA$ が $\forall\vec x\,\exists!y\,R(\vec x,y)$ を証明するとする。このとき $L_A$ 論理式 $\theta(y)$ に対して

\theta(\mathrm{f}_R(\vec x)) \quad\text{を}\quad \exists y\,\bigl(R(\vec x,y)\land\theta(y)\bigr)

の略記とし、 $\mathrm{f}_R$ に固有の名前を付けて用いる。全域性と一意性により、 $PA$ はこの略記と $\forall y\,(R(\vec x,y)\to\theta(y))$ との同値を証明する。等式 $\mathrm{f}_R(\vec x)=\mathrm{f}_{R'}(\vec x')$ も同じ規約で読む。 $L_A$ に新しい関数記号を追加してはいない。

補題 5.1. $PA$ は次を証明する。

$\operatorname{At}^{0}_Q(s,i,t)$ かつ $\operatorname{At}^{0}_Q(s,i,t')$ ならば $t=t'$ である。
$\operatorname{At}^{0}_Q(s,0,s)$ である。
$\operatorname{At}^{0}_Q(s,i,t)$ ならば $t+i\le s$ である。
$\operatorname{At}^{0}_Q(s,i,t)$ かつ $t\ne0$ ならば $\operatorname{At}^{0}_Q(s,Si,\operatorname{Tail}(t))$ である。
次の三つをすべて満たす $n$ が存在する。第一に $\operatorname{At}^{0}_Q(s,n,0)$ である。第二に、 $i\le n$ を満たすすべての $i$ について $\operatorname{At}^{0}_Q(s,i,t)$ を満たす $t$ が存在する。第三に、 $i<n$ を満たすすべての $i$ と $\operatorname{At}^{0}_Q(s,i,t)$ を満たすすべての $t$ について $t\ne0$ である。
$\operatorname{At}^{0}_Q(s,Si,t')$ ならば、 $\operatorname{At}^{0}_Q(s,i,t)$ 、 $t\ne0$ 、 $t'=\operatorname{Tail}(t)$ を満たす $t$ が存在する。

証明.(1)を示す。 $j$ に関する帰納法により、次を示す。 $\operatorname{Prefix}_Q(B,C,s,k)$ 、 $\operatorname{Prefix}_Q(B',C',s,k')$ 、 $j\le k$ 、 $j\le k'$ 、 $\operatorname{Cell}_Q(B,C,j,x)$ 、 $\operatorname{Cell}_Q(B',C',j,x')$ ならば $x=x'$ である。 $j=0$ では、 $\operatorname{Prefix}_Q$ の第1連言が両方の第 $0$ セルを $s$ に定めるので、補題 3.1の一意性から $x=x'=s$ である。 $j$ から $Sj$ へ進む段では、 $Sj\le k$ と $Sj\le k'$ から $j<k$ かつ $j<k'$ であるので、 $\operatorname{Prefix}_Q$ の第2連言が、第 $j$ セルの値 $x$ 、第 $Sj$ セルの値 $y$ 、および $\operatorname{Dec}_Q(x,a,y)$ を与える。 $B',C'$ についても同様である。帰納法の仮定により $x=x'$ であり、補題 4.1 (6)の一意性により $y=y'$ である。(1)は、この主張を $j:=i$ 、 $k=k':=i$ として用いれば従う。

(2)を示す。補題 3.2を論理式 $y=s$ と $k:=1$ へ適用すると、 $\operatorname{Cell}_Q(B,C,0,s)$ を満たす $B,C$ が存在する。 $\operatorname{Prefix}_Q(B,C,s,0)$ は第1連言だけなので成り立ち、 $0\le s$ であるから $\operatorname{At}^{0}_Q(s,0,s)$ である。

(3)を示す。 $j$ に関する帰納法により、 $\operatorname{Prefix}_Q(B,C,s,k)$ 、 $j\le k$ 、 $\operatorname{Cell}_Q(B,C,j,x)$ ならば $x+j\le s$ であることを示す。 $j=0$ では $x=s$ である。 $j$ から $Sj$ へ進む段では、 $\operatorname{Dec}_Q(x,a,y)$ が $y<x$ を含むので $Sy\le x$ であり、帰納法の仮定 $x+j\le s$ と合わせて $y+Sj=Sy+j\le x+j\le s$ である。

(4)を示す。 $\operatorname{At}^{0}_Q(s,i,t)$ の証人 $(B,C)$ を取る。 $t\ne0$ であるから補題 4.1 (6)により $\operatorname{Dec}_Q(t,\operatorname{Head}(t),\operatorname{Tail}(t))$ が成り立つ。論理式

\varphi(j,y):\!\!\Longleftrightarrow (j\le i\land\operatorname{Cell}_Q(B,C,j,y)) \lor(j=Si\land y=\operatorname{Tail}(t)) \lor(Si<j\land y=0)

は、補題 3.1により $j<S(Si)$ の各 $j$ に対して一意な $y$ を定める。補題 3.2を $k:=S(Si)$ へ適用して $(B',C')$ を得る。 $j<i$ では旧い表と同じ値をもつので $\operatorname{Prefix}_Q$ の第2連言が保たれ、 $j=i$ では第 $i$ セルが $t\ne0$ 、第 $Si$ セルが $\operatorname{Tail}(t)$ であり $\operatorname{Dec}_Q(t,\operatorname{Head}(t),\operatorname{Tail}(t))$ が成り立つ。従って $\operatorname{Prefix}_Q(B',C',s,Si)$ と $\operatorname{Cell}_Q(B',C',Si,\operatorname{Tail}(t))$ を得る。(3)により $t+i\le s$ であり $0<t$ であるから $Si\le s$ である。よって $\operatorname{At}^{0}_Q(s,Si,\operatorname{Tail}(t))$ である。

(5)を示す。 $\Lambda(i):\!\!\Longleftrightarrow\exists t\,(\operatorname{At}^{0}_Q(s,i,t)\land t\ne0)$ と置く。(3)により $\Lambda(i)$ ならば $Si\le s$ 、すなわち $i<s$ である。従って $\neg\Lambda(s)$ である。補題 1.2を $\neg\Lambda$ へ適用し、 $\neg\Lambda(n)$ を満たす最小の $n$ を取る。 $n\le s$ である。

$i$ に関する帰納法により、 $i\le n\to\exists t\,\operatorname{At}^{0}_Q(s,i,t)$ を示す。 $i=0$ は(2)による。 $i$ から $Si$ へ進む段で $Si\le n$ とすると $i<n$ であるから $n$ の最小性により $\Lambda(i)$ であり、(4)により $\operatorname{At}^{0}_Q(s,Si,\operatorname{Tail}(t))$ を得る。

従って $i\le n$ を満たす各 $i$ について反復尾が存在し、とくに $\operatorname{At}^{0}_Q(s,n,t_n)$ を満たす $t_n$ について $\neg\Lambda(n)$ から $t_n=0$ である。これが第二の主張と第一の主張である。 $i<n$ については $\Lambda(i)$ と(1)から、 $\operatorname{At}^{0}_Q(s,i,t)$ を満たす $t$ は $0$ でない。これが第三の主張である。

(6)を示す。 $\operatorname{At}^{0}_Q(s,Si,t')$ の証人 $(B,C)$ を取ると、 $\operatorname{Prefix}_Q(B,C,s,Si)$ の第2連言は $j<i$ についても成り立つので $\operatorname{Prefix}_Q(B,C,s,i)$ である。(3)により $t'+Si\le s$ であるから $i\le s$ であり、 $(B,C)$ の第 $i$ セルの値を $t$ とすると $\operatorname{At}^{0}_Q(s,i,t)$ である。 $\operatorname{Prefix}_Q$ の第2連言を $j:=i$ について用いると $t\ne0$ かつ $\operatorname{Dec}_Q(t,a,y)$ であり、補題 3.1の一意性から $y=t'$ である。補題 4.1 (6)により $t'=\operatorname{Tail}(t)$ である。▨

次の補題が本記事の中心である。以下では長さ、成分、連結の値を記法の記法で書く。

補題 5.2. $PA$ は次を証明する。

長さ。 任意の $s$ について $\operatorname{Len}^{0}_Q(s,n)$ を満たす $n$ がちょうど一つ存在する。この $n$ を $\operatorname{Len}(s)$ と書く。 $\operatorname{Len}(s)=0$ であることと $s=0$ であることは同値である。 $\operatorname{At}^{0}_Q(s,i,t)$ を満たす $t$ が存在するのは $i\le\operatorname{Len}(s)$ のとき、かつそのときに限る。
成分。 任意の $s,i$ について $\operatorname{Entry}^{0}_Q(s,i,a)$ を満たす $a$ がちょうど一つ存在する。この $a$ を $\operatorname{Entry}(s,i)$ と書く。 $\operatorname{Len}(s)\le i$ のとき $\operatorname{Entry}(s,i)=0$ である。
先頭追加。 $\operatorname{Len}(\operatorname{Cons}(a,s))=S\operatorname{Len}(s)$ 、 $\operatorname{Entry}(\operatorname{Cons}(a,s),0)=a$ 、および任意の $i$ について $\operatorname{Entry}(\operatorname{Cons}(a,s),Si)=\operatorname{Entry}(s,i)$ である。とくに $0<s$ のとき $s=\operatorname{Cons}(\operatorname{Head}(s),\operatorname{Tail}(s))$ であり $\operatorname{Len}(s)=S\operatorname{Len}(\operatorname{Tail}(s))$ である。
連結。 任意の $s,t$ について $\operatorname{Concat}^{0}_Q(s,t,u)$ を満たす $u$ がちょうど一つ存在する。この $u$ を $\operatorname{Concat}(s,t)$ と書く。
連結の再帰。 $\operatorname{Concat}(0,t)=t$ であり、 $\operatorname{Concat}(\operatorname{Cons}(a,s),t)=\operatorname{Cons}(a,\operatorname{Concat}(s,t))$ である。
連結の長さと成分。 $\operatorname{Len}(\operatorname{Concat}(s,t))=\operatorname{Len}(s)+\operatorname{Len}(t)$ であり、 $i<\operatorname{Len}(s)$ について $\operatorname{Entry}(\operatorname{Concat}(s,t),i)=\operatorname{Entry}(s,i)$ 、 $j<\operatorname{Len}(t)$ について $\operatorname{Entry}(\operatorname{Concat}(s,t),\operatorname{Len}(s)+j)=\operatorname{Entry}(t,j)$ である。
末尾追加。 $\operatorname{Snoc}(s,a):=\operatorname{Concat}(s,\operatorname{Cons}(a,0))$ と定めると、 $\operatorname{Len}(\operatorname{Snoc}(s,a))=S\operatorname{Len}(s)$ 、 $i<\operatorname{Len}(s)$ について $\operatorname{Entry}(\operatorname{Snoc}(s,a),i)=\operatorname{Entry}(s,i)$ 、および $\operatorname{Entry}(\operatorname{Snoc}(s,a),\operatorname{Len}(s))=a$ である。

証明.(1)を示す。補題 5.1 (5)が与える $n$ について、補題 5.1 (5)の証人 $(B,C)$ は $\operatorname{Prefix}_Q(B,C,s,n)$ と $\operatorname{Cell}_Q(B,C,n,0)$ を満たし、補題 5.1 (3)により $n\le s$ である。従って $\operatorname{Len}^{0}_Q(s,n)$ である。 $\operatorname{Len}^{0}_Q(s,n')$ を満たす $n'$ を取る。 $n'$ の証人は $\operatorname{At}^{0}_Q(s,n',0)$ を与える。 $n<n'$ とすると、 $\operatorname{Prefix}_Q$ の第2連言が第 $n$ セルの値が $0$ でないことを要求するが、補題 5.1 (1)によりその値は $0$ である。 $n'<n$ とすると、補題 5.1 (5)の第三の主張により第 $n'$ 反復尾は $0$ でないが、 $\operatorname{Cell}_Q$ の一意性から $0$ である。いずれも矛盾なので $n'=n$ である。

$s=0$ ならば補題 5.1 (2)により $\operatorname{At}^{0}_Q(0,0,0)$ であり、第 $0$ 反復尾が $0$ であるから補題 5.1 (5)が与える $n$ は $0$ である。従って $\operatorname{Len}(0)=0$ である。逆に $\operatorname{Len}(s)=0$ ならば $\operatorname{At}^{0}_Q(s,0,0)$ であり、補題 5.1 (1)と補題 5.1 (2)から $s=0$ である。反復尾の存在範囲は、補題 5.1 (5)の第二の主張が与える「 $i\le n$ のとき存在する」ことと、 $i>n$ のとき $\operatorname{Prefix}_Q$ が第 $n$ セルの値が $0$ でないことを要求して矛盾することによる。

(2)を示す。 $n:=\operatorname{Len}(s)$ を取る。 $i<n$ ならば(1)により反復尾 $t$ が一意に存在し、補題 5.1 (5)により $t\ne0$ であるから、補題 4.1 (7)により $\operatorname{Head}^{0}_Q(t,a)$ を満たす $a$ が一意に存在する。 $n\le i$ ならば $\operatorname{Entry}^{0}_Q$ の第2選言が $a=0$ を与える。長さ $n$ が一意であるから、二つの選言が同時に成り立つことはない。よって $a$ は一意である。

(3)を示す。 $c:=\operatorname{Cons}(a,s)$ と置く。補題 4.1 (5)と補題 4.1 (6)により $\operatorname{Dec}_Q(c,a,s)$ であり、 $\operatorname{Head}(c)=a$ 、 $\operatorname{Tail}(c)=s$ である。 $i$ に関する帰納法により、任意の $t$ について $\operatorname{At}^{0}_Q(c,Si,t)$ と $\operatorname{At}^{0}_Q(s,i,t)$ が同値であることを示す。 $i=0$ では、補題 5.1 (2)と補題 5.1 (4)により $\operatorname{At}^{0}_Q(c,1,s)$ であり、補題 5.1 (1)の一意性から同値である。 $i$ から $Si$ へ進む段では、まず $\operatorname{At}^{0}_Q(s,Si,t')$ を仮定する。補題 5.1 (6)により $\operatorname{At}^{0}_Q(s,i,t)$ 、 $t\ne0$ 、 $t'=\operatorname{Tail}(t)$ を満たす $t$ を取ることができ、帰納法の仮定により $\operatorname{At}^{0}_Q(c,Si,t)$ であり、補題 5.1 (4)により $\operatorname{At}^{0}_Q(c,S(Si),t')$ である。逆に $\operatorname{At}^{0}_Q(c,S(Si),t')$ を仮定すると、補題 5.1 (6)と帰納法の仮定と補題 5.1 (4)を逆向きにたどって $\operatorname{At}^{0}_Q(s,Si,t')$ を得る。従って $c$ の第 $Si$ 反復尾は $s$ の第 $i$ 反復尾である。また、補題 5.1 (2)により $c$ の第 $0$ 反復尾は $c$ であり、補題 4.1 (5)により $c\ne0$ である。よって $\operatorname{Len}(c)=S\operatorname{Len}(s)$ であり、成分についての二つの等式も(2)から従う。 $0<s$ のときの分解は補題 4.1 (6)による。

(4)の存在。 $n:=\operatorname{Len}(s)$ とし、 $\operatorname{Prefix}_Q(B,C,s,n)$ と $\operatorname{Cell}_Q(B,C,n,0)$ を満たす $(B,C)$ を取る。 $l$ に関する帰納法により、 $l\le n$ を満たすすべての $l$ について次を示す。

\Xi(l):\quad \exists D\,\exists E\,\Bigl( \operatorname{Cell}_Q(D,E,n,t)\land \forall j\,\bigl(j<n\land n\le j+l\to\Gamma(D,E,j)\bigr)\Bigr)

ここで $\Gamma(D,E,j)$ は、 $\operatorname{Cell}_Q(B,C,j,x)$ 、 $\operatorname{Cell}_Q(B,C,Sj,y)$ 、 $\operatorname{Dec}_Q(x,a,y)$ 、 $\operatorname{Cell}_Q(D,E,j,r)$ 、 $\operatorname{Cell}_Q(D,E,Sj,r')$ 、 $\operatorname{Cons}_Q(a,r',r)$ を満たす $x,y,a,r,r'$ が存在することを表す。第2表は $e_n=t$ 、 $e_j=\operatorname{Cons}(a_j,e_{Sj})$ という後ろ向きの再帰で定まるので、第1表を作ったときの前向きの構成をそのまま流用することはできない。そこで、 $\Xi(l)$ では末尾から $l$ 段だけ定めた表を主張する。

$l=0$ では条件 $j<n\land n\le j$ が成り立たないので、補題 3.2を論理式 $(j=n\land y=t)\lor(j\ne n\land y=0)$ と $k:=Sn$ へ適用して得た $(D,E)$ でよい。

$l$ から $Sl$ へ進む段で $Sl\le n$ とする。 $\Xi(l)$ の証人 $(D,E)$ を取る。 $j_0+Sl=n$ を満たす $j_0$ が存在し、 $j_0<n$ である。 $\operatorname{Prefix}_Q(B,C,s,n)$ から、 $\operatorname{Cell}_Q(B,C,j_0,x)$ 、 $\operatorname{Cell}_Q(B,C,Sj_0,y)$ 、 $x\ne0$ 、 $\operatorname{Dec}_Q(x,a,y)$ を満たす $x,y,a$ を取る。 $(D,E)$ の第 $Sj_0$ セルの値を $r'$ とし、 $r:=\operatorname{Cons}(a,r')$ と置く。補題 3.2を論理式 $(j=j_0\land y'=r)\lor(j\ne j_0\land\operatorname{Cell}_Q(D,E,j,y'))$ と $k:=Sn$ へ適用して $(D',E')$ を得る。 $j_0<n$ より第 $n$ セルは $t$ のままである。 $j<n$ かつ $n\le j+Sl$ を満たす $j$ を取る。 $n\le j+l$ の場合、 $j_0<j$ であるから第 $j$ セルと第 $Sj$ セルは $(D,E)$ と同じ値であり、 $\Xi(l)$ の条件がそのまま移る。 $n=j+Sl$ の場合は $j=j_0$ であり、 $Sj_0\ne j_0$ から第 $Sj_0$ セルが $r'$ のままであるので、構成により $\Gamma(D',E',j_0)$ が成り立つ。

$l=n$ における $\Xi(n)$ では条件 $j<n\land n\le j+n$ が $j<n$ と一致する。 $\Xi(n)$ の証人の第 $0$ セルを $u$ とすると、 $n\le s$ と合わせて $\operatorname{Concat}^{0}_Q(s,t,u)$ が成り立つ。

(4)の一意性。 $\operatorname{Concat}^{0}_Q(s,t,u)$ と $\operatorname{Concat}^{0}_Q(s,t,u')$ の証人を取る。 $\operatorname{Prefix}_Q$ と終端セルの条件は $\operatorname{Len}^{0}_Q(s,n)$ そのものであるから、(1)により両者の $n$ は一致し、補題 5.1 (1)の証明で示した主張により第1表のセルも一致する。 $l$ に関する帰納法により、 $j\le n$ かつ $n\le j+l$ を満たす $j$ について二つの第2表のセルが一致することを示す。 $l=0$ では $j=n$ であり、どちらも $t$ である。 $l$ から $Sl$ へ進む段では、 $n=j+Sl$ の場合を見ればよい。二つの表はいずれも第 $j$ セルを $\operatorname{Cons}(a_j,\cdot)$ の形に定め、 $a_j$ は一致した第1表から $\operatorname{Dec}_Q$ の一意性で定まり、第 $Sj$ セルは帰納法の仮定により一致する。従って第 $j$ セルも一致する。 $l=n$ 、 $j=0$ として $u=u'$ を得る。

(5)を示す。 $\operatorname{Concat}(0,t)=t$ を示す。 $\operatorname{Len}(0)=0$ より $\operatorname{Concat}^{0}_Q(0,t,u)$ の $n$ は $0$ であり、 $\forall j<n$ の条件は空虚である。残る条件は、第1表について $\operatorname{Cell}_Q(B,C,0,0)$ 、第2表について $\operatorname{Cell}_Q(D,E,0,u)$ と $\operatorname{Cell}_Q(D,E,0,t)$ だけである。補題 3.2によりこれらを満たす表は存在し、補題 3.1の一意性から $u=t$ である。

第二の等式を示す。 $s^{+}:=\operatorname{Cons}(a,s)$ と置き、 $n^{+}:=\operatorname{Len}(s^{+})=S\operatorname{Len}(s)$ 、 $n:=\operatorname{Len}(s)$ とする。 $\operatorname{Concat}^{0}_Q(s^{+},t,u)$ の証人 $(B,C)$ と $(D,E)$ を取る。補題 3.2を論理式 $\operatorname{Cell}_Q(B,C,Sj,y)$ と $k:=S n$ へ適用して $(B'',C'')$ を、論理式 $\operatorname{Cell}_Q(D,E,Sj,y)$ と同じ $k$ へ適用して $(D'',E'')$ を得る。すなわち添字を一つずらした表である。

$(B,C)$ の第 $1$ セルは $s^{+}$ の第 $1$ 反復尾、すなわち $s$ であり、第 $n^{+}$ セルは $0$ である。従って $\operatorname{Prefix}_Q(B'',C'',s,n)$ と $\operatorname{Cell}_Q(B'',C'',n,0)$ が成り立つ。 $(D'',E'')$ については、第 $n$ セルが $(D,E)$ の第 $n^{+}$ セル、すなわち $t$ であり、 $j<n$ に対する後ろ向きの再帰条件は $(D,E)$ の $Sj<n^{+}$ に対する条件がそのまま移る。 $(D'',E'')$ の第 $0$ セルを $u_1$ とすると、 $n\le s$ と合わせて $\operatorname{Concat}^{0}_Q(s,t,u_1)$ を得る。すなわち $u_1=\operatorname{Concat}(s,t)$ である。

一方 $(D,E)$ の第 $0$ セル $u$ は、 $j=0$ に対する条件により $\operatorname{Cons}(a_0,u_1)$ に等しく、 $a_0$ は $\operatorname{Dec}_Q(s^{+},a_0,s)$ から定まるので $a_0=a$ である。よって $\operatorname{Concat}(s^{+},t)=\operatorname{Cons}(a,\operatorname{Concat}(s,t))$ である。

(6)を示す。 $n$ に関する帰納法により、 $\operatorname{Len}(s)=n$ を満たすすべての $s$ について主張を示す。 $n=0$ では(1)により $s=0$ であり、(5)の第一の等式から従う。 $n$ から $Sn$ へ進む段では、 $\operatorname{Len}(s)=Sn$ より $s\ne0$ であるから(3)により $s=\operatorname{Cons}(\operatorname{Head}(s),\operatorname{Tail}(s))$ かつ $\operatorname{Len}(\operatorname{Tail}(s))=n$ である。(5)の第二の等式と(3)を合わせ、帰納法の仮定を $\operatorname{Tail}(s)$ へ適用すればよい。

(7)を示す。 $\operatorname{Cons}(a,0)$ は(3)により長さ $1$ で第 $0$ 成分が $a$ の列であるから、(6)をそのまま適用すればよい。▨

§E16.19 定義 4.1の公開する三式 $\operatorname{Len}_Q$ 、 $\operatorname{Entry}_Q$ 、 $\operatorname{Concat}_Q$ は、対応する raw 式へ $\operatorname{Unique}$ を加えたものである。上の補題が raw 式の出力の一意性を与えたので、 $PA$ は公開する三式と raw 式との同値を証明する。以下ではどちらの形も同じ値を表すものとして用いる。同じことが $\operatorname{Pair}_Q$ と $\operatorname{Cons}_Q$ についても補題 4.1から成り立つ。

6 6. 原始再帰関数を PA の内部で扱う

補題 6.1. $f$ を任意の $k$ 変数原始再帰全関数とし、その原始再帰的定義列を一つ固定して、§E16.19 定理 7.1が与える強い表現式を $F_f(\vec x,y)$ とする。このとき $PA$ は次を証明する。

$\forall\vec x\,\exists!y\,F_f(\vec x,y)$ 。
固定した定義列の各方程式が $F_f$ について成り立つ。すなわち、初期関数については表示した等式、合成については構成要素の値による等式、原始再帰については
$f(\vec x,0)=g(\vec x), \qquad f(\vec x,Sn)=h\bigl(\vec x,n,f(\vec x,n)\bigr)$
に対応する等式が、いずれも $PA$ の定理である。

記号の対応に注意する。上流の§E16.19 補題 6.1は、基底関数を $f$ 、step 関数を $g$ 、原始再帰で得られる関数を $h$ と書いている。本補題はこれと役割を入れ替え、得られる関数を $f$ 、基底関数を $g$ 、step 関数を $h$ と書く。両者を突き合わせるときは、本補題の $(f,g,h)$ が上流の $(h,f,g)$ にあたる。

パラメータ列 $\vec x$ の長さが $0$ の場合、上流は基底値を関数の値ではなく一つの自然数 $c$ とし、基底節を $\operatorname{Entry}_Q(s,0,\overline c)$ へ置き換える別扱いをしている。§E16.18 定義 3.1の $\operatorname{Num}$ がまさにこの場合であり、このとき(2)の第一の方程式は $f(0)=c$ という閉じた等式として読む。

証明. 固定した原始再帰的定義列に関するメタ理論の帰納法を行う。(1)と(2)を同時に示す。

初期関数の場合、§E16.19 補題 5.1の表現式は $y=0$ 、 $y=Sx$ 、 $y=x_i$ という明示的な等式であるから、 $Q\subseteq PA$ より全域性、一意性、および等式そのものを得る。

合成 $f(\vec x)=h(g_1(\vec x),\ldots,g_m(\vec x))$ の場合、§E16.19 補題 5.2の表現式は構成要素の表現式の存在量化による合成である。外側の帰納法の仮定により、 $PA$ は各 $g_j$ と $h$ について(1)と(2)を証明する。存在量化された各 $z_j$ を順に消去すれば、 $f$ の値の存在、一意性、および合成の等式を得る。ここでは $PA$ の帰納法を用いない。

原始再帰の場合を示す。§E16.19 補題 6.1の表現式は

\varphi_f(\vec x,r,y):\!\!\Longleftrightarrow \exists s\,\bigl(\operatorname{Run}(\vec x,r,s)\land\operatorname{Entry}_Q(s,r,y)\bigr)

の形をもち、 $\operatorname{Run}$ は $\operatorname{Len}_Q(s,Sr)$ 、基底節、および $\forall i<r$ の step 節の連言である。 $r$ に関する $PA$ の帰納法により、 $\operatorname{Run}(\vec x,r,s)$ を満たす $s$ の存在を示す。 $r=0$ では、外側の帰納法の仮定が与える $g(\vec x)$ の値 $a_0$ について $s:=\operatorname{Cons}(a_0,0)$ を取る。補題 5.2 (3)により $\operatorname{Len}(s)=1$ かつ $\operatorname{Entry}(s,0)=a_0$ であり、step 節は空虚に成り立つ。 $r$ から $Sr$ へ進む段では、帰納法の仮定が与える $s$ の第 $r$ 成分 $a_r$ へ、外側の帰納法の仮定が与える $h(\vec x,r,a_r)$ の値 $a_{Sr}$ を取り、 $s':=\operatorname{Snoc}(s,a_{Sr})$ とする。補題 5.2 (7)により $\operatorname{Len}(s')=S(Sr)$ であり、 $i\le r$ の成分は変わらず、第 $Sr$ 成分は $a_{Sr}$ である。従って基底節と $i<Sr$ の step 節がすべて成り立つ。

一意性を示す。 $\operatorname{Run}(\vec x,r,s)$ と $\operatorname{Run}(\vec x,r,s')$ を仮定する。 $j$ に関する帰納法により、 $j\le r$ について $\operatorname{Entry}(s,j)=\operatorname{Entry}(s',j)$ を示す。 $j=0$ は基底節と $g$ の値の一意性による。 $j$ から $Sj$ へ進む段は、step 節と $h$ の値の一意性による。従って第 $r$ 成分が一致し、 $\varphi_f(\vec x,r,y)$ の出力は一意である。

(2)の定義方程式は、いま構成した計算列の基底節と最後の一段からそのまま読み取ることができる。 $r=0$ の計算列の第 $0$ 成分が $g(\vec x)$ の値であることが第一の方程式であり、 $r$ から $Sr$ への延長が第二の方程式である。

パラメータ列の長さが $0$ の場合も同じ議論が通る。この場合、上流が別扱いする基底節は $\operatorname{Entry}_Q(s,0,\overline c)$ であり、上の $r=0$ の段で $a_0$ として取る値が $g(\vec x)$ の値ではなく固定した自然数 $c$ になる。step 関数 $h$ は二変数、得られる $f$ は一変数であり、いずれも正のアリティである。以後の存在と一意性の帰納法は、基底の一段をこの閉じた等式に取り替えるだけで、そのまま成り立つ。▨

記法：PA 内で原始再帰関数を項として書く記法 $f$ を原始再帰全関数とし、 $F_f$ を補題 6.1の表現式とする。記法の記法を $R:=F_f$ について用い、その値を $f(\vec x)$ と書く。(1)により略記は一意に定まり、(2)により $PA$ は $f$ の定義方程式を等式として用いることができる。従って、 $PA$ の内部では $f$ を全域一価な関数記号のように扱うことができる。 $L_A$ に新しい関数記号を追加してはいない。

補題 6.2. $R(\vec x,i)$ を原始再帰関係とし、 $\mu(\vec x,n)$ を、 $R(\vec x,i)$ を満たす $i\le n$ が存在すればその最小のもの、存在しなければ $Sn$ を返す関数とする。 $\mu$ は原始再帰全関数であり、 $PA$ は

\mu(\vec x,n)\le n\leftrightarrow\exists i\le n\,\rho_R(\vec x,i), \qquad \mu(\vec x,n)\le n\to \bigl(\rho_R(\vec x,\mu(\vec x,n))\land\forall j<\mu(\vec x,n)\,\neg\rho_R(\vec x,j)\bigr)

を証明する。ここで $\rho_R$ は§E16.19 定理 7.1 (2)が与える表現式である。

証明. $\chi_R$ を $R$ の特性関数とする。 $\mu$ は $n$ に関する通常の原始再帰

\mu(\vec x,0)= \begin{cases}0&\chi_R(\vec x,0)=1,\\1&\text{それ以外},\end{cases} \qquad \mu(\vec x,Sn)= \begin{cases} \mu(\vec x,n)&\mu(\vec x,n)\le n,\\ Sn&n<\mu(\vec x,n)\land\chi_R(\vec x,Sn)=1,\\ S(Sn)&\text{それ以外} \end{cases}

で得るので原始再帰的である。場合分けの述語を関係 $R$ そのものではなく特性関数の値 $\chi_R(\vec x,i)=1$ で書いたのは、 $PA$ の内部で扱うことができるのが $L_A$ 論理式と原始再帰関数の値だけだからである。§E16.19 定理 7.1 (2)は $\rho_R(\vec x):\!\!\Longleftrightarrow\varphi_{\chi_R}(\vec x,\overline1)$ と定めているので、記法の記法のもとで $PA$ は

\rho_R(\vec x,i)\leftrightarrow\chi_R(\vec x,i)=1

を証明する。以下ではこの同値により、表現式 $\rho_R$ と特性関数の値による条件とを同じものとして用いる。補題 6.1により $PA$ は表示した二つの方程式を証明する。主張の二つの式は、 $n$ に関する $PA$ の帰納法によって同時に得る。 $n=0$ では場合分けそのものである。 $n$ から $Sn$ へ進む段では、 $\mu(\vec x,n)\le n$ の場合に帰納法の仮定をそのまま用い、そうでない場合には $i\le n$ の範囲に $\rho_R(\vec x,i)$ を満たす $i$ が無いことを帰納法の仮定から得て、 $Sn$ における判定と合わせる。▨

補題 6.3.補題 6.1が $PA$ の定理として与えるのは、固定した原始再帰的定義列の方程式だけである。そこで、切捨て減法と固定数 $2$ による商について、本記事が用いる定義列を次に明示する。

\begin{aligned} \operatorname{pred}(0)&=0,& \operatorname{pred}(Sx)&=x,\\ x\mathbin{\dot-}0&=x,& x\mathbin{\dot-}Sy&=\operatorname{pred}(x\mathbin{\dot-}y),\\ \operatorname{par}(0)&=0,& \operatorname{par}(Sx)&=S0\mathbin{\dot-}\operatorname{par}(x),\\ \operatorname{half}(0)&=0,& \operatorname{half}(Sx)&=\operatorname{half}(x)+\operatorname{par}(x). \end{aligned}

前者関数と切捨て減法の定義列は、§E15.7 命題 2.3の証明が明示しているものと同じである。固定数 $2$ による商については、上流は「 $x$ を $2$ で割った商」という値の特性づけを与えており、同証明が挙げる $qb\le n$ を満たす最大の $q\le n$ の有界探索は、原始再帰性を示すために選んだ一つの構成である。定義列を一つ固定するのは本記事の作業であり、上に表示した $\operatorname{half}$ がその定義列である。メタ理論では上流の構成と値が一致するが、 $PA$ の内部で用いる方程式は定義列ごとに別であるから、以下では表示した定義列の方程式だけを用いる。

いずれも通常の原始再帰であり、メタ理論での値は順に前者関数、切捨て減法、 $x$ を $2$ で割った余り、 $x$ を $2$ で割った商である。 $PA$ は次を証明する。

$x\mathbin{\dot-}y=0\leftrightarrow x\le y$ 、および $y\le x\to(x\mathbin{\dot-}y)+y=x$ 。
$(x\mathbin{\dot-}y)\mathbin{\dot-}z=x\mathbin{\dot-}(y+z)$ 。
$\operatorname{par}(x)\le S0$ 、 $\operatorname{par}(x)+\operatorname{par}(Sx)=S0$ 、および $\operatorname{half}(x)+\operatorname{half}(x)+\operatorname{par}(x)=x$ 。したがって $\operatorname{half}(x)$ は $x$ を $SS0$ で割った商であり、 $\operatorname{par}(x)$ はその余りである。
$\operatorname{half}(0)=0$ 、 $\operatorname{half}(S0)=0$ 、および $\operatorname{half}(SSx)=S\operatorname{half}(x)$ 。

証明.補題 6.1により、 $PA$ は表示した定義方程式をすべて証明する。以下の帰納法はいずれも $PA$ の内部で行う。

(1)を示す。 $y$ に関する帰納法により、二つの主張「 $y\le x\to(x\mathbin{\dot-}y)+y=x$ 」と「 $x\le y\to x\mathbin{\dot-}y=0$ 」を同時に示す。 $y=0$ では、前者は $x\mathbin{\dot-}0=x$ そのものであり、後者は補題 1.1 (4)により $x=0$ となることによる。 $y$ から $Sy$ へ進む段で前者を示す。 $Sy\le x$ とすると $y\le x$ であるから、帰納法の仮定により $(x\mathbin{\dot-}y)+y=x$ である。 $x\mathbin{\dot-}y=0$ とすると $x=y$ となり $Sy\le y$ に反するので、 $x\mathbin{\dot-}y=Su$ を満たす $u$ が存在する。定義方程式により $x\mathbin{\dot-}Sy=\operatorname{pred}(Su)=u$ であり、 $u+Sy=Su+y=x$ である。後者を示す。 $x\le Sy$ とすると、補題 1.1 (4)により $x\le y$ または $x=Sy$ である。 $x\le y$ ならば帰納法の仮定と $\operatorname{pred}(0)=0$ により $x\mathbin{\dot-}Sy=0$ である。 $x=Sy$ ならば、いま示した前者により $(x\mathbin{\dot-}y)+y=Sy=S0+y$ であり、加法の消約律により $x\mathbin{\dot-}y=S0$ 、従って $x\mathbin{\dot-}Sy=\operatorname{pred}(S0)=0$ である。

逆向きの含意 $x\mathbin{\dot-}y=0\to x\le y$ を示す。補題 1.1 (3)により $x\le y$ または $y\le x$ である。前者ならば示すことがない。後者で $x\ne y$ とすると、いま示した等式により $(x\mathbin{\dot-}y)+y=x$ であり、 $x\mathbin{\dot-}y=0$ から $y=x$ となって矛盾する。

(2)は $z$ に関する帰納法による。 $z=0$ では両辺が $x\mathbin{\dot-}y$ である。 $z$ から $Sz$ へ進む段では、定義方程式と帰納法の仮定により $(x\mathbin{\dot-}y)\mathbin{\dot-}Sz=\operatorname{pred}\bigl(x\mathbin{\dot-}(y+z)\bigr)=x\mathbin{\dot-}S(y+z)=x\mathbin{\dot-}(y+Sz)$ である。

(3)は $x$ に関する帰納法による。 $x=0$ では $\operatorname{par}(0)=0\le S0$ 、 $\operatorname{par}(S0)=S0\mathbin{\dot-}0=S0$ より $\operatorname{par}(0)+\operatorname{par}(S0)=S0$ 、および $0+0+0=0$ である。 $x$ から $Sx$ へ進む段では、帰納法の仮定 $\operatorname{par}(x)\le S0$ により $\operatorname{par}(x)=0$ または $\operatorname{par}(x)=S0$ である。(1)により、前者では $\operatorname{par}(Sx)=S0\mathbin{\dot-}0=S0$ 、後者では $\operatorname{par}(Sx)=S0\mathbin{\dot-}S0=0$ であるから、 $\operatorname{par}(Sx)\le S0$ が成り立つ。この $\operatorname{par}(Sx)\le S0$ に同じ場合分けを適用すると、 $\operatorname{par}(Sx)=0$ のとき $\operatorname{par}(SSx)=S0$ 、 $\operatorname{par}(Sx)=S0$ のとき $\operatorname{par}(SSx)=0$ であるから、 $\operatorname{par}(Sx)+\operatorname{par}(SSx)=S0$ が成り立つ。また

\operatorname{half}(Sx)+\operatorname{half}(Sx)+\operatorname{par}(Sx) =\bigl(\operatorname{half}(x)+\operatorname{half}(x)+\operatorname{par}(x)\bigr) +\bigl(\operatorname{par}(x)+\operatorname{par}(Sx)\bigr) =x+S0=Sx

である。(Q6) と (Q7) および補題 1.1 (1)により $\operatorname{half}(x)\times SS0=\operatorname{half}(x)+\operatorname{half}(x)$ であり、 $\operatorname{par}(x)\le S0<SS0$ であるから、補題 1.3の一意性により $\operatorname{half}(x)$ は $x$ を $SS0$ で割った商、 $\operatorname{par}(x)$ はその余りである。

(4)を示す。 $\operatorname{half}(S0)=\operatorname{half}(0)+\operatorname{par}(0)=0$ である。また(3)により

\operatorname{half}(SSx)=\operatorname{half}(Sx)+\operatorname{par}(Sx) =\operatorname{half}(x)+\operatorname{par}(x)+\operatorname{par}(Sx) =\operatorname{half}(x)+S0=S\operatorname{half}(x)

である。▨

補題 6.4.§E16.17 定義 2.1の対関数、先頭追加、先頭、尾と、§E16.17 補題 3.1の証明が用いる反復尾 $I$ および成分取得 $E$ を、原始再帰全関数として記法の記法で書く。記号を区別する。補題 4.1は、算術式 $\operatorname{Pair}_Q$ 、 $\operatorname{Cons}_Q$ 、 $\operatorname{Dec}_Q$ が一意に定める値を $\operatorname{pair}$ 、 $\operatorname{Cons}$ 、 $\operatorname{Head}$ 、 $\operatorname{Tail}$ と書いている。原始再帰的定義列が与える値がこれらに一致することは(1)と(2)で示すことがらであるから、示すまでは原始再帰関数の側を $\operatorname{pair}^{\ast}$ 、 $\operatorname{Cons}^{\ast}$ 、 $\operatorname{Head}^{\ast}$ 、 $\operatorname{Tail}^{\ast}$ と書く。

上流は対関数を三角数と固定数 $2$ による商の合成として定めているが、その逆については、§E16.17 定義 1.1が $\operatorname{pair}\bigl(\operatorname{left}(z),\operatorname{right}(z)\bigr)=z$ という特性づけを与えるだけである。§E16.17 補題 1.2の証明が挙げる $0\le a,b\le z$ の範囲の二変数の有界探索は、原始再帰性を示すために選んだ一つの構成であって、定義列の固定ではない。二変数の有界探索については、補題 6.2が与える一変数の最小化の法則をそのまま用いることができない。そこで本記事では次の定義列を固定する。補題 6.3の $\operatorname{half}$ と切捨て減法を用い、

\operatorname{tri}(w)=\operatorname{half}(w\times Sw), \qquad \operatorname{pair}^{\ast}(a,b)=\operatorname{tri}(a+b)+b, \qquad \operatorname{Cons}^{\ast}(a,t)=S\operatorname{pair}^{\ast}(a,t)

とする。逆関数は、対の探索を一変数の最小化へ落として

\operatorname{lev}(z)=\mu w\le z\,\bigl[\,Sz\mathbin{\dot-}\operatorname{tri}(Sw)=0\,\bigr], \qquad \operatorname{right}(z)=z\mathbin{\dot-}\operatorname{tri}(\operatorname{lev}(z)), \qquad \operatorname{left}(z)=\operatorname{lev}(z)\mathbin{\dot-}\operatorname{right}(z)

と定める。 $\operatorname{lev}(z)$ は $\operatorname{tri}(w)\le z<\operatorname{tri}(Sw)$ を満たす段 $w$ を一変数の最小化で選ぶ関数である。メタ理論での値は上流の定義と一致する。どちらも $\operatorname{pair}^{\ast}(a,b)=z$ を満たす唯一の対 $(a,b)$ を返すからである。 $\operatorname{Head}^{\ast}$ と $\operatorname{Tail}^{\ast}$ は上流と同じく、 $0<s$ のとき $\operatorname{Head}^{\ast}(s)=\operatorname{left}(s\mathbin{\dot-}1)$ 、 $\operatorname{Tail}^{\ast}(s)=\operatorname{right}(s\mathbin{\dot-}1)$ とし、 $s=0$ のときはいずれも $0$ とする。 $PA$ は次を証明する。

$\operatorname{Pair}_Q(a,b,c)\leftrightarrow c=\operatorname{pair}^{\ast}(a,b)$ 、および $\operatorname{Cons}_Q(a,t,c)\leftrightarrow c=\operatorname{Cons}^{\ast}(a,t)$ 。すなわち $\operatorname{pair}^{\ast}(a,b)=\operatorname{pair}(a,b)$ かつ $\operatorname{Cons}^{\ast}(a,t)=\operatorname{Cons}(a,t)$ である。
任意の $z$ について $\operatorname{pair}^{\ast}\bigl(\operatorname{left}(z),\operatorname{right}(z)\bigr)=z$ である。従って補題 4.1 (3)が与える対の一意性により、 $\operatorname{left}\bigl(\operatorname{pair}(a,b)\bigr)=a$ かつ $\operatorname{right}\bigl(\operatorname{pair}(a,b)\bigr)=b$ である。また $\operatorname{Head}^{\ast}$ と $\operatorname{Tail}^{\ast}$ の値は補題 4.1 (6)が定める $\operatorname{Head}$ と $\operatorname{Tail}$ の値に等しい。
$I(s,i)$ は、 $i\le\operatorname{Len}(s)$ のとき $\operatorname{At}^{0}_Q(s,i,t)$ を満たす $t$ に等しく、 $\operatorname{Len}(s)<i$ のとき $0$ である。
$E(s,i)=\operatorname{Entry}(s,i)$ である。

証明.(1)を示す。 $w:=a+b$ と置く。補題 4.1 (1)の証明で示したとおり、 $PA$ は $w\times Sw=h+h$ を満たす $h$ の存在を証明する。一方補題 6.3 (3)により

\operatorname{half}(w\times Sw)+\operatorname{half}(w\times Sw)+\operatorname{par}(w\times Sw)=w\times Sw=h+h

であり、 $\operatorname{par}(w\times Sw)\le S0<SS0$ であるから、補題 1.3の一意性により $\operatorname{tri}(w)=\operatorname{half}(w\times Sw)=h$ かつ $\operatorname{par}(w\times Sw)=0$ である。この議論は任意の $w$ について通るので、 $PA$ は $\forall w\,\bigl(\operatorname{tri}(w)+\operatorname{tri}(w)=w\times Sw\bigr)$ を証明する。従って固定した定義列による値 $\operatorname{pair}^{\ast}(a,b)=\operatorname{tri}(w)+b=h+b$ は

\operatorname{pair}^{\ast}(a,b)+\operatorname{pair}^{\ast}(a,b)=(w\times Sw)+(b+b)

を満たし、 $\operatorname{pair}^{\ast}(a,b)\le\operatorname{pair}^{\ast}(a,b)+\operatorname{pair}^{\ast}(a,b)$ でもあるから $\operatorname{Pair}^{0}_Q\bigl(a,b,\operatorname{pair}^{\ast}(a,b)\bigr)$ が成り立つ。補題 4.1 (1)が与える一意性により、 $\operatorname{Pair}_Q(a,b,c)\leftrightarrow c=\operatorname{pair}^{\ast}(a,b)$ である。 $\operatorname{Cons}^{\ast}$ については、固定した定義 $\operatorname{Cons}^{\ast}(a,t)=S\operatorname{pair}^{\ast}(a,t)$ と補題 4.1 (5)から従う。

(2)を示す。まず、 $PA$ が $\operatorname{tri}(Sw)=\operatorname{tri}(w)+Sw$ を証明することを見る。(1)で示した $\operatorname{tri}(u)+\operatorname{tri}(u)=u\times Su$ を $u:=Sw$ と $u:=w$ について用いると

\operatorname{tri}(Sw)+\operatorname{tri}(Sw)=Sw\times SSw=w\times Sw+(Sw+Sw) =\bigl(\operatorname{tri}(w)+Sw\bigr)+\bigl(\operatorname{tri}(w)+Sw\bigr)

であり、補題 1.1 (2)の消約律により求める等式を得る。

$\operatorname{lev}$ の最小化について、補題 6.2を関係 $R(z,w):\!\!\Longleftrightarrow Sz\mathbin{\dot-}\operatorname{tri}(Sw)=0$ へ適用する。その特性関数は $\chi_R(z,w)=1\mathbin{\dot-}\bigl(Sz\mathbin{\dot-}\operatorname{tri}(Sw)\bigr)$ という切捨て減法の合成であり、補題 6.3 (1)により $PA$ は $\chi_R(z,w)=1\leftrightarrow Sz\le\operatorname{tri}(Sw)$ を証明する。 $w:=z$ は条件を満たす。実際、補題 1.1 (5)により $Sz\times SSz\ge Sz\times SS0$ であり、(Q6) と (Q7) および補題 1.1 (1)により $Sz\times SS0=Sz+Sz$ であるから、 $\operatorname{tri}(Sz)+\operatorname{tri}(Sz)=Sz\times SSz$ と補題 1.1 (6)から $Sz\le\operatorname{tri}(Sz)$ である。従って $\operatorname{lev}(z)\le z$ であり、最小性から

\operatorname{tri}(\operatorname{lev}(z))\le z<\operatorname{tri}(S\operatorname{lev}(z))=\operatorname{tri}(\operatorname{lev}(z))+S\operatorname{lev}(z)

が成り立つ。左側は、 $\operatorname{lev}(z)=0$ のときは $\operatorname{tri}(0)=0$ から、 $\operatorname{lev}(z)=Sw_1$ のときは $w_1$ が条件を満たさないこと、すなわち $\operatorname{tri}(\operatorname{lev}(z))<Sz$ から従う。右側は $\operatorname{lev}(z)$ 自身が条件を満たすことによる。

$w_0:=\operatorname{lev}(z)$ 、 $b:=\operatorname{right}(z)$ 、 $a:=\operatorname{left}(z)$ と置く。補題 6.3 (1)により $b+\operatorname{tri}(w_0)=z$ であり、右側の不等式から $b<Sw_0$ 、すなわち $b\le w_0$ である。補題 6.3 (1)により $a+b=w_0$ であるから

\operatorname{pair}^{\ast}(a,b)=\operatorname{tri}(a+b)+b=\operatorname{tri}(w_0)+b=z

である。この議論は任意の $z$ について通るので、 $PA$ は $\forall z\ \operatorname{pair}^{\ast}\bigl(\operatorname{left}(z),\operatorname{right}(z)\bigr)=z$ を証明する。(1)により $\operatorname{pair}^{\ast}$ の値は $\operatorname{pair}$ の値であるから、 $z:=\operatorname{pair}(a,b)$ と取ると、補題 4.1 (3)が与える対の一意性により $\operatorname{left}\bigl(\operatorname{pair}(a,b)\bigr)=a$ かつ $\operatorname{right}\bigl(\operatorname{pair}(a,b)\bigr)=b$ である。 $0<s$ とすると $s=Sp$ を満たす $p$ が存在し、 $s\mathbin{\dot-}1=p$ である。いま示したことにより $\operatorname{pair}^{\ast}\bigl(\operatorname{left}(p),\operatorname{right}(p)\bigr)=p$ 、すなわち $\operatorname{Cons}^{\ast}\bigl(\operatorname{left}(p),\operatorname{right}(p)\bigr)=s$ である。補題 4.1 (3)により対は一意であるから、 $\operatorname{Head}^{\ast}(s)$ と $\operatorname{Tail}^{\ast}(s)$ は補題 4.1 (6)が定める $a,t$ に等しい。 $s=0$ では双方の規約により値が $0$ である。

(3)を示す。 $I(s,0)=s$ 、 $I(s,Sj)=\operatorname{Tail}^{\ast}(I(s,j))$ は通常の原始再帰であるから、補題 6.1により $PA$ はこの二式を証明する。 $i$ に関する $PA$ の帰納法を行う。 $i=0$ では補題 5.1 (2)による。 $i$ から $Si$ へ進む段では、 $i<\operatorname{Len}(s)$ ならば第 $i$ 反復尾 $t$ は $0$ でないので、(2)と補題 5.1 (4)により第 $Si$ 反復尾は $\operatorname{Tail}^{\ast}(t)$ である。 $i=\operatorname{Len}(s)$ ならば $t=0$ であり、 $\operatorname{Tail}^{\ast}(0)=0$ であるから以後 $0$ にとどまる。

(4)は、(2)と(3)および補題 5.2 (2)から従う。 $i<\operatorname{Len}(s)$ では $E(s,i)=\operatorname{Head}^{\ast}(I(s,i))$ が第 $i$ 反復尾の先頭であり、 $\operatorname{Len}(s)\le i$ では $I(s,i)=0$ から $E(s,i)=0$ である。▨

(1)と(2)により、原始再帰的定義列が与える $\operatorname{pair}^{\ast}$ 、 $\operatorname{Cons}^{\ast}$ 、 $\operatorname{Head}^{\ast}$ 、 $\operatorname{Tail}^{\ast}$ の値は、算術式が一意に定める $\operatorname{pair}$ 、 $\operatorname{Cons}$ 、 $\operatorname{Head}$ 、 $\operatorname{Tail}$ の値に等しい。以下では星印を落とし、どちらの側の定義から得た値も同じ記号で書く。

6.1 コース再帰の還元が定義方程式を満たすこと

§E16.17 補題 3.1と§E16.17 補題 3.2は、コース再帰を通常の原始再帰へ還元して原始再帰性を得る。しかし、還元によって得た関数が元の再帰方程式を満たすことは、どちらの記事でもメタ理論の帰納法で示されている。補題 6.1が $PA$ の定理として与えるのは、還元後の通常の原始再帰の方程式だけである。 $PA$ の内部で元の構造再帰方程式を用いるには、次の補題が要る。

補題 6.5.

履歴版。§E16.17 補題 3.1の記号を用い、 $PA$ が $\forall\vec x\,\forall s\,(0<s\to D(\vec x,s)<s)$ を証明すると仮定する。このとき $PA$ は
$F(\vec x,0)=B(\vec x), \qquad 0<s\to F(\vec x,s)=G\bigl(\vec x,s,F(\vec x,D(\vec x,s))\bigr)$
を証明する。
有限分岐版。§E16.17 補題 3.2の記号を用い、 $PA$ が
$\forall q\,\forall j\,\bigl(j<m(q)\to r(d(q,j))<r(q)\bigr), \qquad \forall q\ m(q)\le K$
の二つをともに証明すると仮定する。上流は子の個数の上界 $m(q)\le K$ をメタ理論の条件として置いているが、本項の証明は $PA$ の内部でこの不等式を用いるので、 $PA$ の定理であることを別に仮定する。 $K$ の値そのものに制限は置かない。このとき $PA$ は
$\operatorname{Eval}(q)=C\bigl(q,\operatorname{Hist}(q,m(q))\bigr)$
を証明する。ここで $\operatorname{Hist}$ は $\operatorname{Hist}(q,0)=0$ 、 $\operatorname{Hist}(q,Sj)=\operatorname{Cons}\bigl(\operatorname{Eval}(d(q,j)),\operatorname{Hist}(q,j)\bigr)$ で定まる原始再帰全関数であり、子の値を逆順に並べた列である。

証明.(1)を示す。還元は、履歴 $H$ と一段の値 $V$ を通常の原始再帰

H(\vec x,0)=0, \qquad H(\vec x,Sn)=\operatorname{Cons}\bigl(V(\vec x,n),H(\vec x,n)\bigr)

で定め、 $F(\vec x,n)=E(H(\vec x,Sn),0)$ とする。ここで $E(t,j)$ は第 $j$ 成分を取る関数である。補題 6.1により $PA$ はこれらの方程式を証明する。また補題 6.4により、ここに現れる $\operatorname{Cons}$ と $E$ の値は API 式が定める先頭追加と成分に等しい。

$n$ に関する $PA$ の帰納法により、次を示す。 $j+Sd=n$ ならば $E(H(\vec x,n),j)=V(\vec x,d)$ である。 $n=0$ では前件を満たす $j,d$ が存在しない。 $n$ から $Sn$ へ進む段では、補題 5.2 (3)により、 $H(\vec x,Sn)$ の第 $0$ 成分は $V(\vec x,n)$ であり、第 $Sj$ 成分は $H(\vec x,n)$ の第 $j$ 成分である。 $j+Sd=Sn$ において $j=0$ なら $d=n$ であり、 $j=Sj'$ なら $j'+Sd=n$ であるから帰納法の仮定を用いることができる。

$j:=0$ 、 $d:=n$ として $F(\vec x,n)=E(H(\vec x,Sn),0)=V(\vec x,n)$ を得る。従って $F(\vec x,0)=V(\vec x,0)=B(\vec x)$ である。 $0<n$ のとき、 $V$ の定義方程式は

V(\vec x,n)=G\bigl(\vec x,n,E(H(\vec x,n),j)\bigr), \qquad j+S D(\vec x,n)=n

である。§E16.17 補題 3.1は第2引数の添字を切捨て減法の項 $(n\mathbin{\dot-}1)\mathbin{\dot-}D(\vec x,n)$ として書いているので、表示した $j$ がこの項の値であることを確かめる。仮定により $PA$ は $D(\vec x,n)<n$ 、すなわち $SD(\vec x,n)\le n$ を証明する。補題 6.3 (2)により $(n\mathbin{\dot-}1)\mathbin{\dot-}D(\vec x,n)=n\mathbin{\dot-}SD(\vec x,n)$ であり、補題 6.3 (1)により

\bigl((n\mathbin{\dot-}1)\mathbin{\dot-}D(\vec x,n)\bigr)+SD(\vec x,n)=n

である。従って $j+SD(\vec x,n)=n$ を満たす $j$ が存在し、加法の消約律によりそれは切捨て減法の項の値に等しい。上で示した主張を $d:=D(\vec x,n)$ について用いると $E(H(\vec x,n),j)=V(\vec x,D(\vec x,n))=F(\vec x,D(\vec x,n))$ であり、求める方程式を得る。

(2)を示す。還元は、状態遷移 $\operatorname{Step}$ と、上界を与える関数 $N_K(0)=1$ 、 $N_K(Ss)=1+K\times N_K(s)$ を用い、開始状態からの接頭トレース $R(q,n)$ を通常の原始再帰で定め、 $\operatorname{Eval}(q)=\operatorname{Out}\bigl(R(q,3N_K(r(q)))\bigr)$ とする。ここで $\operatorname{Out}$ は唯一の $\operatorname{Val}$ の成分を返す原始再帰関数であり、 $\operatorname{Out}(\operatorname{Cons}(\operatorname{Val}(v),0))=v$ である。 $\operatorname{Iter}(\sigma,0)=\sigma$ 、 $\operatorname{Iter}(\sigma,Sn)=\operatorname{Step}(\operatorname{Iter}(\sigma,n))$ と置くと、 $PA$ は $R(q,n)=\operatorname{Iter}(\operatorname{Cons}(\operatorname{Req}(q),0),n)$ と $\operatorname{Iter}(\sigma,m+n)=\operatorname{Iter}(\operatorname{Iter}(\sigma,m),n)$ を $n$ に関する帰納法で証明する。

$\operatorname{Step}$ は、タグ照合、 $\operatorname{Head}$ 、 $\operatorname{Tail}$ 、 $\operatorname{Cons}$ 、成分取得、有界比較、および $r,m,d,C$ の合成である。従って補題 6.1、補題 6.2、補題 6.4、および補題 5.2により、 $PA$ は $\operatorname{Step}$ の定義の各場合の等式を証明する。とくに次の四つを用いる。

\begin{aligned} m(q)=0&\ \Rightarrow\ \operatorname{Step}\bigl(\operatorname{Cons}(\operatorname{Req}(q),\sigma)\bigr) =\operatorname{Cons}\bigl(\operatorname{Val}(C(q,0)),\sigma\bigr),\\ 0<m(q)&\ \Rightarrow\ \operatorname{Step}\bigl(\operatorname{Cons}(\operatorname{Req}(q),\sigma)\bigr) =\operatorname{Cons}\bigl(\operatorname{Req}(d(q,0)), \operatorname{Cons}(\operatorname{Frame}(q,1,0),\sigma)\bigr),\\ j<m(q)&\ \Rightarrow\ \operatorname{Step}\bigl(\operatorname{Cons}(\operatorname{Val}(a), \operatorname{Cons}(\operatorname{Frame}(q,j,h),\sigma))\bigr) =\operatorname{Cons}\bigl(\operatorname{Req}(d(q,j)), \operatorname{Cons}(\operatorname{Frame}(q,Sj,\operatorname{Cons}(a,h)),\sigma)\bigr),\\ j=m(q)&\ \Rightarrow\ \operatorname{Step}\bigl(\operatorname{Cons}(\operatorname{Val}(a), \operatorname{Cons}(\operatorname{Frame}(q,j,h),\sigma))\bigr) =\operatorname{Cons}\bigl(\operatorname{Val}(C(q,\operatorname{Cons}(a,h))),\sigma\bigr). \end{aligned}

さらに、停止状態では $\operatorname{Step}$ を恒等写像と定めているので、 $PA$ は $\operatorname{Step}(\operatorname{Cons}(\operatorname{Val}(v),0))=\operatorname{Cons}(\operatorname{Val}(v),0)$ を証明し、 $n$ に関する帰納法により、いったん停止状態に達すればそれ以降の状態も同じであることを証明する。

$\beta(\rho):=\bigl(2N_K(\rho)\bigr)\mathbin{\dot-}1$ と置く。ここで切捨て減法は補題 6.3が固定した定義列のものであり、 $L_A$ の関数記号ではなく記法の記法で読む。 $N_K(0)=1$ と $N_K(Ss)=1+K\times N_K(s)$ から、 $PA$ は $s$ に関する帰納法により $1\le N_K(s)$ を証明する。従って $PA$ は次の三つを証明する。

S\beta(\rho)=2N_K(\rho), \qquad \beta(\rho)\le3N_K(\rho), \qquad \beta(S\rho)=S\bigl(K\times(2N_K(\rho))\bigr)

三つの根拠は同じではないので、式ごとに分けて述べる。第一の等式は、 $1\le N_K(\rho)$ と補題 1.1 (5)の乗法の単調性が与える $S0\le2N_K(\rho)$ に、補題 6.3 (1)の後半 $y\le x\to(x\mathbin{\dot-}y)+y=x$ を $x:=2N_K(\rho)$ 、 $y:=S0$ として当てることによる。第二の不等式は、 $\beta(\rho)<S\beta(\rho)=2N_K(\rho)$ と、 $SS0\le SSS0$ に同じく補題 1.1 (5)の乗法の単調性を当てて得る $2N_K(\rho)\le3N_K(\rho)$ による。第三の等式は、 $N_K(S\rho)=1+K\times N_K(\rho)$ に補題 1.1 (1)の分配律と交換律を当てて得る $2N_K(S\rho)=SS\bigl(K\times(2N_K(\rho))\bigr)$ と、補題 6.3が表示した定義列そのものが与える $x\mathbin{\dot-}S0=\operatorname{pred}(x\mathbin{\dot-}0)=\operatorname{pred}(x)$ および $\operatorname{pred}(Sy)=y$ による。第三の等式が用いるのは補題 1.1 (1)ではなく、同補題が固定した定義列である。 $\rho$ に関する $PA$ の帰納法により、次の主張 $\Pi(\rho)$ を示す。

\Pi(\rho):\quad \forall q\,\Bigl(r(q)\le\rho\to\forall\sigma\,\exists n\le\beta(\rho)\ \ \operatorname{Iter}\bigl(\operatorname{Cons}(\operatorname{Req}(q),\sigma),n\bigr) =\operatorname{Cons}\bigl(\operatorname{Val}(\operatorname{Eval}(q)),\sigma\bigr)\Bigr)

まず、 $m(q)=0$ を満たす $q$ については階数によらず結論が成り立つことを示す。上の第一の等式により、 $n:=1$ において状態は $\operatorname{Cons}(\operatorname{Val}(C(q,0)),\sigma)$ である。 $\sigma:=0$ と取ると、 $1\le N_K(r(q))$ と補題 1.1 (5)の乗法の単調性により $1\le3N_K(r(q))$ であり、停止状態が保たれるので、 $R\bigl(q,3N_K(r(q))\bigr)=\operatorname{Cons}(\operatorname{Val}(C(q,0)),0)$ 、すなわち $\operatorname{Eval}(q)=C(q,0)$ である。従って任意の $\sigma$ について $\Pi$ の結論の等式が成り立つ。 $S\beta(\rho)=2N_K(\rho)$ と $1\le N_K(\rho)$ から $1\le\beta(\rho)$ である。とくに $\rho=0$ では、仮定 $r(d(q,j))<r(q)$ により $m(q)=0$ でなければならないので、 $\Pi(0)$ が従う。

$\Pi(\rho)$ を仮定して $\Pi(S\rho)$ を示す。 $r(q)\le S\rho$ とする。 $m(q)=0$ の場合は上で扱った。 $0<m(q)$ とする。本項が仮定した $\forall q\,m(q)\le K$ を用いると $0<m(q)\le K$ であるから $0<K$ であり、上に示した三つから

\beta(\rho)<S\beta(\rho)=2N_K(\rho)\le K\times\bigl(2N_K(\rho)\bigr)<\beta(S\rho)

が成り立つ。従って $r(q)\le\rho$ の場合は、 $\Pi(\rho)$ の結論がそのまま $\Pi(S\rho)$ の結論を与える。以下では $r(q)=S\rho$ とする。 $\operatorname{Hist}$ を用い、 $j$ に関する内側の $PA$ の帰納法により、 $1\le j\le m(q)$ を満たす各 $j$ について、

\operatorname{Iter}\bigl(\operatorname{Cons}(\operatorname{Req}(q),\sigma),n_j\bigr) =\operatorname{Cons}\Bigl(\operatorname{Val}\bigl(\operatorname{Eval}(d(q,j'))\bigr), \operatorname{Cons}\bigl(\operatorname{Frame}(q,j,\operatorname{Hist}(q,j')),\sigma\bigr)\Bigr), \qquad n_j\le j\times(S\beta(\rho))

を満たす $n_j$ が存在することを示す。ここで $j'$ は $Sj'=j$ を満たす数である。 $j=1$ では、第二の等式で一段進めた後、 $r(d(q,0))\le\rho$ に $\Pi(\rho)$ を適用する。 $j$ から $Sj$ へ進む段（ $Sj\le m(q)$ ）では、第三の等式で一段進め、 $\operatorname{Cons}(\operatorname{Eval}(d(q,j')),\operatorname{Hist}(q,j'))=\operatorname{Hist}(q,j)$ を用いてから、 $r(d(q,j))\le\rho$ に $\Pi(\rho)$ を適用する。

$j=m(q)$ の状態へ第四の等式を一段適用すると、 $\operatorname{Cons}\bigl(\operatorname{Val}(C(q,\operatorname{Hist}(q,m(q)))),\sigma\bigr)$ に達する。この状態に達するまでの遷移回数 $n$ は $m(q)\times(S\beta(\rho))+1$ 以下であり、ふたたび本項が仮定した $\forall q\,m(q)\le K$ と、上に示した $S\beta(\rho)=2N_K(\rho)$ および $\beta(S\rho)=S\bigl(K\times(2N_K(\rho))\bigr)$ から

m(q)\times(S\beta(\rho))+1\le K\times\bigl(2N_K(\rho)\bigr)+1=\beta(S\rho)

である。いま $r(q)=S\rho$ であり、 $\beta(S\rho)\le3N_K(S\rho)$ であるから、 $n\le3N_K(r(q))$ である。 $\sigma:=0$ と取り、停止状態が保たれることを用いると $R\bigl(q,3N_K(r(q))\bigr)=\operatorname{Cons}\bigl(\operatorname{Val}(C(q,\operatorname{Hist}(q,m(q)))),0\bigr)$ 、すなわち $\operatorname{Eval}(q)=C(q,\operatorname{Hist}(q,m(q)))$ である。従って $\Pi(S\rho)$ と求める方程式の双方を得る。

帰納法により $\forall\rho\,\Pi(\rho)$ を得た後、 $0<m(q)$ を満たす任意の $q$ について求める方程式を得る。実際、仮定 $r(d(q,0))<r(q)$ により $0<r(q)$ であるから $r(q)=S\rho$ を満たす $\rho$ が存在し、この $\rho$ について $\Pi(\rho)$ から上と同じ議論を行えばよい。 $m(q)=0$ の場合は最初の段で示した。▨

注意 6.6 (PA 内の上界と上流の数え上げの対応). 上の証明で $\Pi(\rho)$ の帰納法が与える遷移回数の上界 $\beta(\rho)$ が§E16.17 補題 3.2の固定した上界 $3N_K(r(q))$ に収まることは、上で $\beta(\rho)\le3N_K(\rho)$ として示した。この不等式は $K$ の値に依存しない。

上流の上界は、要求木の各節点が $\operatorname{Req}$ として一度だけ展開され、各辺が子の値を親の $\operatorname{Frame}$ へ戻すときに一度だけ処理されるという数え上げによる。要求木の節点数を $v$ と書くと辺数は $v-1$ であるから、停止までの遷移回数は $v+(v-1)=2v-1$ である。この勘定も $K$ に依存しない。本記事が置いた $\beta(\rho)=\bigl(2N_K(\rho)\bigr)\mathbin{\dot-}1$ は、この式の $v$ を階数 $\rho$ の要求木の節点数の上界 $N_K(\rho)$ で置き換えたものであり、 $PA$ の内部の帰納法が段ごとに同じ勘定を再現する形になっている。

上界をこれより粗く、たとえば $(K+1)N_K(\rho)$ と取ると、 $3N_K(\rho)$ に収まるのは $K\le2$ の場合に限られ、補題 6.5 (2)を適用することができる $K$ に制限が付く。すなわち、そのような制限は上界の取り方の副産物であって、 $PA$ の内部の議論に固有の障害ではない。

$K$ の値そのものに制限が付かないことと、補題 6.5 (2)が $PA\vdash\forall q\,m(q)\le K$ を仮定することとは別の事柄である。後者は、上の数え上げを $PA$ の内部で行うために要る仮定であり、これを落とすと、 $\mathbb N$ では $m(q)\le K$ を満たすが $PA$ がそれを証明しないような $m$ について、非標準の要求で結論の等式が立たない。なお、本記事および上流の記事が現に用いる有限分岐コース再帰はすべて $K=2$ であり、そこでの $m$ は構成子タグによる有限の場合分けであるから、 $PA$ は $\forall q\,m(q)\le SS0$ を証明する。

補題 6.7.§E16.17 定義 4.1の $\operatorname{Len}$ 、 $\operatorname{Entry}$ 、 $\operatorname{Concat}$ を原始再帰全関数として書く。 $PA$ は、これらの値が補題 5.2の $\operatorname{Len}(s)$ 、 $\operatorname{Entry}(s,i)$ 、 $\operatorname{Concat}(s,t)$ に等しいことを証明する。

証明.§E16.17 定理 4.2は、 $\operatorname{Len}$ を $D(s):=\operatorname{Tail}(s)$ による有界コース再帰として構成している。補題 4.1 (5)と補題 4.1 (6)により $PA$ は $0<s\to\operatorname{Tail}(s)<s$ を証明するので、補題 6.5 (1)の仮定が満たされ、 $PA$ は

\operatorname{Len}(0)=0, \qquad 0<s\to\operatorname{Len}(s)=S\operatorname{Len}(\operatorname{Tail}(s))

を証明する。補題 5.2 (1)と補題 5.2 (3)により、API 側の長さも同じ二つの等式を満たす。補題 1.2を「二つの値が異なる最小の $s$ 」へ適用すると、 $s=0$ では両者が $0$ であり、 $0<s$ では $\operatorname{Tail}(s)<s$ における一致から $s$ における一致が従うので、そのような $s$ は存在しない。よって両者は一致する。

$\operatorname{Entry}$ は補題 6.4 (4)で扱った $E$ そのものである。

$\operatorname{Concat}$ は、 $t$ をパラメータとする第1引数についての有界コース再帰

C(t,0)=t, \qquad 0<s\to C(t,s)=\operatorname{Cons}\bigl(\operatorname{Head}(s),C(t,\operatorname{Tail}(s))\bigr)

である。同じく補題 6.5 (1)により $PA$ はこの二式を証明する。補題 5.2 (5)により、API 側の連結も同じ二式を満たす。再び最小数原理を用いて一致を得る。▨

7 7. 構文符号を PA の内部で扱う

捕獲回避代入は、束縛変数の改名を記録する環境を先頭から走査する。この走査 $\operatorname{Look}$ の定義列は§E16.18 定義 3.2が固定しており、その定義方程式が $PA$ の定理であることは、補題 6.5 (1)が与える。代入についての以下の主張は、この定義方程式から次の補題として取り出した法則だけを用いる。

補題 7.1.§E16.18 定義 3.2の $\operatorname{Look}$ を記法の記法で書く。有限列 $E$ のすべての成分が $\operatorname{pair}(k,k)$ の形であることを表す $L_A$ 論理式を

\Delta(E):\!\!\Longleftrightarrow \forall l<\operatorname{Len}(E)\,\exists k\le E\, \bigl(\operatorname{Entry}(E,l)=\operatorname{pair}(k,k)\bigr)

と定める。有界存在量化の上界を $E$ に取ることができる理由は次のとおりである。 $l<\operatorname{Len}(E)$ とし、 $E$ の第 $l$ 反復尾を $u$ とする。補題 5.2 (2)により $\operatorname{Entry}(E,l)$ は $u$ の先頭であり、補題 5.2 (1)と補題 5.1 (5)により $u\ne0$ である。補題 5.1 (3)により $u\le E$ であり、補題 5.2 (3)により $u=\operatorname{Cons}(\operatorname{Head}(u),\operatorname{Tail}(u))$ であるから、補題 4.1 (5)により $\operatorname{Head}(u)<u\le E$ である。すなわち $E$ の各成分は $E$ 以下である。さらに補題 4.1 (2)により $k\le\operatorname{pair}(k,k)$ であるから、成分が $\operatorname{pair}(k,k)$ の形であるときその $k$ は $E$ 以下である。 $PA$ は次を証明する。

定義方程式。 $\operatorname{Look}(0,i)=0$ である。また $0<E$ のとき、 $\operatorname{left}(\operatorname{Head}(E))=i$ ならば $\operatorname{Look}(E,i)=S\operatorname{right}(\operatorname{Head}(E))$ であり、 $\operatorname{left}(\operatorname{Head}(E))\ne i$ ならば $\operatorname{Look}(E,i)=\operatorname{Look}(\operatorname{Tail}(E),i)$ である。
先頭追加。 $E':=\operatorname{Cons}(\operatorname{pair}(i',j),E)$ と置く。 $i'=i$ ならば $\operatorname{Look}(E',i)=Sj$ であり、とくに $\operatorname{Look}(E',i)\ne0$ である。 $i'\ne i$ ならば $\operatorname{Look}(E',i)=\operatorname{Look}(E,i)$ である。
$\Delta$ の保存。 $\Delta(0)$ が成り立ち、 $\Delta(E)$ ならば $\Delta\bigl(\operatorname{Cons}(\operatorname{pair}(k,k),E)\bigr)$ と $\Delta(\operatorname{Tail}(E))$ が成り立つ。
$\Delta$ の下での対応先。 $\Delta(E)$ かつ $\operatorname{Look}(E,i)\ne0$ ならば $\operatorname{Look}(E,i)=Si$ である。すなわち、 $\Delta(E)$ の下で対応先が存在するときの対応先は $i$ 自身である。

証明.(1)を示す。補題 4.1 (5)と補題 4.1 (6)により $PA$ は $0<s\to\operatorname{Tail}(s)<s$ を証明するので、補題 6.5 (1)の仮定が減少量 $D(E)=\operatorname{Tail}(E)$ について満たされる。再帰引数を第1引数に置いたことは射影との合成による引数の入れ替えであるから、補題 6.5 (1)をそのまま適用することができ、 $PA$ は§E16.18 定義 3.2の二つの定義方程式を証明する。親節に現れる $\operatorname{Head}$ 、 $\operatorname{left}$ 、 $\operatorname{right}$ 、等号判定、および有限の場合分けの値については、補題 6.1と補題 6.4により、 $PA$ はそれらの定義方程式を証明する。

(2)を示す。補題 4.1 (5)と補題 4.1 (6)により $0<E'$ 、 $\operatorname{Head}(E')=\operatorname{pair}(i',j)$ 、 $\operatorname{Tail}(E')=E$ である。補題 6.4 (2)により、 $PA$ は $\operatorname{left}(\operatorname{pair}(a,b))=a$ と $\operatorname{right}(\operatorname{pair}(a,b))=b$ を証明する。従って(1)の場合分けは $i'=i$ であるかどうかで決まり、 $i'=i$ のとき値は $Sj$ 、 $i'\ne i$ のとき値は $\operatorname{Look}(E,i)$ である。(Q1) により $Sj\ne0$ である。

(3)を示す。補題 5.2 (1)により $\operatorname{Len}(0)=0$ であるから、 $\Delta(0)$ の有界全称量化は空虚に成り立つ。 $E^{+}:=\operatorname{Cons}(\operatorname{pair}(k,k),E)$ と置く。補題 5.2 (3)により $\operatorname{Len}(E^{+})=S\operatorname{Len}(E)$ 、 $\operatorname{Entry}(E^{+},0)=\operatorname{pair}(k,k)$ 、 $\operatorname{Entry}(E^{+},Sl)=\operatorname{Entry}(E,l)$ である。第 $0$ 成分については、上で述べたとおり $k\le\operatorname{pair}(k,k)\le E^{+}$ である。第 $Sl$ 成分については、 $\Delta(E)$ が与える $k'\le E$ を取り、補題 4.1 (5)により $E<E^{+}$ であるから $k'\le E^{+}$ である。よって $\Delta(E^{+})$ が成り立つ。 $\Delta(\operatorname{Tail}(E))$ については、 $E=0$ のとき $\operatorname{Tail}(0)=0$ であり、 $0<E$ のとき補題 5.2 (3)により $\operatorname{Tail}(E)$ の第 $l$ 成分が $E$ の第 $Sl$ 成分であるから、 $\Delta(E)$ により $\operatorname{pair}(k,k)$ の形であり、上界については上で述べたとおり $k\le\operatorname{Entry}(\operatorname{Tail}(E),l)\le\operatorname{Tail}(E)$ である。

(4)を示す。補題 1.2を、 $\Delta(E)$ と $\operatorname{Look}(E,i)\ne0$ と $\operatorname{Look}(E,i)\ne Si$ の三つをすべて満たす $E$ の最小値へ適用し、矛盾を導く。 $E=0$ は(1)により $\operatorname{Look}(0,i)=0$ を与えるので、三つを満たさない。 $0<E$ とする。補題 5.2 (1)により $0<\operatorname{Len}(E)$ であり、補題 5.2 (3)により $\operatorname{Entry}(E,0)=\operatorname{Head}(E)$ であるから、 $\Delta(E)$ を $l:=0$ について用いると $\operatorname{Head}(E)=\operatorname{pair}(k,k)$ を満たす $k$ が存在する。(2)で示した $\operatorname{left}$ と $\operatorname{right}$ の値により、 $k=i$ ならば(1)が $\operatorname{Look}(E,i)=Sk=Si$ を与えるので、 $E$ は三つを満たさない。 $k\ne i$ ならば(1)により $\operatorname{Look}(E,i)=\operatorname{Look}(\operatorname{Tail}(E),i)$ である。(3)により $\Delta(\operatorname{Tail}(E))$ が成り立つので、 $\operatorname{Tail}(E)$ も三つをすべて満たす。補題 4.1 (5)と補題 4.1 (6)により $\operatorname{Tail}(E)<E$ であるから、これは $E$ の最小性に反する。▨

補題 7.2. $PA$ は次を証明する。

§E16.18 定義 1.1の各構成子について、その値の直下成分は値より小さい。すなわち、§E16.18 補題 1.2 (1)の $PA$ 内の版が成り立つ。§E16.18 補題 1.2 (2)にあたる主張、すなわち入れ子の任意の深さに現れる自由な変数添字の上界は、本項からは従わない。この上界は補題 7.3が別に与える。
§E16.18 定義 2.1の $\operatorname{Term}$ 、 $\operatorname{Formula}$ 、 $\operatorname{Free}$ について、定義に列挙した各場合の同値が成り立つ。
§E16.18 定義 4.2が用いる $\operatorname{FreeFor}$ について、原子式、否定、含意の場合の同値と、量化子の場合の同値
$\operatorname{FreeFor}(t,i,\operatorname{AllRaw}(j,\psi)) \leftrightarrow \begin{cases} \text{真}&j=i,\\ \operatorname{FreeFor}(t,i,\psi)\land \bigl(\neg\operatorname{Free}(\psi,i)\lor\neg\operatorname{Free}(t,j)\bigr)&j\ne i \end{cases}$
が成り立つ。量化子の場合の第2連言は選言であり、 $\neg\operatorname{Free}(t,j)$ だけを要求する形ではない。
§E16.18 定義 3.3の $\operatorname{WalkTerm}$ と $\operatorname{WalkFormula}$ について、定義に列挙した各場合の等式が成り立つ。従って $\operatorname{SubTermCode}$ と $\operatorname{Sub}$ の場合分けも成り立つ。
§E16.18 定義 4.2 (2)が表す代入例の条件について、 $i,t,a,b\le y$ の有界探索と、 $\operatorname{FreeFor}(t,i,a)$ および $b=\operatorname{SubTermCode}(a,i,t)$ という各構成要素の値による条件との同値が成り立つ。

証明.(1)を示す。各構成子は§E16.17 定義 2.1の右入れ子の Cons 符号である。補題 6.4 (1)により、原始再帰関数として書いた $\operatorname{Cons}$ の値は $\operatorname{Cons}_Q$ が定める値に等しく、補題 4.1 (5)により $\operatorname{Cons}(a,t)$ は $a$ と $t$ の双方より大きい。外側のタグを含む Cons について同じ評価を繰り返せば、直下の項符号・論理式符号・変数添字がいずれも全体より小さいことを得る。ここで繰り返す回数は構成子ごとに定まる標準自然数であり、入れ子の深さについての帰納法は用いていない。

(2)と(3)を示す。§E16.18 定理 2.2は $\operatorname{Term}$ 、 $\operatorname{Formula}$ 、 $\operatorname{Free}$ を、階数を第1引数、最大子数を $K=2$ とする有限分岐コース再帰の値として構成し、 $\operatorname{FreeFor}$ も同じ形の還元で構成している。(1)により $PA$ は階数の減少 $r(d(q,j))<r(q)$ を証明する。要求の生成、子の割り当て、および親の結合関数は $\operatorname{Len}$ 、 $\operatorname{Entry}$ 、等号、有限の場合分けの合成であるから、補題 6.1と補題 6.7により $PA$ はそれらの定義方程式を証明する。子の個数を返す $m$ も同じ合成であり、その値は構成子タグによる有限の場合分けで $0$ 、 $S0$ 、 $SS0$ のいずれかに固定されている。どのタグにも一致しない要求へ与える既定値も $0$ である。従って場合分けを尽くすと、 $PA$ は帰納法を用いずに $\forall q\ m(q)\le SS0$ を証明する。これで補題 6.5 (2)が課す二つの仮定がともに満たされるので、補題 6.5 (2)を $K=2$ について適用することができ、各要求について

\operatorname{Eval}(q)=C\bigl(q,\operatorname{Hist}(q,m(q))\bigr)

を得る。この等式に、各構成子に対する $m,d,C$ の定義を代入すると、表示した各場合の同値が得られる。とくに $\operatorname{FreeFor}$ の量化子節では、親の結合関数が $\operatorname{FreeFor}(t,i,\psi)$ の値と、 $\neg\operatorname{Free}(\psi,i)$ または $\neg\operatorname{Free}(t,j)$ という選言との連言を取るので、表示した形になる。

(4)も同様である。§E16.18 定理 3.4は $\operatorname{WalkTerm}$ と $\operatorname{WalkFormula}$ を、階数を第1引数、 $K=2$ とする有限分岐コース再帰へ移している。量化子の場合に子へ渡す環境が $E$ から $E'=\operatorname{Cons}(\operatorname{pair}(i,j),E)$ へ変わるが、階数は元の真部分符号 $z<y$ であるから減少条件は保たれる。新鮮変数 $j=1+y+t+E+v+i$ の計算、環境の走査 $\operatorname{Look}$ 、 $\operatorname{Free}$ の判定、および $i\ne v$ の等号判定はいずれも原始再帰的であり、 $\operatorname{Look}$ の定義方程式は補題 7.1 (1)が $PA$ の定理として与える。改名を発動させる三条件はこれらの合成であるから、量化子の場合の等式は $\operatorname{Look}(E,v)=0$ 、 $i\ne v$ 、 $\operatorname{Free}(t,i)$ 、 $\operatorname{Free}(z,v)$ の四つの判定による場合分けとして $PA$ の内部で読むことができる。子の個数についても、 $m$ が構成子タグによる有限の場合分けで $0$ 、 $S0$ 、 $SS0$ のいずれかを返すので、 $PA$ は同じく $\forall q\ m(q)\le SS0$ を証明する。従って同じ適用によって各場合の等式を得る。 $\operatorname{SubTermCode}$ と $\operatorname{Sub}$ は、これらと $\operatorname{Term}$ 、 $\operatorname{Formula}$ 、 $\operatorname{Num}$ の合成と有限の場合分けである。

(5)を示す。§E16.18 定義 4.2 (2)が表す代入例の条件は、構成子の等式、 $\operatorname{Term}$ 、 $\operatorname{FreeFor}$ 、 $\operatorname{SubTermCode}$ 、および $i,t,a,b\le y$ の有界探索から作られる。有界探索については補題 6.2、各構成要素については(2)から(4)までを用いると、 $PA$ はこの判定と、表示した条件との同値を証明する。本記事が扱うのは代入可能性の判定にあたるこの部分である。論理公理例の判定 $\operatorname{LogAx}$ 全体について、その値と定義に列挙した場合分けとの同値を $PA$ の内部で証明することは、本単元では扱わない。下流で必要になるのは、 $\operatorname{LogAx}$ の値が $PA$ の内部で存在して一意であることと、個別に与えた公理例について $\operatorname{LogAx}$ の成立を $PA$ が証明することの二つだけである。前者は補題 6.1 (1)が与える。後者は二段を要する。本項が与える代入可能性の判定で§E16.18 定義 4.2 (2)の四条件を確かめ、そのうえで§E16.18 定義 4.2 (1)から§E16.18 定義 4.2 (6)までの有限選言へ移る。後段の一手は補題 6.1 (2)が与える固定した定義列の方程式による。 $\operatorname{LogAx}$ の原始再帰的定義列は§E16.18 定義 4.4が一つに固定しており、その最終段は§E16.18 定義 4.2 (1)から§E16.18 定義 4.2 (6)までの特性関数の有限選言であるから、補題 6.1 (2)をこの最終段へ適用することができる。▨

補題 7.3. $PA$ は

\forall e\,\forall j\,\bigl(\operatorname{Free}(e,j)\to j<e\bigr)

を証明する。

証明.補題 7.2 (1)が与えるのは直下の一段の減少だけであり、入れ子の任意の深さに現れる添字については何も述べていない。そこで別の帰納法を行う。補題 1.2を論理式 $\exists j\,\bigl(\operatorname{Free}(e,j)\land e\le j\bigr)$ へ適用し、これを満たす最小の $e$ を取って矛盾を導く。 $\operatorname{Free}(e,j)$ かつ $e\le j$ を満たす $j$ を固定する。

補題 7.2 (2)により、 $PA$ は $\operatorname{Free}$ について、 $e$ のタグに応じた各場合の同値を証明する。 $e=\operatorname{Var}(k)$ の場合、 $\operatorname{Free}(e,j)$ は $j=k$ と同値であり、補題 7.2 (1)により $k<e$ であるから $j<e$ となって $e\le j$ に反する。 $e=\operatorname{Zero}$ の場合と、 $e$ がどの構成子の値でもない場合、 $\operatorname{Free}(e,j)$ は偽である。 $e$ が $\operatorname{Succ}$ 、 $\operatorname{Add}$ 、 $\operatorname{Mul}$ 、 $\operatorname{Eq}$ 、 $\operatorname{NegRaw}$ 、 $\operatorname{ImpRaw}$ の値である場合、 $\operatorname{Free}(e,j)$ は直下の対象についての $\operatorname{Free}$ の選言と同値であるから、 $\operatorname{Free}(u,j)$ を満たす直下の対象 $u$ が存在する。補題 7.2 (1)により $u<e$ であるから、 $e$ の最小性により $j<u$ であり、 $j<u<e$ が $e\le j$ に反する。 $e=\operatorname{AllRaw}(k,z)$ の場合、 $\operatorname{Free}(e,j)$ は $j\ne k$ かつ $\operatorname{Free}(z,j)$ と同値であり、 $z<e$ であるから同じく $j<z<e$ となって矛盾する。

いずれの場合も矛盾するので、 $\operatorname{Free}(e,j)$ かつ $e\le j$ を満たす $e,j$ は存在しない。▨

補題 7.4. 符号 $e$ が閉項符号であるとは、 $\operatorname{Term}(e)$ が成り立ち、かつ $i\le e$ を満たすすべての $i$ について $\neg\operatorname{Free}(e,i)$ が成り立つことをいう。補題 7.3により、 $e$ に自由に現れる変数の添字は $e$ より小さいので、この有界全称量化はすべての候補を調べている。すなわち $PA$ は、 $e$ が閉項符号であることと $\operatorname{Term}(e)\land\forall i\,\neg\operatorname{Free}(e,i)$ とが同値であることを証明する。以下ではこの同値を断らずに用いる。 $PA$ は次を証明する。

$\forall x\ \operatorname{Num}(Sx)=\operatorname{Succ}(\operatorname{Num}(x))$ 。
任意の $x$ について $\operatorname{Num}(x)$ は閉項符号である。
閉項符号は任意の論理式符号の任意の変数へ自由に代入可能である。すなわち
$\forall e\,\forall a\,\forall i\, \bigl(e\ \text{が閉項符号}\ \land\ \operatorname{Formula}(a) \to\operatorname{FreeFor}(e,i,a)\bigr)$
である。ここで $\operatorname{FreeFor}$ の引数の順序は項、変数添字、論理式である。
$e,e'$ が閉項符号ならば $\operatorname{Succ}(e)$ 、 $\operatorname{Add}(e,e')$ 、 $\operatorname{Mul}(e,e')$ も閉項符号である。
$\operatorname{Term}(t)$ 、 $\operatorname{Formula}(a)$ 、 $\neg\operatorname{Free}(a,i)$ ならば $\operatorname{SubTermCode}(a,i,t)=a$ である。
$\operatorname{Term}(t)$ 、 $\operatorname{Formula}(a)$ 、 $\operatorname{Free}(a,i)$ ならば $t\le\operatorname{SubTermCode}(a,i,t)$ である。
$\operatorname{Term}(t)$ かつ $\operatorname{Formula}(a)$ ならば $\operatorname{Formula}\bigl(\operatorname{SubTermCode}(a,i,t)\bigr)$ である。さらに $\operatorname{Free}\bigl(\operatorname{SubTermCode}(a,i,t),k\bigr)$ ならば、 $k\ne i$ かつ $\operatorname{Free}(a,k)$ であるか、または $\operatorname{Free}(a,i)$ かつ $\operatorname{Free}(t,k)$ である。

証明.(1)は§E16.18 定義 3.1が与える通常の原始再帰であるから、補題 6.1 (2)による。

(2)は $x$ に関する $PA$ の帰納法による。 $x=0$ では $\operatorname{Num}(0)=\operatorname{Zero}$ であり、補題 7.2 (2)により $\operatorname{Term}(\operatorname{Zero})$ が成り立ち、 $\operatorname{Free}(\operatorname{Zero},i)$ はどの $i$ についても偽である。 $x$ から $Sx$ へ進む段では、(1)により $\operatorname{Num}(Sx)=\operatorname{Succ}(\operatorname{Num}(x))$ であり、補題 7.2 (2)の $\operatorname{Term}(\operatorname{Succ}(u))\leftrightarrow\operatorname{Term}(u)$ と $\operatorname{Free}(\operatorname{Succ}(u),i)\leftrightarrow\operatorname{Free}(u,i)$ を用いる。

(3)を示す。論理式符号 $a$ に関する $PA$ の強い帰納法、すなわち補題 1.2を反例の最小値へ適用する。補題 7.2 (3)により、 $\operatorname{FreeFor}(e,i,a)$ は $a$ の構成に関する再帰で定まる。原子式では条件が空である。 $\neg$ と $\to$ では真部分符号へ再帰し、いずれも $a$ より小さいので最小性に反する反例が無い。 $\operatorname{AllRaw}(j,b)$ では、 $j=i$ ならば条件が空であり、 $j\ne i$ ならば

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

を要求する。 $e$ が閉項符号であれば、補題 7.3により $j$ の大きさによらず $\neg\operatorname{Free}(e,j)$ が成り立つので、連言の第2成分である選言は右側で満たされる。連言の第1成分は $b<a$ に対する最小性から従う。ここで用いたのは選言であり、 $\neg\operatorname{Free}(b,i)$ と $\neg\operatorname{Free}(e,j)$ の双方を要求してはいない。

(4)を示す。補題 7.2 (2)が与える $\operatorname{Term}$ の節により、 $\operatorname{Term}(e)$ と $\operatorname{Term}(e')$ から $\operatorname{Term}(\operatorname{Succ}(e))$ 、 $\operatorname{Term}(\operatorname{Add}(e,e'))$ 、 $\operatorname{Term}(\operatorname{Mul}(e,e'))$ が従う。 $\operatorname{Free}$ の節は直下の対象についての選言であるから、 $\operatorname{Free}(\operatorname{Succ}(e),i)$ は $\operatorname{Free}(e,i)$ と同値であり、二項構成子でも同様である。 $e$ と $e'$ が閉項符号であれば、上で述べた同値により $i$ の大きさによらず $\neg\operatorname{Free}(e,i)$ かつ $\neg\operatorname{Free}(e',i)$ であるから、構成した符号についても $i$ の大きさによらず $\neg\operatorname{Free}$ が成り立ち、再び同じ同値により閉項符号である。 $\operatorname{Succ}(e)$ では有界全称量化の範囲が $i\le e$ から $i\le\operatorname{Succ}(e)$ へ広がるが、補題 7.3を経由して量化の範囲を外したので、この差は問題にならない。

(5)から(7)までを示す。いずれも補題 7.2 (4)が与える $\operatorname{WalkTerm}$ と $\operatorname{WalkFormula}$ の各場合の等式だけを用い、符号に関する強い帰納法、すなわち補題 1.2を反例の最小値へ適用する形の議論を行う。補助環境 $E$ は帰納法の主張の中で全称量化する。 $\operatorname{Walk}(y,v,t,E)$ は、 $y$ が項符号のとき $\operatorname{WalkTerm}(y,v,t,E)$ 、論理式符号のとき $\operatorname{WalkFormula}(y,v,t,E)$ を表すものとする。以下では代入対象の変数添字を $v$ 、代入する項の符号を $t$ と書き、最後に $v:=i$ と取って(5)から(7)までを得る。§E16.18 定義 3.3の改名の三条件は、 $\operatorname{Look}(E,v)=0$ 、 $i'\ne v$ 、および「 $v_{i'}$ が $t$ に自由に現れ、かつ $v_v$ が本体に自由に現れる」である。

(5)を示す。次の主張 $\Sigma(y)$ を、 $y$ に関する強い帰納法で示す。

\Sigma(y):\quad \forall E\,\Bigl( \bigl(\operatorname{Term}(y)\lor\operatorname{Formula}(y)\bigr)\land \Delta(E)\land \bigl(\operatorname{Look}(E,v)\ne0\lor\neg\operatorname{Free}(y,v)\bigr) \to\operatorname{Walk}(y,v,t,E)=y\Bigr)

ここで $\Delta(E)$ は補題 7.1が定めた論理式であり、 $E$ のすべての成分が $\operatorname{pair}(k,k)$ の形であることを表す。整形式であるという連言を置いたのは、どの構成子の値でもない $y$ に対して $\operatorname{Walk}$ が $0$ を返すからである。補題 7.2 (2)により、整形式な符号の直下の対象はふたたび整形式であるから、この連言は帰納法の各段で引き継がれる。

$y=\operatorname{Var}(i')$ の場合を見る。 $\operatorname{Look}(E,i')\ne0$ ならば、補題 7.1 (4)により $\operatorname{Look}(E,i')=Si'$ 、すなわち対応先は $i'$ 自身であるから、返る値は $\operatorname{Var}(i')$ である。 $\operatorname{Look}(E,i')=0$ の場合、 $i'=v$ とすると $\operatorname{Free}(y,v)$ かつ $\operatorname{Look}(E,v)=0$ となって前件に反するので $i'\ne v$ であり、返る値はやはり $\operatorname{Var}(i')$ である。 $y=\operatorname{Zero}$ では値が $\operatorname{Zero}$ である。 $\operatorname{Succ}$ 、 $\operatorname{Add}$ 、 $\operatorname{Mul}$ 、 $\operatorname{Eq}$ 、 $\operatorname{NegRaw}$ 、 $\operatorname{ImpRaw}$ の場合、 $\operatorname{Free}(y,v)$ は直下の対象についての選言と同値であるから、前件は各直下の対象へそのまま引き継がれる。直下の対象は補題 7.2 (1)により $y$ より小さいので、最小性により値が変わらず、親は同じ構成子で戻すので値は $y$ である。

$y=\operatorname{AllRaw}(i',z)$ の場合を見る。前件により $\operatorname{Look}(E,v)\ne0$ であるか、または $\neg\operatorname{Free}(y,v)$ 、すなわち $i'=v$ または $\neg\operatorname{Free}(z,v)$ である。第一の場合は改名の第1条件が、 $i'=v$ の場合は第2条件が、 $\neg\operatorname{Free}(z,v)$ の場合は第3条件が破れるので、いずれにせよ改名は発動せず $j=i'$ である。従って子へ渡る環境は $E'=\operatorname{Cons}(\operatorname{pair}(i',i'),E)$ であり、補題 7.1 (3)により $\Delta(E')$ が成り立つ。また補題 7.1 (2)により、 $i'=v$ ならば $\operatorname{Look}(E',v)\ne0$ であり、 $i'\ne v$ ならば $\operatorname{Look}(E',v)=\operatorname{Look}(E,v)$ であるから、いずれの場合も前件が $z$ と $E'$ について成り立つ。 $z<y$ であるから最小性により $\operatorname{Walk}(z,v,t,E')=z$ であり、親は $\operatorname{AllRaw}(i',z)=y$ を返す。以上のどの場合にも反例が無いので $\Sigma(y)$ が成り立つ。

補題 7.1 (3)により $\Delta(0)$ が成り立ち、補題 7.1 (1)により $\operatorname{Look}(0,v)=0$ である。 $\operatorname{Formula}(a)$ と $\operatorname{Term}(t)$ により $\operatorname{SubTermCode}(a,i,t)=\operatorname{WalkFormula}(a,i,t,0)$ であるから、 $\neg\operatorname{Free}(a,i)$ のとき $\Sigma(a)$ から $\operatorname{SubTermCode}(a,i,t)=a$ を得る。

改名の第2条件（ $i'\ne v$ ）と第1条件（ $\operatorname{Look}(E,v)=0$ ）は、この主張のために必要である。これらを課さない改名条件では、 $v_v$ が束縛されていて代入が起こらない位置でも改名が発動し、結果が $a$ と一致しない。

第2条件の必要性は、最外の量化子だけで現れる。 $i=0$ 、 $t=\operatorname{Var}(0)$ 、 $a=\operatorname{AllRaw}\bigl(0,\operatorname{Eq}(\operatorname{Var}(0),\operatorname{Var}(0))\bigr)$ では $\neg\operatorname{Free}(a,0)$ であるが、第2条件が無ければ最外の量化子で $i'=0=v$ のまま改名が発動する。

第1条件の必要性は、入れ子になった量化子でしか現れない。 $i=0$ 、 $t=\operatorname{Var}(1)$ 、 $a=\operatorname{AllRaw}\bigl(0,\operatorname{AllRaw}(1,\operatorname{Eq}(\operatorname{Var}(0),\operatorname{Var}(1)))\bigr)$ を取る。 $v_0$ は最外の量化子に束縛されているので $\neg\operatorname{Free}(a,0)$ であり、(5)は $\operatorname{SubTermCode}(a,0,t)=a$ を要求する。最外の量化子では $i'=0=v$ により第2条件が破れるので改名は発動せず、子へ渡る環境は $E'=\operatorname{Cons}(\operatorname{pair}(0,0),0)$ である。内側の量化子では $i'=1\ne v$ であり、 $v_1$ は $t$ に自由に現れ、 $v_0$ は $\operatorname{Eq}(\operatorname{Var}(0),\operatorname{Var}(1))$ に自由に現れるので、第2条件と第3条件はどちらも破れない。第1条件だけが $\operatorname{Look}(E',0)\ne0$ によって破れており、これを課さなければ内側の量化子で改名が発動して、結果は $\operatorname{AllRaw}(0,\operatorname{AllRaw}(j,\cdots))$ （ $j\ne1$ ）となり $a$ と一致しない。

(6)を示す。次の主張 $\Xi_0(y)$ を、 $y$ に関する強い帰納法で示す。

\Xi_0(y):\quad \forall E\,\Bigl( \bigl(\operatorname{Term}(y)\lor\operatorname{Formula}(y)\bigr)\land \operatorname{Look}(E,v)=0\land\operatorname{Free}(y,v) \to t\le\operatorname{Walk}(y,v,t,E)\Bigr)

$\Sigma(y)$ と同じく整形式であるという連言を置いたのは、どの構成子の値でもない $y$ に対して $\operatorname{Walk}$ が $0$ を返すからである。補題 7.2 (2)により、整形式な符号の直下の対象はふたたび整形式であるから、この連言は帰納法の各段で引き継がれる。

$y=\operatorname{Var}(i')$ の場合、 $\operatorname{Free}(y,v)$ は $i'=v$ を与え、 $\operatorname{Look}(E,v)=0$ であるから返る値は $t$ である。 $y=\operatorname{Zero}$ では前件が偽である。一項構成子と二項構成子の場合、 $\operatorname{Free}(y,v)$ は直下の対象についての選言と同値であるから、 $\operatorname{Free}(u,v)$ を満たす直下の対象 $u$ が存在する。補題 7.2 (1)により $u<y$ であるから、最小性により $t\le\operatorname{Walk}(u,v,t,E)$ である。親は返った値を直下成分としてもつ符号を返すので、再び補題 7.2 (1)により $\operatorname{Walk}(u,v,t,E)<\operatorname{Walk}(y,v,t,E)$ であり、 $t\le\operatorname{Walk}(y,v,t,E)$ を得る。 $y=\operatorname{AllRaw}(i',z)$ の場合、 $\operatorname{Free}(y,v)$ は $i'\ne v$ かつ $\operatorname{Free}(z,v)$ を与える。改名が発動するかどうかによらず子へ渡る環境は $E'=\operatorname{Cons}(\operatorname{pair}(i',j),E)$ であり、 $i'\ne v$ であるから、補題 7.1 (2)により $\operatorname{Look}(E',v)=\operatorname{Look}(E,v)=0$ である。 $z<y$ に最小性を用いて $t\le\operatorname{Walk}(z,v,t,E')$ を得る。親が返す符号は $\operatorname{AllRaw}\bigl(j,\operatorname{Walk}(z,v,t,E')\bigr)$ であり、補題 7.2 (1)によりこれは $\operatorname{Walk}(z,v,t,E')$ より大きい。

$E:=0$ と取ると、補題 7.1 (1)により $\operatorname{Look}(0,v)=0$ である。 $\operatorname{Formula}(a)$ と $\operatorname{Term}(t)$ により $\operatorname{SubTermCode}(a,i,t)=\operatorname{WalkFormula}(a,i,t,0)$ であることを用いると、 $\operatorname{Free}(a,i)$ のとき $t\le\operatorname{SubTermCode}(a,i,t)$ を得る。この議論では「部分符号は全体以下である」という推移的な主張を用いていない。補題 7.2 (1)が与えるのは直下の一段だけであり、その推移閉包を別に立てる代わりに、いま行った $y$ に関する帰納法を用いている。

(7)を示す。環境 $E$ が現に有効にしている改名先を表す論理式を

\operatorname{Ren}(E,k) :\!\!\Longleftrightarrow \exists k'\,\bigl(\operatorname{Look}(E,k')=Sk\bigr)

と置く。 $\operatorname{Look}$ の値が $0$ でないことは対応先が存在することを表し、そのときの対応先は $\operatorname{Look}(E,k')=Sk$ を満たす $k$ であるから、 $\operatorname{Ren}(E,k)$ は「 $E$ のもとで何らかの変数が $v_k$ へ改名される」ことを表す。次の二つの主張の連言 $\Xi_1(y)$ を、 $y$ に関する強い帰納法で示す。

\Phi(y,E):\quad \bigl(\operatorname{Term}(y)\to\operatorname{Term}(\operatorname{Walk}(y,v,t,E))\bigr) \land \bigl(\operatorname{Formula}(y)\to\operatorname{Formula}(\operatorname{Walk}(y,v,t,E))\bigr)

\Lambda(y,E):\quad \forall k\,\Bigl( \operatorname{Free}\bigl(\operatorname{Walk}(y,v,t,E),k\bigr) \to \operatorname{Ren}(E,k) \lor\bigl(\operatorname{Free}(y,k)\land k\ne v\land\operatorname{Look}(E,k)=0\bigr) \lor\bigl(\operatorname{Free}(t,k)\land\operatorname{Free}(y,v)\land\operatorname{Look}(E,v)=0\bigr)\Bigr)

\Xi_1(y):\quad \forall E\,\Bigl( \operatorname{Term}(t)\land \bigl(\operatorname{Term}(y)\lor\operatorname{Formula}(y)\bigr) \to\Phi(y,E)\land\Lambda(y,E)\Bigr)

$\Sigma(y)$ および $\Xi_0(y)$ と同じく整形式であるという連言を置いたのは、どの構成子の値でもない $y$ に対して $\operatorname{Walk}$ が $0$ を返すからである。 $\operatorname{Term}$ と $\operatorname{Formula}$ の各節はタグによって排他的であるから、以下の各場合では $\Phi(y,E)$ の二つの含意のうち一方だけが実質をもち、他方は前件が偽で空虚に成り立つ。

$y=\operatorname{Var}(i')$ の場合を見る。 $\operatorname{Look}(E,i')\ne0$ ならば、補題 7.1 (1)が与える定義方程式により、 $\operatorname{Look}(E,i')=Sj$ を満たす $j$ について値は $\operatorname{Var}(j)$ である。補題 7.2 (2)により $\operatorname{Term}(\operatorname{Var}(j))$ が成り立ち、 $\operatorname{Free}(\operatorname{Var}(j),k)$ は $k=j$ と同値である。 $\operatorname{Look}(E,i')=Sj$ であるから $\operatorname{Ren}(E,j)$ が成り立ち、第1の選言肢を得る。 $\operatorname{Look}(E,i')=0$ かつ $i'=v$ ならば値は $t$ であり、前件の $\operatorname{Term}(t)$ が $\Phi$ を与える。 $\operatorname{Free}(t,k)$ に対しては、 $\operatorname{Free}(\operatorname{Var}(v),v)$ と $\operatorname{Look}(E,v)=0$ により第3の選言肢を得る。 $\operatorname{Look}(E,i')=0$ かつ $i'\ne v$ ならば値は $\operatorname{Var}(i')$ であり、 $\operatorname{Free}$ の $\operatorname{Var}$ の節が与える $k=i'$ に対して第2の選言肢を得る。 $y=\operatorname{Zero}$ の場合、値は $\operatorname{Zero}$ であり、 $\operatorname{Term}(\operatorname{Zero})$ が成り立ち、 $\operatorname{Free}(\operatorname{Zero},k)$ はどの $k$ についても偽である。

$y$ が $\operatorname{Succ}$ 、 $\operatorname{Add}$ 、 $\operatorname{Mul}$ 、 $\operatorname{Eq}$ 、 $\operatorname{NegRaw}$ 、 $\operatorname{ImpRaw}$ の値である場合、補題 7.2 (4)により、値は同じ構成子を直下の対象の値へ適用したものである。直下の対象は補題 7.2 (1)により $y$ より小さく、補題 7.2 (2)により整形式であるから、最小性により $\Phi$ と $\Lambda$ が同じ $E$ について成り立つ。 $\operatorname{Term}$ と $\operatorname{Formula}$ の各節は直下の対象についての連言であるから $\Phi(y,E)$ を得る。 $\operatorname{Free}$ の各節は直下の対象についての選言であるから、 $\operatorname{Free}(\operatorname{Walk}(y,v,t,E),k)$ を満たす $k$ に対しては、 $\operatorname{Free}(\operatorname{Walk}(u,v,t,E),k)$ を満たす直下の対象 $u$ が存在する。 $\Lambda(u,E)$ の三つの選言肢は、 $\operatorname{Free}(u,k)\to\operatorname{Free}(y,k)$ と $\operatorname{Free}(u,v)\to\operatorname{Free}(y,v)$ によってそのまま $\Lambda(y,E)$ の三つの選言肢へ移る。

$y=\operatorname{AllRaw}(i',z)$ の場合を見る。§E16.18 定義 3.3の改名の三条件、すなわち $\operatorname{Look}(E,v)=0$ であること、 $i'\ne v$ であること、および $v_{i'}$ が $t$ に自由に現れかつ $v_v$ が $z$ に自由に現れることは、補題 7.2 (4)により $PA$ の内部での場合分けとして読むことができる。三条件がすべて成り立つときは $j=1+y+t+E+v+i'$ 、それ以外のときは $j=i'$ であり、いずれの場合も子へ渡る環境は $E'=\operatorname{Cons}(\operatorname{pair}(i',j),E)$ 、値は $\operatorname{AllRaw}\bigl(j,\operatorname{Walk}(z,v,t,E')\bigr)$ である。以下の議論は、どちらの場合であるかによらない。 $z<y$ であり、 $\operatorname{Formula}(y)$ から $\operatorname{Formula}(z)$ が従うので、最小性により $\Phi(z,E')$ と $\Lambda(z,E')$ が成り立つ。 $\operatorname{Formula}$ の $\operatorname{AllRaw}$ の節は本体についての条件だけであるから $\Phi(y,E)$ を得る。

$\Lambda(y,E)$ を示す。 $\operatorname{Free}$ の $\operatorname{AllRaw}$ の節により、 $\operatorname{Free}\bigl(\operatorname{AllRaw}(j,\operatorname{Walk}(z,v,t,E')),k\bigr)$ は $k\ne j$ かつ $\operatorname{Free}(\operatorname{Walk}(z,v,t,E'),k)$ と同値である。 $\Lambda(z,E')$ が与える三つの選言肢を順に見る。

$\operatorname{Ren}(E',k)$ の場合。 $\operatorname{Look}(E',k')=Sk$ を満たす $k'$ を取る。補題 7.1 (2)により、 $k'=i'$ ならば $\operatorname{Look}(E',k')=Sj$ であるから $k=j$ となり、 $k\ne j$ に反する。 $k'\ne i'$ ならば $\operatorname{Look}(E,k')=\operatorname{Look}(E',k')=Sk$ であるから $\operatorname{Ren}(E,k)$ が成り立つ。
$\operatorname{Free}(z,k)\land k\ne v\land\operatorname{Look}(E',k)=0$ の場合。補題 7.1 (2)により、 $k=i'$ ならば $\operatorname{Look}(E',k)=Sj$ となり (Q1) に反するので $k\ne i'$ であり、 $\operatorname{Look}(E,k)=\operatorname{Look}(E',k)=0$ である。 $\operatorname{Free}(z,k)$ と $k\ne i'$ から $\operatorname{Free}(y,k)$ が従うので、第2の選言肢を得る。
$\operatorname{Free}(t,k)\land\operatorname{Free}(z,v)\land\operatorname{Look}(E',v)=0$ の場合。同じ理由で $v\ne i'$ かつ $\operatorname{Look}(E,v)=0$ であり、 $\operatorname{Free}(z,v)$ と $v\ne i'$ から $\operatorname{Free}(y,v)$ が従うので、第3の選言肢を得る。

以上のどの場合にも反例が無いので $\Xi_1(y)$ が成り立つ。

$E:=0$ と取る。補題 7.1 (1)により $\operatorname{Look}(0,k')=0$ であり、(Q1) により $0\ne Sk$ であるから、どの $k$ についても $\operatorname{Ren}(0,k)$ は成り立たず、どの $k$ についても $\operatorname{Look}(0,k)=0$ である。 $\operatorname{Formula}(a)$ と $\operatorname{Term}(t)$ により $\operatorname{SubTermCode}(a,i,t)=\operatorname{WalkFormula}(a,i,t,0)$ であるから、 $v:=i$ 、 $y:=a$ と取ると、 $\Phi(a,0)$ が $\operatorname{Formula}\bigl(\operatorname{SubTermCode}(a,i,t)\bigr)$ を与え、 $\Lambda(a,0)$ が

\operatorname{Free}\bigl(\operatorname{SubTermCode}(a,i,t),k\bigr) \to \bigl(k\ne i\land\operatorname{Free}(a,k)\bigr) \lor\bigl(\operatorname{Free}(a,i)\land\operatorname{Free}(t,k)\bigr)

を与える。第3の選言肢に現れる $\operatorname{Free}(a,i)$ は $\operatorname{Free}(y,v)$ の $v:=i$ の場合である。▨

定義 7.5 (固定論理式への数詞代入符号). $\chi$ を、自由変数が $v_{i_1},\ldots,v_{i_k}$ に含まれる固定した $L_A$ 論理式とする。§E16.18 定義 3.3の数詞代入 API を反復した

\operatorname{sub}_{\chi}(x_1,\ldots,x_k) =\operatorname{Sub}\bigl( \cdots\operatorname{Sub}(\ulcorner\chi\urcorner,i_1,x_1)\cdots, i_k,x_k\bigr)

を数詞代入符号関数 (numeral-substitution code function) という。この関数は原始再帰全関数である。この値を記法の記法で書き、

\ulcorner\chi(\dot x_1,\ldots,\dot x_k)\urcorner

と表す。これは自由変数 $x_1,\ldots,x_k$ をもつ $L_A$ 論理式の中で、一つの値を表す略記として用いる。 $k=0$ のときは固定した文の符号であり、 $\ulcorner\chi\urcorner$ と書く。

記号 $\dot x_j$ に付した点は、外側の変数 $x_j$ の値を数詞へ変えてから符号へ代入することを表す。 $\ulcorner\chi(x_1,\ldots,x_k)\urcorner$ という書き方は用いない。前者は $x_j$ を自由変数としてもつ算術式の中の略記であり、後者は変数記号を含む固定した符号であって、両者は異なる。

例 7.6 (自由変数を残した長さの主張).§E16.19 定理 4.5は、固定した標準自然数 $a,b$ ごとに

Q\vdash\forall z\,\bigl(\operatorname{Len}_Q(\overline{\operatorname{Cons}(a,\operatorname{Cons}(b,0))},z)\leftrightarrow z=\overline2\bigr)

を与える。これは $a,b$ ごとに長さの異なる別々の有限導出である。これに対し補題 5.2 (3)は、 $a,b$ を自由変数として残した一つの文

PA\vdash\forall a\,\forall b\ \operatorname{Len}\bigl(\operatorname{Cons}(a,\operatorname{Cons}(b,0))\bigr)=SS0

を与える。ここで $a$ と $b$ は対象言語の自由変数であり、全称量化子は対象言語の中にある。二つの主張の違いはこの点にある。§E16.19 注意 8.2が述べるとおり、標準入力ごとの無限個のメタ理論上の結論から、一つの対象言語の文が従うわけではない。

8 演習

問題 8.1. 次の問いに答えよ。

補題 2.1で用いた論理式 $\sigma_{a,b}$ が、 $a$ と $b$ について対称な形をしていないにもかかわらず $d\mid b$ が従う理由を、証明のどの構成が担っているかを指摘して述べよ。
補題 3.2の帰納法の主張が、法の積 $P$ を存在量化された証人として持ち回る形になっている理由を述べよ。
$B_{Sl}$ が $i<l$ について正しい剰余をもつことは、どの二つの事実の合成から従うか。
$\operatorname{At}^{0}_Q$ が与える対象と $\operatorname{Entry}^{0}_Q$ が与える対象の違いを述べよ。
補題 5.2 (4)の存在の証明で、第1表と同じ前向きの構成を第2表へ流用することができない理由を述べよ。
上流の記事が原始再帰性を証明していれば、その関数の構造再帰方程式を $PA$ の定理として直ちに用いることができるか。用いることができないならば、何を別に証明する必要があるかを述べよ。

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

$d\mid b$ の証明では、 $s:=A+B$ を用いて $U+A=b\times s$ と $V+B=a\times s$ を満たす自然数 $U,V$ を取り直し、 $r+b\times V=a\times U$ という $\sigma_{a,b}$ の要求する形へ書き換えている。この取り直しが、 $b$ の倍数と $a$ の倍数の役割を入れ替える働きをしており、 $\sigma_{a,b}$ の非対称性を補っている。
可変長 $k$ の族の積 $m_0\times\cdots\times m_{k-1}$ は $L_A$ の項ではなく、既知の関数でもない。従って主張の中で名指すことができず、帰納法の各段で存在を主張する証人として持ち回るほかない。
$M(i,C)\mid P_l$ と $B_{Sl}\equiv B_l\ (\mathrm{mod}\ P_l)$ から補題 1.5 (3)によって $B_{Sl}\equiv B_l\ (\mathrm{mod}\ M(i,C))$ を得ること、および帰納法の仮定が与える $B_l\equiv y_i\ (\mathrm{mod}\ M(i,C))$ に推移律を用いることの二つである。
$\operatorname{At}^{0}_Q(s,i,t)$ の $t$ は、 $s$ から $\operatorname{Dec}_Q$ を $i$ 回たどった反復尾である。第 $i$ 成分はその反復尾の先頭であり、 $\operatorname{Entry}^{0}_Q(s,i,a)$ が与える。
第2表は $e_n=t$ から始めて $e_j=\operatorname{Cons}(a_j,e_{Sj})$ と後ろ向きに定まるので、添字の小さいほうから順に値が決まらない。そこで、末尾から数えた段数 $l$ に関する帰納法を別に立て、各段で表を作り直している。
用いることができない。上流の原始再帰性の証明は、還元後の通常の原始再帰の方程式だけを対象言語の再帰として用いており、還元した関数が元の構造再帰方程式を満たすことはメタ理論の帰納法で示している。補題 6.5のように、還元が定義方程式を満たすことを $PA$ の内部で証明する補題を別に立てる必要がある。

▨

9 境界と次の段階

本記事が証明したのは、 $PA$ の内部で有限列符号と原始再帰関数を一様に扱うことができるということである。用いた道具は、除法定理、最小数原理、Bézout の等式、二つの法に対する中国剰余定理、および有限族の表符号化であり、いずれも帰納法公理スキーマを必要とする。§E16.15 定義 2.1の七公理には帰納法公理が含まれないので、本記事の主張は $Q$ を含むだけの理論へは及ばない。

有限列の符号は§E16.17 注意 4.4の方針に従い、右入れ子の Cons 符号と§E16.19 定義 4.1の五式だけを用いた。有限列の符号を素因数分解符号や Gödel の $\beta$ 関数へ取り替えると、構文符号と計算列の符号が一致しなくなる。ただし、§3 で可変長の族を一括して扱うために用いた補助の表符号は、上流が固定した $M(i,C)=S((Si)\times C)$ を法とする剰余 $\operatorname{Cell}_Q$ であり、これは $\beta$ 関数と同じ形の式である。本記事が $\beta$ 関数を用いないというのは、有限列の符号としては用いないという意味であって、可変長の復号履歴を保持する補助の道具としては、上流が固定したこの式をそのまま用いている。

本記事は、特定の理論 $T$ の公理列挙、証明列、証明述語、および証明可能性述語を扱っていない。これらを対象とする一様な内部主張、すなわち証明列の合成が $PA$ の内部で保存されることと、証明可能性が対象理論の内部でもう一段証明可能になることは、本記事が用意した道具のうえで後続の記事が扱う。また、非標準モデルにおいて $PA$ の内部の「有限列」が外側の有限列に対応するとは限らないことも、本記事は主張していない。§E16.15 定理 3.2により標準モデルでは対応するが、非標準モデルでは長さが非標準の対象が現れる。

§E16.20算術化の PA 内での形式化