§E16.24導出可能性条件と第二不完全性定理

証明.$T\vdash\varphi$と仮定する。この仮定は、標準自然数で符号化された有限な$T$証明が存在するという外的主張である。その証明符号を$p_0$とする。§E16.21 定理 5.4の具体的証明の内部化により

である。存在導入により

すなわち$Q\vdash\Box_T\varphi$を得る。$Q\subseteq PA\subseteq T$なので$PA\vdash\Box_T\varphi$かつ$T\vdash\Box_T\varphi$である。ここでは$T\vdash\varphi$という外的前提を標準モデルにおける真理へ移していない。具体的な有限証明符号$p_0$を数詞として$Q$内へ移しただけであり、$T$の無矛盾性や健全性を用いていない。▨

証明.$\operatorname{Prf}_T(p,y)$は$\exists z\,\operatorname{Check}_T(p,y,z)$の略記である。§E16.21 定義 3.3は$\operatorname{Check}_T(p,y,z)$を、受理証人の条件$\operatorname{Acc}_T(p,y,z)$と、$z'\preccurlyeq z$を満たす棄却証人が存在しないという条件との連言として定めている。$\operatorname{Acc}_T$は五つの項目からなる。上流はこれらを第1項から第5項と呼ぶが、本補題自身の項と紛れるため、本記事では第1節から第5節と呼ぶ。第1節、第2節、第4節、第5節が上の第1項から第3項までの条件そのものであり、第3節は各行で必要になる原始再帰的検査の計算 trace が$z$の成分として入っていることを述べる。

左から右を示す。$\operatorname{Check}_T(p,y,z)$を仮定すると、第1連言から$\operatorname{Acc}_T(p,y,z)$が成り立つ。その第1節と第2節は$\operatorname{Len}^{0}_Q$、$\operatorname{At}^{0}_Q$、$\operatorname{Entry}^{0}_Q$の raw 式によって$p$の長さと各行の六成分を取り出す。§E16.20 補題 5.2 (1)と第2項により、これらの値は$PA$の内部で一意に定まり、$\operatorname{Len}(p)$と$\operatorname{Entry}(p,s)$に等しい。従って第1項が成り立ち、第4節と第5節から第2項と第3項が成り立つ。

右から左を示す。 第1項から第3項までを仮定し、$\operatorname{Check}_T(p,y,z)$を満たす$z$を作る。

まず、$z$に入るべき成分をすべて集める。$n:=\operatorname{Len}(p)$とする。§E16.20 補題 5.1 (5)は、$p$の第$n$反復尾が$0$であり、$i<n$を満たす各$i$の反復尾が$0$でないような$n$の存在を与える。§E16.20 補題 5.2 (1)により、この$n$は$\operatorname{Len}(p)$に等しい。$\operatorname{At}^{0}_Q(p,n,0)$が成り立つので、その証人として、$p$を$n$回復号する表符号$(B,C)$を取ることができる。各行$\ell_s$とその六成分は§E16.20 補題 5.2 (2)が与える一意な値である。各行について$z$へ集める trace は、§E16.21 定義 3.3の定義の第3項が正典として定めた一覧に従う。すなわち$\operatorname{Term}$、$\operatorname{Formula}$、$\operatorname{Free}$、$\operatorname{FreeFor}$、$\operatorname{SubTermCode}$、$\operatorname{Look}$、および$\operatorname{AxWit}_T$のうち、当該行で必要となるものの trace である。$\operatorname{LogAx}$と$\operatorname{Sentence}$は、同項が上流の定義の字面へ展開した形で用いると定めた述語であり、固有の遷移列をもたない。従ってこの二つについて同項が求めるのは、展開に現れる上の各判定の trace である。$\operatorname{Term}$、$\operatorname{Formula}$、$\operatorname{Free}$、$\operatorname{FreeFor}$は§E16.18 定理 5.2により、$\operatorname{SubTermCode}$は§E16.18 定理 3.4により、$\operatorname{Look}$は§E16.18 定義 3.2と§E16.17 補題 3.1により、$\operatorname{AxWit}_T$は§E16.21 定理 2.2により、いずれも原始再帰的である。従って、それぞれの計算の接頭トレース$R(q,n')$も原始再帰全関数の値である。§E16.20 補題 6.1 (1)により、これらの値はいずれも$PA$の内部で存在し一意である。$\operatorname{AxWit}_T$の証人$w_s$は行$\ell_s$の第6成分としてすでに$p$の中にあり、その検査 trace も同じ理由で一意に定まる。$\operatorname{Term}$、$\operatorname{Formula}$、$\operatorname{Free}$については§E16.20 補題 7.2 (2)、$\operatorname{FreeFor}$については同補題の第3項、$\operatorname{SubTermCode}$については同補題の第4項が、いずれも§E16.20 補題 6.5 (2)を経て、$PA$がその値の構造再帰方程式を証明することを与える。$\operatorname{Look}$については§E16.20 補題 7.1 (1)が定義方程式を与える。$\operatorname{LogAx}$と$\operatorname{Sentence}$自身については、構造再帰方程式による展開を用いない。ここで用いるのは、上の一覧が挙げた判定の値の存在と一意性だけである。

次に、これらを一つの符号へまとめる。各添字$s<n$に対して、第$s$行に付随する成分を並べた符号を対応させる論理式は、上で述べた一意性により$s$ごとに一意な値を定める。§E16.20 補題 3.2を用いてこの族の表符号を取り、§E16.20 補題 5.2 (7)の末尾追加を$n$回繰り返す帰納法によって、長さ$n$の一つの列符号へ収めることができる。復号表と全体に関わる成分を先頭へ加えると、目的の$z$を得る。

最後に、$z'\preccurlyeq z$を満たす棄却証人が存在しないことを確かめる。§E16.21 定義 3.3の$\operatorname{Rej}_T(p,y,z')$は、次の三つの場合のいずれかを、$z'$に格納した復号表と trace とともに主張する。第一は、$\operatorname{Len}(p)=0$であることである。第二は、$n=\operatorname{Len}(p)>0$であり、ある行$r<n$について$\operatorname{Formula}(a_r)$または第4節の四つの場合のいずれもが成り立たないことである。第三は、$n=\operatorname{Len}(p)>0$であり、$a_{n-1}\ne y$もしくは$\neg\operatorname{Sentence}(y)$であることである。

第一の場合を排除する。仮定した第1項は$0<n=\operatorname{Len}(p)$を与えており、§E16.20 補題 5.2 (1)により長さの値は$PA$の内部で一意であるから、$\operatorname{Len}(p)=0$は成り立たない。第二の場合と第三の場合を排除する。$\operatorname{Rej}_T$が読み出す長さ、成分、および各判定の値は、同じ§E16.20 補題 5.2と§E16.20 補題 6.1により$PA$の内部で一意に定まるので、仮定した第2項および第3項と衝突する。従って$PA$は$\forall z'\,\neg\operatorname{Rej}_T(p,y,z')$を証明し、とくに$z'\preccurlyeq z$へ有界化した連言肢を得る。

以上により$\operatorname{Check}_T(p,y,z)$を満たす$z$が存在し、$\operatorname{Prf}_T(p,y)$を得る。▨

証明.$PA$の内部で$b,c,p,q$を取り、二つの前件を仮定する。$n=\operatorname{Len}(p)$、$m=\operatorname{Len}(q)$とすると、補題 4.1により$n,m>0$であり、$p$の末尾行の論理式は$\operatorname{ImpRaw}(b,c)$、$q$の末尾行の論理式は$b$である。§E16.21 定義 6.1の$\operatorname{Conseq}$は、符号が$\operatorname{ImpRaw}(b,c)$の形をもつときにその後件$c$を返す原始再帰全関数であり、§E16.20 補題 6.1 (2)によりその定義列の方程式は$PA$の定理である。従って$PA$は$\operatorname{Conseq}(a_{n-1})=c$を証明する。また、§E16.20 補題 7.2 (2)が与える$\operatorname{Formula}(\operatorname{ImpRaw}(b,c))\leftrightarrow(\operatorname{Formula}(b)\land\operatorname{Formula}(c))$と$\operatorname{Free}(\operatorname{ImpRaw}(b,c),i)\leftrightarrow(\operatorname{Free}(b,i)\lor\operatorname{Free}(c,i))$、および同補題の第1項が与える$c<\operatorname{ImpRaw}(b,c)$により、§E16.18 定義 2.1の$\operatorname{Sentence}$の定義の有界全称量化がそのまま$c$へ移る。従って$\operatorname{Sentence}(\operatorname{ImpRaw}(b,c))$から$\operatorname{Sentence}(c)$が従う。

$r=\operatorname{comb}(p,q)$と置く。$\operatorname{comb}$は原始再帰的な$\operatorname{Concat}$と$\operatorname{Cons}$で定義されているのに対し、$\operatorname{Prf}_T$は有限列算術式 API を用いる。§E16.20 補題 6.7と§E16.20 補題 6.4により、$PA$は双方の値が一致することを証明するので、以下では区別せずに扱う。§E16.20 補題 5.2 (6)と第7項により、$PA$は$\operatorname{Len}(r)=n+m+1$と、$r$の第$s$成分についての次の三つの場合分けを証明する。ここで$\operatorname{comb}$は二回の連結として定義されており、末尾の一行は長さ$1$の列との連結として加わる。

$s<n$の場合、$r$の第$s$行は$p$の第$s$行である。規則タグ、論理式、先行添字、公理証人はいずれも変わらず、先行添字は$s$より小さいままである。従って補題 4.1 (2)の該当する場合が$r$でも成り立つ。参照する先行行が$p$の中にあることは、$s<n$の範囲で$r$と$p$の成分が一致することから従う。

$n\le s<n+m$の場合、$s=n+j$と書くと、$r$の第$s$行は$q$の第$j$行を$\operatorname{Shift}_n$で移したものである。論理公理行と理論公理行では、論理式、$\operatorname{LogAx}$判定、$\operatorname{AxWit}_T$証人が変わらないので条件はそのまま保たれる。modus ponens 行では、$q$における先行添字$u,v<j$が$u+n,v+n<n+j=s$となり、参照先の論理式は第2領域で同じだけ移るため、$a_{u+n}=\operatorname{ImpRaw}(a', a_{s})$と$a_{v+n}=a'$という一致が保たれる。一般化行でも同様に、先行添字が$n$だけ増え、一般化変数と本体の論理式が変わらないので条件が保たれる。ここで用いた「$\operatorname{Shift}_n$が論理式を変えない」という事実と「添字が$n$だけ増える」という事実は、次のように得る。§E16.21 定義 6.1は$\operatorname{Shift}_n$を Cons 符号に関する有界コース再帰で定めており、§E16.20 補題 4.1により$PA$は$0<s\to\operatorname{Tail}(s)<s$を証明するので、§E16.20 補題 6.5 (1)により$PA$は$\operatorname{Shift}_n$の二つの定義方程式を証明する。そのうえで列の長さに関する$PA$の帰納法を行い、§E16.20 補題 5.2 (3)で成分を追跡すればよい。

$s=n+m$の場合、$r$の第$s$行は$\operatorname{Line}_T(3,c,n-1,n+m-1,0,0)$である。第$n-1$行の論理式は$\operatorname{ImpRaw}(b,c)$、第$n+m-1$行の論理式は$b$であるから、modus ponens の節が$a'=b$について成り立つ。二つの先行添字はいずれも$s$より小さい。

以上で$r$の全行が第2項を満たす。末尾行の論理式は$c$であり、$\operatorname{Sentence}(c)$はすでに得ている。従って補題 4.1により$\operatorname{Prf}_T(r,c)$である。

第二の主張は、二つの前件の存在量化子を除去して$p,q$を取り、第一の主張を適用したうえで$\operatorname{comb}(p,q)$を証人として存在導入すれば得られる。▨

証明.§E16.18 定義 1.1が含意の符号を$\operatorname{ImpRaw}(y,z)=\operatorname{SeqCode}(8,y,z)$と固定しているので、$\ulcorner\alpha\to\beta\urcorner=\operatorname{ImpRaw}(\ulcorner\alpha\urcorner,\ulcorner\beta\urcorner)$である。補題 4.2の第二の主張の全称量化子へ$b:=\ulcorner\alpha\urcorner$、$c:=\ulcorner\beta\urcorner$を代入すると、表示した$PA$の定理を得る。$PA\subseteq T$より$T$も同じ文を証明する。この導出では、標準証明符号を一つも選んでいない。$p,q$を自由変数として残した補題 4.2を用いており、無矛盾性も用いていない。▨

証明.$k$は外側で固定した自然数なので、$k$に関する帰納法は不要であり、$k$段の有限な操作を並べればよい。$j=0,1,\ldots,k$について、$\chi$の$v_{i_1},\ldots,v_{i_j}$へ$e_1,\ldots,e_j$を代入し、残る$v_{i_{j+1}},\ldots,v_{i_k}$を全称量化した符号を$\theta_j(\vec e)$と書く。$\theta_0$は仮定の$\forall\vec v\,\chi$であり、$\theta_k(\vec e)$は$\operatorname{inst}_{\chi}(\vec e)$である。

まず、各$e_j$が閉項符号であれば、$j=0,1,\ldots,k$のすべてについて$\theta_j(\vec e)$が文の符号であることを確かめる。$j=0$では、$\theta_0$は固定した文$\forall\vec v\,\chi$の符号であるから$\operatorname{Sentence}(\theta_0)$が成り立つ。§E16.20 補題 7.3により、符号に自由に現れる変数の添字はその符号より小さいので、$\operatorname{Sentence}$に現れる有界全称量化$\forall i\le y$はすべての候補を調べており、$\forall k'\,\neg\operatorname{Free}(\theta_0,k')$が従う。以下の各段でも、文の符号であるという主張はこの有界化していない形で用いる。$\theta_j(\vec e)$が文の符号であるとし、$\theta_j(\vec e)=\operatorname{AllRaw}(i_{j+1},a_j)$と書く。§E16.20 補題 7.2 (2)が与える$\operatorname{Formula}$と$\operatorname{Free}$の$\operatorname{AllRaw}$の節により、$\operatorname{Formula}(a_j)$が成り立ち、$\operatorname{Free}(a_j,k')$を満たす$k'$は$k'=i_{j+1}$に限る。$\theta_{j+1}(\vec e)=\operatorname{SubTermCode}(a_j,i_{j+1},e_{j+1})$であり、$e_{j+1}$は閉項符号であるから$\operatorname{Term}(e_{j+1})$が成り立つ。従って§E16.20 補題 7.4 (7)を$a:=a_j$、$i:=i_{j+1}$、$t:=e_{j+1}$について適用することができる。同項の前半により$\operatorname{Formula}(\theta_{j+1}(\vec e))$である。同項の後半により、$\operatorname{Free}(\theta_{j+1}(\vec e),k')$が成り立つならば、$k'\ne i_{j+1}$かつ$\operatorname{Free}(a_j,k')$であるか、または$\operatorname{Free}(a_j,i_{j+1})$かつ$\operatorname{Free}(e_{j+1},k')$である。前者は$\operatorname{Free}(a_j,k')\to k'=i_{j+1}$に反する。後者については、同補題が「$e$が閉項符号であること」と$\operatorname{Term}(e)\land\forall k'\,\neg\operatorname{Free}(e,k')$との同値を$PA$の定理として与えているので、$\operatorname{Free}(e_{j+1},k')$はこれに反する。従って$PA$は$\forall k'\,\neg\operatorname{Free}(\theta_{j+1}(\vec e),k')$を証明する。§E16.18 定義 2.1の$\operatorname{Sentence}$は$\operatorname{Formula}$と有界全称量化$\forall i\le y\,\neg\operatorname{Free}(y,i)$の連言であるから、有界化していない主張からこの連言が従い、$\operatorname{Sentence}(\theta_{j+1}(\vec e))$を得る。

同じ段で、$j+1<k$のときに$\theta_{j+1}(\vec e)$の最外の量化子が$\forall v_{i_{j+2}}$のままであることも確かめておく。$a_j$の最外の構成子は$\operatorname{AllRaw}(i_{j+2},\cdot)$であり、§E16.18 定義 3.3の改名の第3条件は$v_{i_{j+2}}$が代入する項に自由に現れることを含むが、$e_{j+1}$は閉項符号なのでこれは成り立たない。従って改名は発動せず、§E16.20 補題 7.2 (4)の$\operatorname{AllRaw}$の場合の等式により、束縛変数の添字は$i_{j+2}$のままである。以上により、代入をこの順序で行えば、途中の各段の符号も文の符号であり、各段で次に取り除く量化子の変数添字も定まる。

$PA$の内部で閉項符号$\vec e$を取り、$\Box_T\theta_0$を仮定する。$j$を$0$から$k-1$まで動かし、次の二段を順に適用する。

§E16.20 補題 7.4 (3)により、閉項符号$e_{j+1}$は$\theta_j(\vec e)$の量化子$\forall v_{i_{j+1}}$の本体へ自由に代入可能である。従って符号

は§E16.10 定義 1.1の論理公理スキーマのうち、定義 1.1で全称具体化の公理と呼んだものの置換例の符号であり、$PA$は$\operatorname{LogAx}(d_j(\vec e))$を証明する。

このことを確かめる。$y:=d_j(\vec e)$、$i:=i_{j+1}$とし、$\theta_j(\vec e)=\operatorname{AllRaw}(i,a)$と書く。§E16.18 定義 4.2 (2)は、$i,t,a,b\le y$を満たす$i,t,a,b$が存在して

が成り立つことを要求する。すなわち有界性も判定の一部である。$a$と$b=\theta_{j+1}(\vec e)$は$y$の真部分符号であり、$i$は$\operatorname{AllRaw}(i,a)$の成分であるから、§E16.20 補題 7.2 (1)により$i,a,b\le y$である。証人$t$については場合を分ける。

$\operatorname{Free}(a,i)$が成り立つ場合は$t:=e_{j+1}$を証人に取る。§E16.20 補題 7.4 (6)により$t\le\operatorname{SubTermCode}(a,i,t)=b\le y$である。

$\neg\operatorname{Free}(a,i)$が成り立つ場合、$e_{j+1}$は$y$の上界を超え得る。実際、代入する変数が本体に自由に現れなければ代入結果は本体と同じであり、$e_{j+1}$の大きさは結果に反映されない。そこで$t:=\operatorname{Zero}$を証人に取る。§E16.20 補題 7.4 (5)により$\operatorname{SubTermCode}(a,i,\operatorname{Zero})=a=b$であり、この場合は$\theta_{j+1}(\vec e)=\operatorname{SubTermCode}(a,i,e_{j+1})=a$でもあるから両者は一致する。$\operatorname{Zero}\le y$は次による。§E16.18 定義 1.1により$\operatorname{Zero}=\operatorname{Cons}(2,0)$であり、$y=\operatorname{ImpRaw}(\theta_j(\vec e),\theta_{j+1}(\vec e))$は先頭成分がタグ$8$の Cons 符号である。§E16.20 補題 4.1 (5)は$\operatorname{Cons}(a,t)=S\operatorname{pair}(a,t)$と$a<\operatorname{Cons}(a,t)$を与えるので、$\operatorname{pair}(2,0)=3$から$\operatorname{Zero}=4$であり、$8<y$から$9\le y$である。従って$\operatorname{Zero}\le y$である。$\operatorname{Term}(\operatorname{Zero})$と$\operatorname{FreeFor}(\operatorname{Zero},i,a)$は同補題の第2項と第3項による。

いずれの場合も、代入可能性は§E16.20 補題 7.4 (3)が与える。従って$PA$は判定の四条件をすべて確かめ、$\operatorname{LogAx}(d_j(\vec e))$を証明する。

長さ$1$の列$\operatorname{Cons}(\operatorname{Line}_T(1,d_j(\vec e),0,0,0,0),0)$を取る。末尾の論理式$d_j(\vec e)=\operatorname{ImpRaw}(\theta_j(\vec e),\theta_{j+1}(\vec e))$は文の符号である。実際、上で$\theta_j(\vec e)$と$\theta_{j+1}(\vec e)$がともに文の符号であることを示しており、§E16.20 補題 7.2 (2)が与える$\operatorname{Formula}(\operatorname{ImpRaw}(b,c))\leftrightarrow(\operatorname{Formula}(b)\land\operatorname{Formula}(c))$と$\operatorname{Free}(\operatorname{ImpRaw}(b,c),k')\leftrightarrow(\operatorname{Free}(b,k')\lor\operatorname{Free}(c,k'))$により、$\operatorname{Formula}(d_j(\vec e))$と$\forall k'\,\neg\operatorname{Free}(d_j(\vec e),k')$が従うからである。従って補題 4.1によりこの列は$T$証明であり、

である。この段の入力$\operatorname{Prov}_T(\theta_j(\vec e))$と合わせ、補題 4.2の第二の主張を$b:=\theta_j(\vec e)$、$c:=\theta_{j+1}(\vec e)$について適用すると$\operatorname{Prov}_T(\theta_{j+1}(\vec e))$を得る。

$j=k-1$の段を終えると$\operatorname{Prov}_T(\operatorname{inst}_{\chi}(\vec e))$である。特別な場合は、§E16.20 補題 7.4 (2)により$\operatorname{Num}(x_j)$が閉項符号であることから得る。▨

証明.(1)を示す。$PA$の内部で$x$を固定し、$y$に関する$PA$の帰納法を行う。

$y=0$の場合を見る。$\operatorname{Num}(0)=\operatorname{Zero}$は§E16.18 定義 3.1の基底節であり、$\operatorname{Num}$はパラメータ列が空の原始再帰であるから、§E16.20 補題 6.1 (2)によりこの閉じた等式は$PA$の定理である。また$PA$は$x+0=x$を証明するので$\operatorname{Num}(x+0)=\operatorname{Num}(x)$である。$T$は (Q4) の全称閉包$\forall v\,(v+0=v)$を証明するから、内部具体化を$x$に適用して$\operatorname{Prov}_T(\ulcorner\dot x+0=\dot x\urcorner)$を得る。

$y$から$Sy$へ進む段では、§E16.20 補題 7.4 (1)により$\operatorname{Num}(Sy)=\operatorname{Succ}(\operatorname{Num}(y))$であり、$PA$が証明する$x+Sy=S(x+y)$から$\operatorname{Num}(x+Sy)=\operatorname{Succ}(\operatorname{Num}(x+y))$である。次の三つを順に得る。

• $T$が証明する (Q5) の全称閉包$\forall v\forall w\,(v+Sw=S(v+w))$へ内部具体化を適用して、$\operatorname{Prov}_T(\ulcorner\dot x+S\dot y=S(\dot x+\dot y)\urcorner)$。
• 帰納法の仮定$\operatorname{Prov}_T(\ulcorner\dot x+\dot y=(x+y)^{\textstyle\cdot}\urcorner)$と、$T$が証明する$\forall v\forall w\,(v=w\to Sv=Sw)$への内部具体化、および補題 4.2により、$\operatorname{Prov}_T(\ulcorner S(\dot x+\dot y)=S\,(x+y)^{\textstyle\cdot}\urcorner)$。
• $T$が証明する等号の推移律$\forall u\forall v\forall w\,(u=v\to(v=w\to u=w))$への内部具体化と補題 4.2の二回の適用により、$\operatorname{Prov}_T(\ulcorner\dot x+S\dot y=S\,(x+y)^{\textstyle\cdot}\urcorner)$。

最後の符号は$\ulcorner\dot x+(Sy)^{\textstyle\cdot}=(x+Sy)^{\textstyle\cdot}\urcorner$に等しい。従って帰納法の段が閉じる。

(2)も同様である。$y=0$では (Q6)、$y$から$Sy$への段では (Q7)$\forall v\forall w\,(v\times Sw=(v\times w)+v)$への内部具体化を用い、第1項が与える加法の内部計算と等号の推移律を組み合わせる。

(3)を示す。$x\ne y$とする。$PA$は、$x\ne y$ならば$x<y$または$y<x$であることを証明する。$T$が証明する$\forall v\forall w\,(v\ne w\to w\ne v)$への内部具体化と補題 4.2により二つの場合は互いに移るので、$x<y$の場合を扱えばよい。$x$に関する$PA$の帰納法を行う。$x=0$かつ$0<y$ならば$PA$の内部で$y=Sy'$を満たす$y'$を取ることができ、§E16.20 補題 7.4 (1)により$\operatorname{Num}(y)=\operatorname{Succ}(\operatorname{Num}(y'))$である。$T$が証明する (Q1) の全称閉包$\forall v\,(Sv\ne0)$への内部具体化は$\operatorname{Prov}_T(\ulcorner\dot y\ne0\urcorner)$を与え、上の対称性を一度用いると$\operatorname{Prov}_T(\ulcorner0\ne\dot y\urcorner)$を得る。$x$から$Sx$へ進む段では、$Sx<y$から$y=Sy'$かつ$x<y'$であり、帰納法の仮定が$\operatorname{Prov}_T(\ulcorner\dot x\ne\dot y'\urcorner)$を与える。$T$が証明する (Q2) の対偶$\forall v\forall w\,(v\ne w\to Sv\ne Sw)$への内部具体化と補題 4.2により$\operatorname{Prov}_T(\ulcorner S\dot x\ne S\dot y'\urcorner)$を得る。§E16.20 補題 7.4 (1)により、これは$\operatorname{Prov}_T(\ulcorner(Sx)^{\textstyle\cdot}\ne\dot y\urcorner)$である。

(4)の前半を示す。$x\le y$ならば、§E16.15 定義 1.1の略記$v\le w:\Leftrightarrow\exists z\,(w=v+z)$により、$PA$の内部で$y=x+u$を満たす$u$を取ることができる。第1項により$\operatorname{Prov}_T(\ulcorner\dot x+\dot u=\dot y\urcorner)$である。同じ略記により、$T$は$\forall v\forall t\forall w\,(v+t=w\to v\le w)$を証明する。内部具体化を$(x,u,y)$へ適用し、補題 4.2を用いると$\operatorname{Prov}_T(\ulcorner\dot x\le\dot y\urcorner)$を得る。

(4)の後半では、$y<x$から$PA$の内部で$y+Sw=x$を満たす$w$を取る。第1項により$\operatorname{Prov}_T(\ulcorner\dot y+(Sw)^{\textstyle\cdot}=\dot x\urcorner)$である。$<$の略記の定義により$T$は$\forall t\forall v\forall w'\,(v+St=w'\to v<w')$を証明するので、内部具体化と補題 4.2により$\operatorname{Prov}_T(\ulcorner\dot y<\dot x\urcorner)$を得る。$PA\subseteq T$であるから、$T$は$\forall v\forall w'\,(w'<v\to\neg(v\le w'))$も証明する。同じ二段を適用すると$\operatorname{Prov}_T(\ulcorner\neg(\dot x\le\dot y)\urcorner)$を得る。

(5)の前半は、(4)の後半の証明の途中で得た$\operatorname{Prov}_T(\ulcorner\dot y<\dot x\urcorner)$と同じ議論であり、$x<y$から$y=x+Su$を満たす$u$を取り、第1項と$T$の定理$\forall v\forall t\forall w\,(v+St=w\to v<w)$への内部具体化を用いる。後半は、$PA\subseteq T$により$T$が$\forall v\forall w\,(w\le v\to\neg(v<w))$を証明することと、第4項の前半が与える$\operatorname{Prov}_T(\ulcorner\dot y\le\dot x\urcorner)$を合わせて得る。▨