証明論

1：翻訳は原子論理式に $\lnot\lnot$ を付け、$\lor$・$\exists$ を同じ変数を束縛する $\lnot,\land,\forall$ の組み合わせに置き換えるだけで、項にも量化する変数にも手を触れない。したがって、自由変数と代入可能性は変わらず、代入と翻訳の順序を入れ替えても同じ論理式になる。$A$ の組み立てについての帰納法で、各場合の定義を見比べれば確かめられる。
2：論理記号の個数についての帰納法で示す。要点は、原子論理式・$\lor$・$\exists$ の 3 つの場合に古典論理の同値 $\lnot\lnot P\leftrightarrow P$、$(B\lor C)\leftrightarrow\lnot(\lnot B\land\lnot C)$、$\exists x\,B\leftrightarrow\lnot\forall x\,\lnot B$ を使い、ほかの場合は帰納法の仮定の同値を部分に当てはめることである。

$A$ の論理記号の個数についての帰納法で、場合を分ける。

• $A$ が $\bot$ 以外の原子論理式：$A^N=\lnot\lnot A$ で、$\lnot\lnot\lnot\lnot A\to\lnot\lnot A$ は (ii) で $B:=\lnot A$ としたものである。
• $A=\bot$：$\bot$ を仮定し $\lnot\mathrm I$ でそれを外すと $\vdash_{\mathrm i}\lnot\bot$ である。$\lnot\lnot\bot$ を仮定すると $\lnot\mathrm E$ で $\bot$ が出る。
• $A$ が $\lnot B$、$B\lor C$、$\exists x\,B$：$A^N$ はある式 $D$ の否定 $\lnot D$ であり、$\lnot\lnot\lnot D\to\lnot D$ は (ii) である。
• $A=B\land C$：$\lnot\lnot(B^N\land C^N)$ を仮定する。$\land\mathrm E$ と $\to\mathrm I$ で得られる $B^N\land C^N\to B^N$ に (iv) を使って $\lnot\lnot B^N$、帰納法の仮定で $B^N$ を得る。$C^N$ も同じで、$\land\mathrm I$ で $B^N\land C^N$ である。
• $A=B\to C$：$\lnot\lnot(B^N\to C^N)$ と $B^N$ を仮定する。仮定 $B^N$ のもとで $(B^N\to C^N)\to C^N$ が導出できるので、(iv) により $\lnot\lnot C^N$、帰納法の仮定により $C^N$ を得る。$\to\mathrm I$ で $B^N$ を外す。
• $A=\forall x\,B(x)$：$\lnot\lnot\forall x\,B^N(x)$ を仮定し、$A$ に現れない定数記号 $a$ をとる。$\forall\mathrm E$ と $\to\mathrm I$ で得られる $\forall x\,B^N(x)\to B^N(a)$ に (iv) を使うと $\lnot\lnot B^N(a)$ である。$B(a)$ は $A$ より論理記号が少なく、lem-pt-basic の 1 により $(B(a))^N=B^N(a)$ なので、帰納法の仮定により $B^N(a)$ を得る。開いた仮定 $\lnot\lnot\forall x\,B^N(x)$ にも結論にも $a$ は現れないので、$\forall\mathrm I$ で $\forall x\,B^N(x)$ を得る。
  どの場合も最後に $\to\mathrm I$ で $\lnot\lnot A^N$ を外せばよい。$\square$

$\Rightarrow$：$\mathbf{NK}$ のすべての導出 $D$ について $\mathrm{Open}(D)^N\vdash_{\mathrm i}\mathrm{concl}(D)^N$ を、$D$ の組み立てに沿った帰納法で示す。各場合に $\mathbf{NJ}$ の導出を具体的に組み立てるので、この証明が求める手続きを与える。以下 $\Delta_j:=\mathrm{Open}(D_j)^N$ と書く。古典論理に固有の規則と、翻訳で形の変わる規則が要所である。

• $\bot_{\mathrm C}$：$D_1$ は $\bot$ の導出で、帰納法の仮定により $\Delta_1\vdash_{\mathrm i}\bot$ である。$(\lnot A)^N=\lnot A^N$ なので、$\lnot\mathrm I$ で仮定 $\lnot A^N$ を外すと $\lnot\lnot A^N$ が得られ、lem-pt-stable により $A^N$ を得る。開いた仮定は $\mathrm{Open}(D)^N$ に含まれる。
• $\lor\mathrm E$：帰納法の仮定により、$\Delta_1\vdash_{\mathrm i}\lnot(\lnot A^N\land\lnot B^N)$、仮定 $A^N$ を加えて $C^N$、仮定 $B^N$ を加えて $C^N$ が導出できる。$\lnot C^N$ を仮定すると、2 つ目と 3 つ目から $\lnot\mathrm E$ と $\lnot\mathrm I$ で $\lnot A^N$ と $\lnot B^N$ が得られ、$\land\mathrm I$ と 1 つ目から $\bot$ が出る。$\lnot\mathrm I$ で $\lnot C^N$ を外して $\lnot\lnot C^N$、lem-pt-stable で $C^N$ を得る。
• $\exists\mathrm E$：帰納法の仮定により、$\Delta_1\vdash_{\mathrm i}\lnot\forall x\,\lnot A^N(x)$ であり、仮定 $A^N(a)$ を加えて $C^N$ が導出できる。$\lnot C^N$ を仮定すると、2 つ目から $\lnot\mathrm I$ で $\lnot A^N(a)$ が得られる。このときの開いた仮定は、$A(a)$ 以外の開いた仮定の翻訳と $\lnot C^N$ で、$a$ はどれにも現れない（固有変数の条件と lem-pt-basic の 1）。$\forall\mathrm I$ で $\forall x\,\lnot A^N(x)$ を得て、1 つ目と $\lnot\mathrm E$ で $\bot$ が出る。あとは $\lor\mathrm E$ と同じく $\lnot\lnot C^N$ から $C^N$ を得る。
  残りの規則は、翻訳が規則の形をそのまま保つか、短い導出で置き換えられる。
  残りの場合を開く

  葉（仮定 $A$ 1 つ）では $\{A^N\}\vdash_{\mathrm i}A^N$ である。$\land\mathrm I$、$\land\mathrm E$、$\to\mathrm I$、$\to\mathrm E$、$\lnot\mathrm I$、$\lnot\mathrm E$ は、翻訳が $\land,\to,\lnot$ と交換するので、帰納法の仮定に同じ規則を使えばよい（$\to\mathrm I$・$\lnot\mathrm I$ で外す仮定は $A^N$ になる）。$\bot_{\mathrm I}$：$\bot^N=\bot$ なので、$\bot_{\mathrm I}$ で $A^N$ を得る。$\lor\mathrm I$：$A^N$ から $\lnot(\lnot A^N\land\lnot B^N)$ を導く。$\lnot A^N\land\lnot B^N$ を仮定し、$\land\mathrm E$ で $\lnot A^N$、$\lnot\mathrm E$ で $\bot$、$\lnot\mathrm I$ で仮定を外す。$\forall\mathrm E$：lem-pt-basic の 1 により $(A(t))^N=A^N(t)$ なので、$\forall\mathrm E$ をそのまま使う。$\forall\mathrm I$：翻訳は定数記号を増やさないので、固有変数 $a$ は $\Delta_1$ にも $\forall x\,A^N(x)$ にも現れず、$\forall\mathrm I$ をそのまま使える。$\exists\mathrm I$：$A^N(t)$ から $\lnot\forall x\,\lnot A^N(x)$ を導く。$\forall x\,\lnot A^N(x)$ を仮定し、$\forall\mathrm E$ で $\lnot A^N(t)$、$\lnot\mathrm E$ で $\bot$、$\lnot\mathrm I$ で仮定を外す。

  
  結論 $A$ の導出で $\mathrm{Open}(D)\subset\Gamma$ なら $\mathrm{Open}(D)^N\subset\Gamma^N$ なので、$\Gamma^N\vdash_{\mathrm i}A^N$ である。
  $\Leftarrow$：$\Gamma^N\vdash_{\mathrm i}A^N$ なら $\Gamma^N\vdash_{\mathrm c}A^N$ である。lem-pt-basic の 2 により、$\Gamma$ の各元 $\gamma$ から $\gamma^N$ が、$A^N$ から $A$ が $\mathbf{NK}$ で導出できるので、導出をつなげて $\Gamma\vdash_{\mathrm c}A$ を得る。$\square$

$\bot^N=\bot$ なので、thm-pt-negative を $A:=\bot$ に使うと、$\Gamma\vdash_{\mathrm c}\bot\iff\Gamma^N\vdash_{\mathrm i}\bot$ である。導出を移す手続きは thm-pt-negative の後半による。$\square$

lem-pt-basic の 1 により、翻訳は全称化・代入と交換する。公理ごとに確かめる。以下、$a,b,\dots$ は新しい定数記号で、最後に $\to\mathrm I$ と $\forall\mathrm I$ で全称化する。

• 帰納法の公理：$\varphi$ についての帰納法の公理の翻訳は、$\varphi^N$ についての帰納法の公理そのものである。$\varphi^N$ も $L_A$ の論理式なので、これは $\mathrm{Ax}$ の元である。
  ほかの公理は、もとの公理から (i)〜(iv) と短い推論で得られる。
  公理ごとの導出を開く

  • (E1)、公理 2・4・5・6・7：$\forall\vec x\,B$（$B$ は原子論理式かその否定）の翻訳は $\forall\vec x\,\lnot\lnot B$ か $\forall\vec x\,\lnot\lnot\lnot B'$ で、もとの公理から (i) で得られる。
  • 公理 1：$Sa=Sb\to a=b$ に (iv) を使うと $\lnot\lnot Sa=Sb\to\lnot\lnot a=b$ である。
  • (E2)：翻訳は $\lnot\lnot a=b\to(\varphi^N(a,\vec c)\to\varphi^N(b,\vec c))$ の全称化である。$\lnot\lnot a=b$ と $\varphi^N(a,\vec c)$ を仮定する。lem-pt-stable により $\lnot\lnot\varphi^N(b,\vec c)$ を示せばよい。$\lnot\varphi^N(b,\vec c)$ を仮定すると、$\varphi^N$ についての (E2)（$\varphi^N$ も自由変数が $x,\vec u$ の中にある $L_A$ の論理式で、lem-pt-basic の 1 により $y$ は $\varphi^N$ の $x$ に代入可能なので、これも $\mathrm{Ax}$ の元である）から、$a=b$ を仮定すれば $\varphi^N(b,\vec c)$ が出て矛盾するので $\lnot a=b$ であり、$\lnot\lnot a=b$ と矛盾する。
  • 公理 3：翻訳は $\lnot\lnot\lnot a=0\to\lnot\forall y\,\lnot\lnot\lnot a=Sy$ の全称化である。(ii) により $\lnot a=0$、公理 3 により $\exists y\,a=Sy$ を得る。$\forall y\,\lnot\lnot\lnot a=Sy$ を仮定すると、$\exists\mathrm E$ で $a=Sb$ をとり、$\forall\mathrm E$ と (ii) で $\lnot a=Sb$ となって $\bot$ が出る。$\lnot\mathrm I$ で仮定を外す。
  • 公理 8：$C(z):=(Sz+a=b)$ とおくと、翻訳は $\bigl(\lnot\lnot a< b\to\lnot\forall z\,\lnot\lnot\lnot C(z)\bigr)\land\bigl(\lnot\forall z\,\lnot\lnot\lnot C(z)\to\lnot\lnot a< b\bigr)$ の全称化である。(ii) と (i) により $\forall z\,\lnot\lnot\lnot C(z)$ と $\forall z\,\lnot C(z)$ は $\mathbf{NJ}$ で同値なので、その形で示す。前半：$\forall z\,\lnot C(z)$ と $a< b$ を仮定すると、公理 8 から $\exists z\,C(z)$、$\exists\mathrm E$ で矛盾するので $\lnot a< b$ であり、$\lnot\lnot a< b$ と矛盾する。よって $\lnot\lnot a< b$ から $\lnot\forall z\,\lnot C(z)$ が出る。後半：$\lnot a< b$ を仮定すると、公理 8 の右から左の向きにより、どの $C(d)$（$d$ は新しい定数記号）からも $\exists\mathrm I$ で $a< b$ が出て矛盾するので $\forall z\,\lnot C(z)$ が得られ、仮定 $\lnot\forall z\,\lnot C(z)$ と矛盾する。
  
  どの場合も、使ったのは $\mathrm{Ax}$ の元と $\mathbf{NJ}$ の規則だけである。$\square$

$\mathsf{PA}\vdash\sigma$ なら、開いた仮定が $\mathrm{Ax}$ の有限個の元 $\gamma_1,\dots,\gamma_k$ である $\mathbf{NK}$ の導出がある。thm-pt-negative により $\{\gamma_1^N,\dots,\gamma_k^N\}\vdash_{\mathrm i}\sigma^N$ であり、$\to\mathrm I$ を $k$ 回使うと、開いた仮定のない $\gamma_1^N\to(\gamma_2^N\to\cdots(\gamma_k^N\to\sigma^N)\cdots)$ の $\mathbf{NJ}$ の導出が得られる。lem-pt-ha-axioms により各 $\gamma_j^N$ は $\mathsf{HA}$ で導出できるので、$\to\mathrm E$ を $k$ 回使って $\mathsf{HA}\vdash\sigma^N$ を得る。
$\sigma:=\bot$ とすると $\bot^N=\bot$ なので、$\mathsf{PA}\vdash\bot$ なら $\mathsf{HA}\vdash\bot$ である。lem-pt-ha-axioms の各導出は公理ごとに具体的に書け、thm-pt-negative の変換は計算可能なので、$\mathsf{PA}$ からの $\bot$ の導出を $\mathsf{HA}$ からの $\bot$ の導出に移す手続きが得られる。$\square$