§E16.21証明述語と証明可能性述語

1 対象理論と三つの言語水準

算術言語を$L_A=\{0,S,+,\times\}$とする。理論$T$は$L_A$の文からなる公理集合をもち、$Q\subseteq T$を満たすと仮定する。さらに、$T$の公理を重複を許して列挙する決定的プログラム$E_T$を一つ固定する。計算モデルは本記事の中で一つに固定し、有限個の状態と有限個のレジスタをもつ決定的レジスタ機械とする。各命令は、一つのレジスタの値を$1$だけ増やすこと、$1$だけ減らすこと、一つのレジスタが$0$であるかによって次の状態を分けること、または指定したレジスタの値を出力することのいずれかである。証明体系には、一階論理の Hilbert 型体系、modus ponens、一般化、および等号公理を用いる。

2 計算可能な公理列挙を有限証人へ変える

$E_T$の一時点の配置は、状態番号と各レジスタの値を並べた有限列で符号化する。配置が初期配置であること、二配置が一回の計算規則で結ばれること、および配置が数$a$を出力することは、いずれも原始再帰的な関係として選ぶ。固定された有限プログラムについては、各条件が有限個の状態番号の等号、レジスタ値の後続者と前者、零判定、および有限場合分けへ展開されるためである。

公理集合そのものの特性関数は用いていない。存在量化された有限計算証人を証明符号へ含めることが、列挙可能性と原始再帰的な検査を接続する。

3 証明符号と算術式

単に表現可能性定理を適用するだけでは、$\operatorname{Prf}_T$として得られる論理式の形が定まらず、$\Sigma_1$論理式そのものとして固定されるとは限らない。そこで、証明検査の算術式を次の形に固定する。以下では、受理側と棄却側の双方について有限な証人を用意し、量化子をすべて項で有界化した展開として式を固定する。受理側だけを固定すると、標準モデルで偽な入力について$Q$が非標準の証人を排除することができず、否定例の証明可能性が得られない。

固定する式の量化子の形は、§E16.19 定義 2.1が定めた$\Delta_0$論理式と$\Sigma_1$論理式の類に従う。同定義は、順序の略記$t<s$、$t\le s$に加えて加数の位置を入れ替えた略記$t\preccurlyeq s$、$t\prec s$を置き、四つの略記が含む$\exists d$を有界量化子として扱うことを規約としている。数詞を代入した$\Delta_0$文の真偽を$Q$が決定することは§E16.19 補題 3.3が与える。本記事では、加法の第2引数に関係の左辺が来る$\preccurlyeq$と$\prec$の向きも用いる。上界が数詞$\bar n$になったときに$d+\bar n=S^nd$という書き換えを経て、$Q$の内部で有限分解と二分法を得ることができるのがこの向きだからである。どの量化子をこの向きで有界化するかは、以下の各節で個別に述べる。

条件 (d)の一般化の肢では、§E16.18 定義 5.1の第4節がもつ変数条件$\operatorname{GenOK}$を改めて検査していない。同定義の直後が述べるとおり、理論の公理に由来する行はすべて文の符号をもつので、その論理式には自由な変数が現れず、$\operatorname{GenOK}$は自動的に成り立つ。上の定義でも条件 (d)の$k_r=2$の肢が Sentence$(a_r)$を要求している。従って条件 (d)は定義 3.1 条件 (a)および定義 3.1 条件 (b)と同じ規則集合を表す。

$\operatorname{AxWit}_T$の照合は、行に付随して与えられた$w_r$についての有限な検査であって探索ではない。従って、$p$の復号、各行の構文判定、および最終行の照合はいずれも有限回で停止する。

4 固定した式が$\Delta_0$である理由

$\operatorname{Acc}_T$と$\operatorname{Rej}_T$に現れる量化子を四つの系統に分け、それぞれに$L_A$の項の上界を与える。まず§E16.19 定義 4.1の$\operatorname{Dec}_Q(s,a,t)$は$a<s$と$t<s$を含むので、Cons 符号の成分は符号自身より小さい。上で$z$に格納すると定めた証人はすべて$z$の成分であるから、いずれも$z$より小さい。以下で「項$z$で有界化する」というときは、§E16.19 定義 2.1の略記$\preccurlyeq$による有界量化$\exists v\preccurlyeq z$または$\forall v\preccurlyeq z$を指す。$\operatorname{Check}_T$が付加する全称量化子と同じ関係である。

第一の系統として、有限列算術式 API に由来する量化子と上界は次のとおりである。

• $\operatorname{Pair}^{0}_Q(a,b,c)$の$\exists w$は、連言肢$w=a+b$により項$a+b$で有界化する。
• $\operatorname{Cons}^{0}_Q(a,t,c)$の$\exists p$は、連言肢$c=Sp$により項$c$で有界化する。
• $\operatorname{Unique}[\operatorname{Pair}^{0}_Q]$の$\forall z'$は、raw 式が出力に課す上界により項$(a+b)\times S(a+b)+(b+b)$で有界化する。$\operatorname{Unique}[\operatorname{Cons}^{0}_Q]$の$\forall z'$は、$c=Sp$を経由して項$S\bigl((a+t)\times S(a+t)+(t+t)\bigr)$で有界化する。
• $\operatorname{Tab}^{0}_Q(B,C,i,x)$の$\exists q$にはすでに$q\le B$が付いている。$\operatorname{Cell}_Q$の一意性節の全称量化子は、$\operatorname{Tab}^{0}_Q$が含む$x<M(i,C)$により項$M(i,C)=S((Si)\times C)$で有界化する。
• $\operatorname{Prefix}_Q(B,C,s,k)$の$\forall j$はすでに$j<k$で有界である。その内側の$\exists x\exists y\exists a$は、$x<M(j,C)$、$y<M(Sj,C)$、および$\operatorname{Dec}_Q$が与える$a<x$で有界化する。
• $\operatorname{Len}^{0}_Q(s,n)$の$\exists B\exists C$と$\operatorname{At}^{0}_Q(s,i,t)$の$\exists B\exists C$は、$B,C$を$z$の成分として格納するので項$z$で有界化する。$\operatorname{Len}^{0}_Q$の$n\le s$と$\operatorname{At}^{0}_Q$の$i\le s$はすでに有界である。
• $\operatorname{Head}^{0}_Q(s,a)$の$\exists t$は、$\operatorname{Dec}_Q$が与える$t<s$で有界化する。
• $\operatorname{Entry}^{0}_Q(s,i,a)$の$\exists n$は$\operatorname{Len}^{0}_Q(s,n)$が含む$n\le s$で有界化し、$\exists t$は反復尾を$z$の成分として格納するので項$z$で有界化する。
• $\operatorname{Unique}[\operatorname{Len}^{0}_Q]$の$\forall z'$は raw 式が含む$z'\le s$で有界化する。出力の上界が字面に無い$\operatorname{Unique}[\operatorname{Entry}^{0}_Q]$と$\operatorname{Unique}[\operatorname{Concat}^{0}_Q]$の$\forall z'$は項$z$で有界化する。この二つでは$z$より大きい出力候補を排除しないので、有界化した一意性節は元の節より弱い。この弱化は$\operatorname{Acc}_T$の標準モデルでの真理値を変えない。§E16.19 定理 4.5は、標準符号と固定した標準添字を代入した API 式の出力を一つの数詞へ固定しており、その証明は$\operatorname{Len}^{0}_Q$について raw 式の段階で候補が一つに限られることを示し、$\operatorname{Entry}^{0}_Q$と$\operatorname{Concat}^{0}_Q$についても、長さと各段の Cell の機能性から任意の候補出力が同じ数詞に固定されることを示しているからである。従って標準入力では$z$より大きい出力候補がそもそも存在しない。
• $\operatorname{Concat}^{0}_Q(s,t,u)$の$\exists n$はすでに$n\le s$で有界であり、$\exists B\exists C\exists D\exists E$は項$z$で有界化する。内側の$\forall j$は$j<n$で有界であり、$\exists x\exists y\exists a\exists r\exists r'$は$x<M(j,C)$、$y<M(Sj,C)$、$a<x$、$r<M(j,E)$、$r'<M(Sj,E)$で有界化する。

第二の系統は、構文判定の式が字面にもつ量化子である。

$\operatorname{Sentence}(y)$は§E16.18 定義 2.1により$\operatorname{Formula}(y)\land\forall i\le y\,\neg\operatorname{Free}(y,i)$である。この全称量化子はすでに項$y$で有界であり、$\operatorname{Acc}_T$では$y$の位置に$a_r$または$y$が入る。

$\operatorname{Acc}_T$の第4項の$k_r=1$の肢は、$\operatorname{LogAx}(a_r)$を§E16.18 定義 4.2の6つの節の有限選言へ展開した形で含む。$\operatorname{LogAx}$を独立した判定として評価し、その値を trace から読み出すのではない。この6つの節が含む存在量化子は、いずれも項$y$で有界化する。ここでも$y$の位置には$a_r$が入る。同定義の第2項では、上流の字面がすでに$i,t,a,b\le y$を課している。第3項が課すのは$i,a,b\le y$であり、第3項が表示するパターンには項符号が現れないので$t$は無い。第1項の$a,b,c$、第4項の$y=\operatorname{Eq}(t,t)$の$t$、第5項と第6項の$t,u,t_1,u_1,t_2,u_2$には上流の字面に上界が無い。しかし、これらはいずれも表示されたパターンにおいて$y$の真部分符号として現れる。§E16.18 補題 1.2 (1)は、構文符号の直下に現れる項または論理式の符号が全体より小さいことを与えるので、入れ子の各段へ反復して適用すると、これらの符号はすべて$y$より小さい。従って各存在量化子を$\exists\,\cdot\le y$の形へ書くことができる。6つの節が表示する構成子の等式、たとえば第2項の$y=\operatorname{ImpRaw}(\operatorname{AllRaw}(i,a),b)$や第5項と第6項の入れ子の等式を$L_A$の式へ展開すると、$\operatorname{AllRaw}(i,a)$や$\operatorname{AndCode}(\operatorname{Eq}(t_1,u_1),\operatorname{Eq}(t_2,u_2))$のような中間の Cons 値についての存在量化子が新たに現れる。これらの中間値は、表示されたパターンにおける$y$の真部分符号か、その Cons 符号としての尾のいずれかであるから、§E16.18 補題 1.2 (1)と本節の冒頭で述べた$\operatorname{Dec}_Q$の規則を反復して用いると、いずれも$y$より小さい。従って項$y$で有界化する。さらに、これらは上の定義が置いた包括規則、すなわち各 raw 式の存在証人をすべて$z$の成分へ入れるという規則の対象でもあるので、項$z$で有界化することもできる。6つの節が要求する$\operatorname{Term}$、$\operatorname{Formula}$、$\operatorname{Free}$、$\operatorname{FreeFor}$、および$\operatorname{SubTermCode}$の判定は、この展開の中に現れる。これらの評価が導入する量化子は第三の系統が扱う。

第三の系統は、有限分岐評価の遷移列の走査である。

$\operatorname{Acc}_T$の定義の第3項が正典として挙げた trace は、§E16.17 補題 3.2の有限スタックの一段遷移を反復した遷移列、または§E16.17 補題 3.1の履歴符号の列であり、当該判定の値はその末尾から読み出される。同項が述べたとおり、$\operatorname{Sentence}$と$\operatorname{LogAx}$については、上流の定義の字面へ展開したときに現れる各判定の trace がこれにあたる。$\operatorname{Acc}_T$では、いずれの場合も、その列の停止までの接頭部を一つの有限列符号$\tau$として$z$の成分に格納し、次の三条件を課す。第$0$成分が開始状態であること、$N=\operatorname{Len}(\tau)$と$Sm'=N$について、$j\prec m'$を満たす各$j$で第$j$成分と第$Sj$成分が一段の遷移で結ばれること、および第$m'$成分が停止状態であって、そこから当該判定の値が読み出されることである。

この系統だけは、停止時刻を項で押さえるのではなく、$z$の成分として格納した trace 符号自身で押さえる。§E16.17 補題 3.2が与える停止時刻の上界は$3N_K(r(q))$であり、$N_K$は$N_K(0)=1$、$N_K(s+1)=1+K\,N_K(s)$で定まる指数的に増大する関数である。$L_A$の項は$0,S,+,\times$の合成だけからなるので、この上界を項として書くことはできない。上の三条件に現れる量化子は、$\operatorname{Len}^{0}_Q(\tau,N)$が含む$N\le\tau$、$m'\prec N$、および$j\prec m'$で有界であり、$\tau$が$z$の成分であることから、いずれも項$z$で押さえられる。各成分の取得は$\operatorname{Entry}^{0}_Q$であり、その量化子には第一の系統が与えた上界を用いる。一段遷移そのものは、固定された有限個のタグ照合と$\operatorname{Head}$、$\operatorname{Tail}$、$\operatorname{Entry}$、$\operatorname{Cons}$の合成であるから、新たな系統の量化子を生まない。$\operatorname{AxWit}_T$の配置列についても同じ方式を用いる。こちらは証人$w_r$が行に付随して与えられるので、そもそも探索を含まない。

第四の系統は、$\operatorname{Acc}_T$と$\operatorname{Rej}_T$が自ら導入した量化子である。

まず、$\operatorname{Acc}_T$の第2項と$\operatorname{Rej}_T$の第2項が導入する行$\ell_r$とその六成分$k_r,a_r,u_r,v_r,i_r,w_r$の存在量化子と、$\ell_r=\operatorname{Line}_T(k_r,a_r,u_r,v_r,i_r,w_r)$、$a_{u_r}=\operatorname{ImpRaw}(b,a_r)$、$a_r=\operatorname{AllRaw}(i_r,a_{u_r})$の各等式を$L_A$の式へ展開したときに現れる中間の Cons 値の存在量化子がある。これらはいずれも定義が$z$の成分として格納すると定めたものであるから、本節の冒頭で述べた規則により項$z$で有界化する。

格納の宣言が及ばない読み出しは、上界を$p$に取る。$\operatorname{Rej}_T$の第3項が格納を宣言しているのは復号表と当該の判定 trace だけであり、同項が読む第$m$行とその論理式$a_m$は宣言に入っていない。$\operatorname{Rej}_T$の第2項が先行行として読む$a_{u_r}$も同様である。これらはいずれも$p$の成分である行の、さらにその成分であるから、本節の冒頭で述べた$\operatorname{Dec}_Q$の規則を$p$から二段反復して用いると、項$p$で有界化する。残りの量化子は次のとおりである。

第4項の modus ponens の肢にある$\exists b$は、$a_{u_r}=\operatorname{ImpRaw}(b,a_r)$により$b$が$a_{u_r}$の直下成分であることから、$b<a_{u_r}$で有界化する。$a_{u_r}$は、$\operatorname{Acc}_T$では$z$の成分であり、$\operatorname{Rej}_T$では上に述べたとおり項$p$で押さえられる。第5項と$\operatorname{Rej}_T$の第3項が用いる$Sm=n$の$\exists m$は、$m\prec n$すなわち項$n$で有界化する。$L_A$には切捨て減法が無いので、最終行の添字を$n-1$という項で書くことはできず、この存在量化子を置くほかない。全行条件の全称量化子は$r<n$であり、$\operatorname{Rej}_T$の第2項の$\exists r$も同じ上界をもつ。$n$自身の存在量化子は$\operatorname{Len}^{0}_Q(p,n)$が含む$n\le p$で有界である。最後に、本節が用いる順序の四つの略記$t<s$、$t\le s$、$t\preccurlyeq s$、$t\prec s$が含む$\exists d$は、§E16.19 定義 2.1の規約によりいずれも有界量化子として扱う。

以上により、$\operatorname{Acc}_T$と$\operatorname{Rej}_T$に現れるすべての量化子に、$p,y,z$と外側の束縛変数から作った$L_A$の項の上界が与えられた。従って両者は§E16.19 定義 2.1の$\Delta_0$論理式である。$\operatorname{Check}_T$が付加する全称量化子も$z$で有界であるから$\operatorname{Check}_T$も$\Delta_0$論理式であり、(P) は$\Sigma_1$論理式である。

5 受理証人と棄却証人

上で固定した二つの式が標準自然数について排他的かつ網羅的であることを、独立の命題として取り出す。この主張は以下の主結果が繰り返し用いる。

(2)が述べるとおり、付加した第2連言は (P) の標準モデルでの真理値を変えない。この連言を置くのは、標準モデルで偽な入力について$Q$が (P) を反証することができるようにするためである。

証人$z$を式 (P) に明示した理由を述べる。表現可能性定理を適用して$\operatorname{Proof}_T$を表す何らかの算術式を得るだけでは、その式が$\Sigma_1$論理式の形をもつとは限らない。証人を$z$に集めて (P) の形を固定すると、$\operatorname{Prf}_T$は同値な別の式へ取り替えることなく、それ自身が$\Sigma_1$論理式になる。この差は導出可能性条件 D3 で効く。$\operatorname{Prov}_T(\ulcorner\varphi\urcorner)$が$\Sigma_1$論理式として固定されていない場合には、これと同値な$\Sigma_1$文$\sigma$を別に作ることになり、$\sigma$の符号と$\ulcorner\operatorname{Prov}_T(\ulcorner\varphi\urcorner)\urcorner$が異なる自然数になるため、符号を取り替える一段が必要になる。(P) の形で固定しておけば、この一段が生じない。後続の記事はこの点を明示して D3 を証明する。

6 証明符号を合成する関数

二つの証明列を連結するときは、後半の行が参照する行番号を前半の長さだけずらし、末尾に modus ponens の一行を加える。この有限列操作を固定しておく。

7 理論の無矛盾性を表す文

この命題は標準モデルについての外的な同値である。$T\vdash\operatorname{Con}_T$を主張していない。また、自然言語で述べるすべての無矛盾性概念が同じ算術文になるとも主張していない。

8 演習

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

1. 前者は標準モデルでの意味論的真理であり、後者は対象理論内の形式的導出である。両者は定義 1.1が区別する別の水準の主張であり、一方から他方は従わない。
2. 非論理公理の行が実際に公理であるかを、公理でない入力について判定する検査が停止しない可能性がある。公理集合が列挙可能であるだけの場合、列挙されないことを有限時間で確かめる手続きが一般には無いからである。
3. 二つの入力列の末尾がそれぞれ$\varphi\to\psi$と$\varphi$であり、連結後に両行を参照する modus ponens の行を末尾へ追加するからである。その行の論理式は$\operatorname{Conseq}(\ulcorner\varphi\to\psi\urcorner)=\ulcorner\psi\urcorner$である。
4. 三領域に分ける議論が、外側の標準自然数$n,m$に関する有限回の場合分けだからである。同じ議論を対象理論の内部で行うには、可変長の列に関する法則を対象理論が証明しなければならない。

▨

9 境界と次の段階

本記事は$\operatorname{Prf}_T$、$\operatorname{Prov}_T$、$\operatorname{Con}_T$を固定し、$\operatorname{Prf}_T$が$\Sigma_1$論理式であることと、証明符号の合成関数およびその外的な閉性を証明した。導出可能性条件 D2 と D3 は、外的な原始再帰関数、グラフを表す算術式、および対象理論内の存在証明を区別したうえで、対象理論が Peano 算術$PA$を含む場合に別の記事が証明する。注意 6.3の通り、本記事は一様な内部主張を扱わない。第一不完全性定理、導出可能性条件、および第二不完全性定理の結論は、本記事の証明には用いていない。