黒田の二重否定翻訳

どれも数行の導出である。4 の右から左だけが $\bot_{\mathrm I}$（矛盾からは何でも出る）を使う。

1：翻訳は $\forall x$ の直後に $\lnot\lnot$ を入れるだけで、項にも量化する変数にも触れないので、$A$ の組み立てについての帰納法で各場合の定義を見比べればよい。2：$A$ の論理記号の個数についての帰納法で $\vdash_{\mathrm c}A\leftrightarrow A^{\ast}$ を示す。原子論理式と $\bot$ では両辺が同じで、$\lnot,\land,\lor,\to,\exists$ では帰納法の仮定の同値を部分に当てはめればよい。$\forall x\,B(x)$ では、$A$ に現れない定数記号 $a$ をとると、帰納法の仮定と 1 により $\vdash_{\mathrm c}B(a)\leftrightarrow B^{\ast}(a)$ で、古典論理では $\vdash_{\mathrm c}B^{\ast}(a)\leftrightarrow\lnot\lnot B^{\ast}(a)$ である（右から左は $\bot_{\mathrm C}$ による）。$\forall\mathrm E$ と $\forall\mathrm I$ で $\forall x\,B(x)\leftrightarrow\forall x\,\lnot\lnot B^{\ast}(x)$ を得る。$A^{\mathrm K}$ については、さらに $\vdash_{\mathrm c}A^{\ast}\leftrightarrow\lnot\lnot A^{\ast}$ を合わせる。$\square$

(a)⇒(b) が本体である。$\mathbf{NK}$ のすべての導出 $D$ について $\mathrm{Open}(D)^{\ast}\vdash_{\mathrm i}\lnot\lnot\mathrm{concl}(D)^{\ast}$ を、$D$ の組み立てに沿った帰納法で示す。各場合に $\mathbf{NJ}$ の導出を具体的に組み立てるので、これが求める手続きを与える。前提の導出を $D_1,D_2,\dots$ とし、$\Delta_j:=\mathrm{Open}(D_j)^{\ast}$ と書く。帰納法の仮定は $\Delta_j\vdash_{\mathrm i}\lnot\lnot\mathrm{concl}(D_j)^{\ast}$ である。外した仮定を除いた後の開いた仮定は、いつも $\mathrm{Open}(D)^{\ast}$ に含まれることに注意する。

• $\bot_{\mathrm C}$：$D_1$ は仮定 $\lnot A$ を外す前の $\bot$ の導出である。$(\lnot A)^{\ast}=\lnot A^{\ast}$ なので、帰納法の仮定は $\Delta_1\vdash_{\mathrm i}\lnot\lnot\bot$、lem-knt-dn の 1 で $\Delta_1\vdash_{\mathrm i}\bot$ である。$\Delta_1\setminus\{\lnot A^{\ast}\}$ から、$\lnot\mathrm I$ で仮定 $\lnot A^{\ast}$ を外して $\lnot\lnot A^{\ast}$ を得る。古典論理に固有の規則は、外側の $\lnot\lnot$ にそのまま吸収される。
• $\forall\mathrm E$：$D_1$ の結論は $\forall x\,B(x)$ で、帰納法の仮定は $\Delta_1\vdash_{\mathrm i}\lnot\lnot\forall x\,\lnot\lnot B^{\ast}(x)$ である。lem-knt-dn の 5 で $\forall x\,\lnot\lnot B^{\ast}(x)$、$\forall\mathrm E$ と lem-knt-basic の 1 で $\lnot\lnot B^{\ast}(t)=\lnot\lnot(B(t))^{\ast}$ を得る。全称記号の直後の $\lnot\lnot$ がここで使われる。
• $\forall\mathrm I$：$D_1$ の結論は $B(a)$ で、$a$ は $\mathrm{Open}(D_1)$ にも $\forall x\,B(x)$ にも現れない。帰納法の仮定は $\Delta_1\vdash_{\mathrm i}\lnot\lnot B^{\ast}(a)$ で、翻訳は定数記号を増やさないので $a$ は $\Delta_1$ にも $\forall x\,\lnot\lnot B^{\ast}(x)$ にも現れない。$\forall\mathrm I$ で $\forall x\,\lnot\lnot B^{\ast}(x)$、lem-knt-dn の 1 で $\lnot\lnot\forall x\,\lnot\lnot B^{\ast}(x)$ を得る。
• $\to\mathrm I$：$D_1$ は仮定 $B$ を外す前の $C$ の導出である。帰納法の仮定 $\Delta_1\vdash_{\mathrm i}\lnot\lnot C^{\ast}$ と $\to\mathrm I$ で、$\Delta_1\setminus\{B^{\ast}\}\vdash_{\mathrm i}B^{\ast}\to\lnot\lnot C^{\ast}$ である。lem-knt-dn の 2 により $\{B^{\ast}\to\lnot\lnot C^{\ast},\lnot\lnot B^{\ast}\}\vdash_{\mathrm i}\lnot\lnot C^{\ast}$ なので、$\lnot\lnot B^{\ast}\to\lnot\lnot C^{\ast}$ が導け、lem-knt-dn の 4 で $\lnot\lnot(B^{\ast}\to C^{\ast})$ を得る。
• $\exists\mathrm E$：$D_1$ の結論は $\exists x\,B(x)$、$D_2$ は仮定 $B(a)$ を外す前の $C$ の導出で、$a$ は $\exists x\,B(x)$、$C$、$B(a)$ 以外の $\mathrm{Open}(D_2)$ の元に現れない。帰納法の仮定は $\Delta_1\vdash_{\mathrm i}\lnot\lnot\exists x\,B^{\ast}(x)$ と $\Delta_2\vdash_{\mathrm i}\lnot\lnot C^{\ast}$ で、lem-knt-basic の 1 により $B(a)^{\ast}=B^{\ast}(a)$ であり、固有変数の条件は翻訳の後も成り立つ。$\exists\mathrm E$（結論 $\lnot\lnot C^{\ast}$）で $\{\exists x\,B^{\ast}(x)\}\cup(\Delta_2\setminus\{B^{\ast}(a)\})\vdash_{\mathrm i}\lnot\lnot C^{\ast}$、lem-knt-dn の 2 で $\exists x\,B^{\ast}(x)$ を $\lnot\lnot\exists x\,B^{\ast}(x)$ に替え、$\Delta_1$ からの導出をつなぐ。
  残りの規則は短い導出で済む。
  残りの場合を開く

  葉（仮定 $A$ 1 つ）では $\{A^{\ast}\}\vdash_{\mathrm i}\lnot\lnot A^{\ast}$（lem-knt-dn の 1）。$\land\mathrm I$：$\lnot\lnot B^{\ast}$ と $\lnot\lnot C^{\ast}$ から lem-knt-dn の 3 で $\lnot\lnot(B^{\ast}\land C^{\ast})$。$\land\mathrm E$：$\lnot\lnot(B^{\ast}\land C^{\ast})$ から同じく $\lnot\lnot B^{\ast}$（$C^{\ast}$ も同じ）。$\to\mathrm E$：$\lnot\lnot(B^{\ast}\to C^{\ast})$ と $\lnot\lnot B^{\ast}$ から lem-knt-dn の 4 で $\lnot\lnot C^{\ast}$。$\lnot\mathrm I$：仮定 $B^{\ast}$ を加えて $\lnot\lnot\bot$、lem-knt-dn の 1 で $\bot$、$\lnot\mathrm I$ で $\lnot B^{\ast}$、さらに 1 で $\lnot\lnot\lnot B^{\ast}$。$\lnot\mathrm E$：$\lnot\lnot\lnot B^{\ast}$ から 1 で $\lnot B^{\ast}$。$\Delta=\{\lnot B^{\ast}\}$、$C=\bot$ として 2 を使うと、$\{\lnot B^{\ast},B^{\ast}\}\vdash_{\mathrm i}\bot\vdash_{\mathrm i}\lnot\lnot\bot$ から $\{\lnot B^{\ast},\lnot\lnot B^{\ast}\}\vdash_{\mathrm i}\lnot\lnot\bot$。$\bot_{\mathrm I}$：$\lnot\lnot\bot$ から 1 で $\bot$、$\bot_{\mathrm I}$ で $\lnot\lnot A^{\ast}$。$\lor\mathrm I$：$B^{\ast}\vdash_{\mathrm i}B^{\ast}\lor C^{\ast}\vdash_{\mathrm i}\lnot\lnot(B^{\ast}\lor C^{\ast})$ に 2 を当てる。$\lor\mathrm E$：仮定 $B^{\ast}$ と $C^{\ast}$ のもとの $\lnot\lnot E^{\ast}$ の導出から、$\lor\mathrm E$（結論 $\lnot\lnot E^{\ast}$）で $B^{\ast}\lor C^{\ast}$ から $\lnot\lnot E^{\ast}$、2 で $\lnot\lnot(B^{\ast}\lor C^{\ast})$ に替える。$\exists\mathrm I$：$B^{\ast}(t)\vdash_{\mathrm i}\exists x\,B^{\ast}(x)\vdash_{\mathrm i}\lnot\lnot\exists x\,B^{\ast}(x)$ に 2 を当てる。

  
  結論 $A$ の導出で $\mathrm{Open}(D)\subset\Gamma$ なら $\mathrm{Open}(D)^{\ast}\subset\Gamma^{\ast}$ なので、(b) が成り立つ。
  (b)⇒(c)：(b) の導出が使う $\Gamma^{\ast}$ の元を $\gamma_1^{\ast},\dots,\gamma_n^{\ast}$ とする。lem-knt-dn の 2 を $n$ 回当てると $\{\lnot\lnot\gamma_1^{\ast},\dots,\lnot\lnot\gamma_n^{\ast}\}\vdash_{\mathrm i}\lnot\lnot A^{\ast}$ で、これは (c) である。
  (c)⇒(a)：(c) の導出は $\mathbf{NK}$ の導出でもある。lem-knt-basic の 2 により $\Gamma$ の各元 $\gamma$ から $\gamma^{\mathrm K}$ が、$A^{\mathrm K}$ から $A$ が $\mathbf{NK}$ で導出できるので、導出をつなげて (a) を得る。$\square$

全称記号を含まない文では $\gamma^{\ast}=\gamma$、$A^{\ast}=A$ なので、thm-knt-main の (a)⇔(b) そのものである。$\square$

$\bot^{\ast}=\bot$ なので、thm-knt-main により $\Gamma\vdash_{\mathrm c}\bot\iff\Gamma^{\ast}\vdash_{\mathrm i}\lnot\lnot\bot$ である。lem-knt-dn の 1 により $\lnot\lnot\bot$ と $\bot$ は $\mathbf{NJ}$ で互いに導出できる。$\square$

$A$ の論理記号の個数についての帰納法で $\vdash_{\mathrm i}A^N\leftrightarrow\lnot\lnot A^{\ast}$ を示す。$\mathbf{NJ}$ で成り立つ同値 $\lnot(X\lor Y)\leftrightarrow\lnot X\land\lnot Y$ と $\lnot\exists x\,X(x)\leftrightarrow\forall x\,\lnot X(x)$ を使う。

要点は、$\mathbf{NJ}+\mathrm{DNS}$ ではすべての文 $B$ について $\lnot\lnot B^{\ast}\dashv\vdash_{\mathrm{dns}}\lnot\lnot B$ となることである。これを認めると、(⇒) は thm-knt-main の (b) と、$\gamma\vdash\lnot\lnot\gamma\vdash_{\mathrm{dns}}\lnot\lnot\gamma^{\ast}$ と lem-knt-dn の 2 から $\Gamma\vdash_{\mathrm{dns}}\lnot\lnot A^{\ast}\vdash_{\mathrm{dns}}\lnot\lnot A$ となる。(⇐) は、DNS の各文が $\mathbf{NK}$ で導出でき（lem-knt-basic の 2 と同じ考えで、$\lnot\lnot$ を外せばよい）、$\lnot\lnot A\vdash_{\mathrm c}A$ であることによる。