§E19.19算術における表現可能性

証明.§E19.15 定義 2.1 (Q3)を$x$と順序の証人へ外側で固定した回数だけ適用し、各変数を零、固定回数以内の後続者、またはさらに後続者をもつ残余のいずれかへ分ける。§E19.15 定義 2.1 (Q4)、§E19.15 定義 2.1 (Q5)で加法をその固定回数だけ展開する。右辺が$\overline r$を越える場合は、§E19.15 定義 2.1 (Q2)で共通する後続者を除いた後に§E19.15 定義 2.1 (Q1)を用いて排除することができる。残る場合は§E19.15 補題 4.1の固定数詞加法により、表示した各数詞と一致する。これは$r$ごとに長さの異なる有限導出であり、自由変数$r$に関する帰納法ではない。▨

証明.補題 3.1により、

である。左辺の有界全称条件からは、$i=\overline j$を各$j<r$について代入して$\theta(\overline j,\vec z)$を得る。逆に右辺の有限連言を仮定する。$i<\overline r$を満たす$i$は表示した有限選言のいずれかの数詞に等しいため、等号の置換可能性により$\theta(i,\vec z)$を得る。$i$を全称化すると左辺が従う。$r=0$では候補の選言と右辺の連言がともに空であり、同じ論証が成り立つ。▨

証明.主張 (1)を示す。$z\preccurlyeq\bar m$は$\exists d\,(d+z=\bar m)$である。左から右を示す。§E19.15 定義 2.1 (Q3)を$z$へ$m+1$回適用すると、$z$は$\bar0,\ldots,\bar m$のいずれかに等しいか、ある$e$について$z=S^{m+1}e$である。最後の場合、§E19.15 定義 2.1 (Q5)を$m+1$回用いると$d+S^{m+1}e=S^{m+1}(d+e)$であり、$\bar m=S^m0$と合わせて§E19.15 定義 2.1 (Q2)で$m$個の後続者を消すと$S(d+e)=0$を得るので、§E19.15 定義 2.1 (Q1)に反する。右から左は、各$j\le m$について§E19.15 補題 4.1により$\overline{m-j}+\bar j=\bar m$が得られることによる。$\prec$の同値は、$z\prec\bar m$が$Sz\preccurlyeq\bar m$であることと、$Sz=\bar0$が§E19.15 定義 2.1 (Q1)に反すること、および$Sz=S\bar j$から§E19.15 定義 2.1 (Q2)で$z=\bar j$が従うことから得る。

主張 (2)を示す。§E19.15 定義 2.1 (Q3)を$z$へ$m$回適用すると、$z$は$\bar0,\ldots,\overline{m-1}$のいずれかに等しいか、ある$d$について$z=S^md$である。前者の各場合は主張 (1)により$z\prec\bar m$を与える。後者では、§E19.15 定義 2.1 (Q4)、§E19.15 定義 2.1 (Q5)を$m$回用いて$d+\bar m=S^md=z$を得るので$\bar m\preccurlyeq z$である。$m=0$では最初の選言が空であり、§E19.15 定義 2.1 (Q4)の$d+0=d$から$\bar0\preccurlyeq z$である。

主張 (3)を$\delta$の構成に関するメタ理論の帰納法で示す。数詞を代入した後、各量化子の上界と各原子式の項は閉項である。任意の閉項$t$について$Q\vdash t=\overline{t^{\mathbb N}}$が成り立つことを、項の構成に関するメタ理論の帰納法で先に確かめる。$t$が$0$のときは自明であり、$t=Su$のときは帰納法の仮定と等号の合同から従う。$t=u+u'$と$t=u\times u'$のときは、帰納法の仮定で両辺を数詞へ移したうえで、§E19.15 補題 4.1により得られる$Q\vdash\overline a+\overline b=\overline{a+b}$と$Q\vdash\overline a\times\overline b=\overline{ab}$を用いる。原子式$t=s$については、両辺を値の数詞へ移したうえで、同補題により真の場合の等号の証明と偽の場合の$Q\vdash\overline a\ne\overline b$が得られる。順序の略記$t\le s$、$t<s$、$t\preccurlyeq s$、$t\prec s$については、閉項の値を数詞へ移したうえで、$\le$と$<$には補題 3.1を、$\preccurlyeq$と$\prec$には主張 (1)を適用して証人の候補を有限個の数詞へ分け、各候補について数詞の等式を§E19.15 補題 4.1で判定する。命題結合子の場合は、部分式についての帰納法の仮定と命題論理の有限導出で閉じる。有界量化$\forall v\le t\,\delta'$と$\exists v\le t\,\delta'$は、$t$の値を数詞$\bar r$へ移した後、補題 3.1により得られる同値$v\le\bar r\leftrightarrow(v=\bar0\lor\cdots\lor v=\bar r)$により、$v=\bar0,\ldots,\bar r$についての有限連言と有限選言へ展開されるので、各項に帰納法の仮定を適用することができる。上界が$<$で与えられる全称量化については、補題 3.2により同じ展開が直接得られる。上界が$<$で与えられる存在量化は同じ補題 3.1の第1の同値で、上界が$\preccurlyeq$、$\prec$で与えられる有界量化は主張 (1)の有限分解で、それぞれ同様に扱う。▨

証明. 最初に Bézout の等式を Euclid の互除法から導く。正の自然数$a,b$に除法を反復し、

とする。正の余りは真に減少するため、有限回で余り$0$に達する。最後の非零余り$d$は、各等式を逆向きにたどると$a,b$の公約数であり、$a,b$の任意の公約数は各余りを割るため$d$も割る。したがって$d=\gcd(a,b)$である。また、最後の非零余りから等式を順に逆代入すると、整数$u,v$が存在して

となる。

互いに素な二法$m,n$について、$um+vn=1$を満たす整数$u,v$を取る。剰余$\alpha,\beta$に対して

とおけば、$x\equiv\alpha\pmod m$かつ$x\equiv\beta\pmod n$である。$x$を$mn$で割った非負の余りを$B$とすれば、$B$は同じ二つの合同式を満たす。これで二法の場合が従う。

法の個数に関する有限帰納法を用いる。一法$m_0$の場合は、$x_0$を$m_0$で割った非負の余りを$B_0$とすればよい。最初の$k+1$個の合同式を満たす数を$B_k$とし、

とおく。各$i\le k$について$\gcd(m_i,m_{k+1})=1$なので、 Bézout の等式から$u_im_i\equiv1\pmod{m_{k+1}}$を満たす整数$u_i$を取ることができる。これらを掛け合わせると

となるため、$M_k$と$m_{k+1}$は互いに素である。二法の場合を、法$M_k,m_{k+1}$と剰余$B_k,x_{k+1}$へ適用する。得られた$B_{k+1}$は最初の$k+1$個の合同式を保ち、新しい合同式も満たす。有限帰納法により結論を得る。この論証は標準自然数と整数についての有限なメタ理論上の証明であり、外部の中国剰余定理も$Q$内の帰納法も用いていない。▨

証明.$C$を$1,\ldots,r$のすべてで割り切れ、かつ$x_i<1+(i+1)C$をすべての$i\le r$で満たす正の標準自然数とする。例えば$r!\,(1+\max_{i\le r}x_i)$を必要ならさらに大きく取ればよい。$M_i=1+(i+1)C$とおく。$M_i-(i+1)C=1$なので、$M_i$は$C$と互いに素である。$i<j$とし、$d$を$M_i$と$M_j$の正の公約数とする。差を取ると$d$は$(j-i)C$を割る。$d$と$C$は互いに素であるから、Bézout の等式を用いると$d$は$j-i$を割る。一方、$j-i$は$C$を割るため$M_i\equiv1\pmod{j-i}$である。従って$d$は$1$を割り、$M_i$と$M_j$は互いに素である。したがって補題 4.2により、次の合同式をすべての$i\le r$について満たす標準自然数$B$が存在する。

対応する商を$q_i$とすれば$q_i\le B$である。

固定した$B,C,i$に対する Cell の強い検証は、補題 3.1だけで行うことができる。 Tab の$z<M(i,C)$により$z$は固定個の数詞へ、存在する$q\le B$により$q$も固定個の数詞へ分かれる。各組では$B=q\times M(i,C)+z$は数詞だけの等式であるから、§E19.15 補題 4.1により正しい一組を証明し、ほかの組を§E19.15 定義 2.1 (Q1)、§E19.15 定義 2.1 (Q2)で否定することができる。したがって$Q$は Cell の存在連言と任意候補の一意性連言を直接証明し、表示した双条件を得る。ここでは本記事後半の一般表現可能性定理を用いていない。▨

証明. 一般に Unique$[R](\vec x,u)$と Unique$[R](\vec x,v)$を仮定する。第1の式の全称節を第2の式により得られる$R(\vec x,v)$へ適用すると$v=u$を得る。等号の対称律から$u=v$である。この論証は$R$の算術的性質を使わない純粋な一階論理の導出である。五つの API 式はすべて Unique の形で定義したので、各機能性が$Q$で証明される。 Unique の第1連言は raw 計算の存在を要求するため、この定義だけから全入力での出力存在は従わない。▨

証明.$a,b$を固定すると Pair$^{0}_Q$の$w$は固定数詞$\overline{a+b}$に等しい。候補出力$z$は Pair$^{0}_Q$に加えた固定上界以下なので、補題 3.1で有限個の数詞へ分けることができる。$z+z=(w\times Sw)+(b+b)$を固定数詞計算で調べると$z=\overline p$だけが残る。正しい数詞は同じ計算から raw 式を満たすため、Unique の連言も含めて Pair$_Q$の双条件を得る。 Cons$^{0}_Q$では Pair の raw 出力が同じ議論で$\overline p$に固定され、$z=Sp$から$z=\overline{c'}$が従う。これにより Cons$_Q$の双条件も得る。

$c_0=c$、$c_{j+1}=\operatorname{Tail}(c_j)$とおくと、外側の標準計算により$c_0,\ldots,c_n=0$と各$a_j=\operatorname{Head}(c_j)$が具体的な数詞として得られる。 Pair$^{0}_Q$には出力の固定上界を入れたので、固定した入力$a,t$について候補$p$を有限分解し、数詞計算により正しい pair 値だけを残すことができる。Cons についても$c=Sp$から同じことが従う。したがって各標準$c_j>0$について

を得る。$a,t<c_j$は補題 3.1により有限個の数詞へ分かれるため、式 (4.5.1)は Pair の一般的な逆関数定理を$Q$内で用いたものではない。

長さの正しい候補を作る。標準表$c_0,\ldots,c_n$に対して補題 4.3で構成した$B,C$を数詞として代入する。各 Cell と各式 (4.5.1)を用い、$j<n$を固定有限選言へ分けると$Q\vdash\operatorname{Len}^{0}_Q(\overline c,\overline n)$を得る。ここで$n\le c$は、正である間に Tail が真に減少する外側の有限計算から得た数詞不等式である。

任意の候補$z$について Len$^{0}_Q(\overline c,z)$を仮定する。$z\le\overline c$なので、$z=\overline0,\ldots,\overline c$へ有限分解することができる。$z=\overline k$を一つ固定する。 Prefix の第0 Cell と各段の Cell の機能性を用い、式 (4.5.1)を$k$または$n$まで有限回適用すると、第$j$Cell の値は$\overline{c_j}$に限られる。$k<n$なら終端 Cell の値$0$と$c_k>0$が矛盾する。$k>n$なら Prefix の第$n$段が$x=c_n=0$と$x\ne0$を同時に要求するため矛盾する。したがって$k=n$だけが残る。これにより

を得る。raw 式の存在と一意性を得たため、Unique を加えた Len$_Q$についても同じ双条件が成り立つ。

Entry を検証する。$i<n$なら標準表$c_0,\ldots,c_i$を At$^{0}_Q$の証人とし、式 (4.5.1)の Head 成分から出力$\overline{a_i}$を得る。任意の候補では Len の直前の一意性から$n$が固定され、At の Prefix と Cell の機能性から反復尾が$\overline{c_i}$に固定され、式 (4.5.1)から Head が$\overline{a_i}$に固定される。$i\ge n$では Len が$\overline n$に固定され、 Entry$^{0}_Q$の第2選言が出力を$0$に固定する。固定数詞$i,n$の$i<n$と$n\le i$の場合分けも七公理からの有限数詞計算である。よって範囲内と範囲外の両方で、Entry$_Q$の表示した双条件を得る。

最後に Concat を検証する。第1表に$c_0,\ldots,c_n$、第2表に

を入れると、$e_0=e$、$e_n=d$、$e_j=\operatorname{Cons}(a_j,e_{j+1})$である。二つの標準有限表の Cell、式 (4.5.1)、および固定入力に対する Cons$_Q$の存在を並べれば Concat$^{0}_Q(\overline c,\overline d,\overline e)$を得る。任意の候補出力では、長さの議論が$n$と第1表の各$c_j,a_j$を固定する。第2表の終端は$e_n=d$に固定されるので、$j=n-1,\ldots,0$の順に Cons$_Q$の固定入力一意性を有限回用いると、第0 Cell と出力候補は$\overline e$に固定される。$n=0$では第0 Cell が同時に候補出力と$d$を表し、Cell の機能性から直ちに一致する。

以上は、各標準列と各固定添字について、§E19.15 定義 2.1 (Q3)による有限分解、§E19.15 定義 2.1 (Q1)、§E19.15 定義 2.1 (Q2)による数詞の分離、§E19.15 定義 2.1 (Q4)–§E19.15 定義 2.1 (Q7)による固定数詞計算を有限回並べた導出である。$PA$の帰納法も、本記事後半の原始再帰関数の一般表現可能性も、Len または Entry を Cell の定義に用いる循環もない。▨

証明. 固定した標準入力を代入する。零関数と射影では、表示した式自体が$y=\overline0$または$y=\overline{n_i}$である。後続者では$S\overline n$は定義により$\overline{n+1}$である。等号の反射律、対称律、推移律から、各場合に$Q\vdash\forall y(\varphi(y)\leftrightarrow y=\overline m)$を得る。▨

証明. 標準入力$\vec n$を固定し、$b_j=g_j(\vec n)$、$c=f(b_1,\ldots,b_m)$とおく。帰納法の仮定により

が各$j$について得られる。したがって$\varphi_h(\overline{\vec n},y)$の存在量化された各$z_j$は$\overline{b_j}$へ順に消去することができる。$f$に関する仮定を固定入力$\vec b$へ適用すると

を得る。$y$を全称閉包して必要な強い表現が従う。▨

証明. 最初に$\ell\ge1$とし、標準入力$\vec n,r$を固定する。外側の自然数計算で

という実際の有限計算列を作る。その Cons 符号を$c$とする。定理 4.5により、$Q$は Len$_Q(\overline c,\overline{r+1})$と、各$j\le r$に対する Entry$_Q(\overline c,\overline j,\overline{a_j})$を、一意出力の形で証明する。