Hilbert流の体系におけるGlivenkoの定理の証明について書きます.
論理学について知らない方でも読めるように書いたつもりなので, 知っている方は「証明の準備」の節から読んでください.
名前 $a,b,c,\ldots$
変項 $x,y,z,\ldots$
$n$項演算子 $f,g,h,\ldots$
$n$項述語 $F,G,H,\ldots$
零項真理函数 $\bot$
二項真理函数 $\to,\lor,\land$
量化子 $\forall,\exists$
${\to}(\varphi,\psi)$のことは$\varphi\to\psi$と書きます. $\lor,\land$についても同様です.
$\varphi\to\psi\to\chi$は$\varphi\to(\psi\to\chi)$を意味します.
結合の強さは$\{\forall,\exists\}>\{\lor,\land\}>\to$の順です. したがって, $(\exists\xi\varphi\lor\psi\to\chi)\to\forall\xi\varphi\to\chi\land\chi$は$(((\exists\xi\varphi)\lor\psi)\to\chi)\to((\forall\xi\varphi)\to(\chi\land\chi))$を意味します.
$\varphi\to\bot$を$\lnot\varphi$と略記する.
論理式$\varphi$に対し, $\varphi$の自由変項の集合を$fv(\varphi)$と表す. また, 変項$\xi$, 項$\tau$に対し, 「$\varphi$に自由変項として現れる$\xi$をすべて$\tau$に置き換えたもの」を$\varphi[\tau/\xi]$と書く.
自由変項とは, $\forall$などによって束縛されていないということです.
$fv(\varphi),\varphi[\tau/\xi]$のちゃんとした定義についてはronriなどを参照してください.
論理式$\varphi,\psi$に対し, $\varphi$と$\psi$が(文字列として)等しいことを$\varphi\equiv\psi$と書く.
この$\equiv$は$\mathbf{HM}$の記号ではなく, メタ数学の記号です. したがって, $\varphi\equiv\psi$は論理式ではありません. 後に出てくる$\vdash$なども同様です.
また, $\varphi\equiv\psi$において$()$の有無は無視することがあります.
$\varphi,\psi,\chi,\varphi_1,\varphi_2$を任意の論理式, $\xi,\zeta$を任意の変項, $\tau$を任意の項とする.
\begin{align}
&(S)&&(\varphi\to\psi\to\chi)\to(\varphi\to\psi)\to(\varphi\to\chi)\\
&(K)&&\varphi\to(\psi\to\varphi)\\
&(DI)&&\varphi_i\to\varphi_1\lor\varphi_2&&(i=1,2)\\
&(DE)&&(\varphi\to\chi)\to(\psi\to\chi)\to(\varphi\lor\psi\to\chi)\\
&(CI)&&\varphi\to\psi\to(\varphi\land\psi)\\
&(CE)&&\varphi_1\land\varphi_2\to\varphi_i&&(i=1,2)\\
&(UI)&&\forall\zeta(\psi\to\varphi[\zeta/\xi])\to(\psi\to\forall\xi\varphi)&&(\zeta\notin fv(\psi)\cup fv(\forall\xi\varphi))\\
&(UE)&&\forall\xi\varphi\to\varphi[\tau/\xi]\\
&(EI)&&\varphi[\tau/\xi]\to\exists\xi\varphi\\
&(EE)&&\forall\zeta(\varphi[\zeta/\xi]\to\psi)\to(\exists\xi\varphi\to\psi)&&(\zeta\notin fv(\psi)\cup fv(\forall\xi\varphi))
\end{align}
正確にはこれらは公理ではなく公理図式です. $\varphi$などに具体的な論理式を代入したものが公理となります.
\begin{align}
&(MP)&\varphi,\varphi\to\psi&\implies\psi\\
&(GEN)&\varphi[\zeta/\xi]&\implies\forall\xi\varphi
\end{align}
ただし, $\zeta$は$\forall\xi\varphi$および演繹の前提に自由変項として現れない.
\begin{align}
&(EFQ)&&\bot\to\varphi\\
&(DNE)&&\lnot\lnot\varphi\to\varphi
\end{align}
とし, $\mathbf{HJ}$は$\mathbf{HM}$に$(EFQ)$を公理として加えたもの, $\mathbf{HK}$は$\mathbf{HM}$に$(DNE)$を公理として加えたものと定める.
$\Gamma$を(0個以上の)論理式の列とする.
$\mathbf{HM}$における$\Gamma$から$\varphi$への演繹とは, 有限個の論理式からなる列$\varphi_1,\ldots,\varphi_n$であって, $\varphi_n\equiv\varphi$をみたし, 任意の$1\leq i\leq n$に対して以下のいずれかが成り立つものである.
$\mathbf{HM}$において$\Gamma$から$\varphi$への演繹が存在することを$\Gamma\vdash_{\mathbf{HM}}\varphi$と書く. $\mathbf{HJ},\mathbf{HK}$についても同様に定める.
$\Gamma\vdash_{\mathbf{HM}}\varphi$ならば$\Gamma\vdash_{\mathbf{HJ}}\varphi$や$\Gamma\vdash_{\mathbf{HK}}\varphi$が成り立ちます.
$\mathbf{HM}$における証明において欠かせない演繹定理について解説します.
任意の論理式列$\Gamma$, 論理式$\varphi,\psi$について以下が成り立つ.
\begin{align}
\Gamma\vdash_{\mathbf{HM}}\varphi\to\psi\iff\varphi,\Gamma\vdash_{\mathbf{HM}}\psi
\end{align}
また, $\mathbf{HJ},\mathbf{HK}$についても同様のことが成り立つ.
$\implies$の証明
$\Gamma$から$\varphi\to\psi$への演繹が$\varphi_1,\ldots,\varphi_n$ ($\varphi_n\equiv\varphi\to\psi$)であるとする. このとき,
$\varphi_1,\ldots,\varphi_{n-1},\varphi\to\psi,\varphi,\psi$
は$\varphi,\Gamma$から$\psi$への演繹である.
$\impliedby$の証明
はじめに証明の概略を述べる.
$\varphi$を$\mathbf{HM}$の定理とする.
任意の論理式列$\Gamma$, 論理式$\psi$について以下が成り立つ.
$\varphi,\Gamma\vdash_{\mathbf{HM}}\psi\iff\Gamma\vdash_{\mathbf{HM}}\psi$
$\impliedby$は自明. $\implies$を示す.
演繹定理より$\Gamma\vdash_{\mathbf{HM}}\varphi\to\psi$であり, $\Gamma$から$\varphi\to\psi$への演繹を$\varphi_1,\ldots,\varphi_m$, $\varphi$の証明を$\varphi^\prime_1,\ldots,\varphi^\prime_n$としたとき, $\varphi_1,\ldots,\varphi_{m-1},\varphi\to\psi,\varphi^\prime_1,\ldots,\varphi^\prime_{n-1},\varphi,\psi$が$\Gamma$から$\psi$への演繹である.
定理は公理のように用いても問題ないということです. この事実は以後断りなく用います.
Glivenkoの定理の証明に必要となる定理を証明します. 知っている方は流し読みしてください.
$\vdash_{\mathbf{HM}}\varphi\to\lnot\lnot\varphi$
$\varphi,\lnot\varphi\vdash_{\mathbf{HM}}\bot$を示せばよい.
\begin{align}
&1.&&\varphi&&(\text{前提})\\
&2.&&\lnot\varphi&&(\text{前提})\\
&3.&&\bot&&(1,2,MP)
\end{align}
$\vdash_{\mathbf{HM}}(\varphi\to\psi)\to(\lnot\psi\to\lnot\varphi)$
$\varphi\to\psi,\lnot\psi,\varphi\vdash_{\mathbf{HM}}\bot$を示せばよい.
\begin{align}
&1.&&\varphi&&(\text{前提})\\
&2.&&\varphi\to\psi&&(\text{前提})\\
&3.&&\psi&&(1,2,MP)\\
&4.&&\lnot\psi&&(\text{前提})\\
&5.&&\bot&&(3,4,MP)
\end{align}
$\vdash_{\mathbf{HM}}\lnot\lnot\lnot\varphi\to\lnot\varphi$
\begin{align} &1.&&\varphi\to\lnot\lnot\varphi&&(\text{定理2})\\ &2.&&(\varphi\to\lnot\lnot\varphi)\to(\lnot\lnot\lnot\varphi\to\lnot\varphi)&&(\text{定理3})\\ &3.&&\lnot\lnot\lnot\varphi\to\lnot\varphi&&(1,2,MP) \end{align}
$\vdash_{\mathbf{HM}}(\varphi\to\psi)\to(\lnot\lnot\varphi\to\lnot\lnot\psi)$
$\varphi\to\psi\vdash_{\mathbf{HM}}\lnot\lnot\varphi\to\lnot\lnot\psi$を示せばよい.
\begin{align}
&1.&&\varphi\to\psi&&(\text{前提})\\
&2.&&(\varphi\to\psi)\to(\lnot\psi\to\lnot\varphi)&&(\text{定理3})\\
&3.&&\lnot\psi\to\lnot\varphi&&(1,2,MP)\\
&4.&&(\lnot\psi\to\lnot\varphi)\to(\lnot\lnot\varphi\to\lnot\lnot\psi)&&(\text{定理3})\\
&5.&&\lnot\lnot\varphi\to\lnot\lnot\psi&&(3,4,MP)
\end{align}
$\vdash_{\mathbf{HM}}\varphi\to\psi\to\lnot(\varphi\to\lnot\psi)$
$\varphi,\psi,\varphi\to\lnot\psi\vdash_{\mathbf{HM}}\bot$を示せばよい.
\begin{align}
&1.&&\varphi&&(\text{前提})\\
&2.&&\varphi\to\lnot\psi&&(\text{前提})\\
&3.&&\lnot\psi&&(1,2,MP)\\
&4.&&\psi&&(\text{前提})\\
&5.&&\bot&&(3,4,MP)
\end{align}
$\vdash_{\mathbf{HM}}\lnot\lnot(\varphi\to\psi)\to(\lnot\lnot\varphi\to\lnot\lnot\psi)$
$\lnot\lnot(\varphi\to\psi),\lnot\lnot\varphi,\lnot\psi\vdash_{\mathbf{HM}}\bot$を示せばよい.
\begin{align}
&1.&&(\varphi\to\psi)\to(\lnot\lnot\varphi\to\lnot\lnot\psi)&&(\text{定理5})\\
&2.&&((\varphi\to\psi)\to(\lnot\lnot\varphi\to\lnot\lnot\psi))\to(\lnot\lnot(\varphi\to\psi)\to\lnot\lnot(\lnot\lnot\varphi\to\lnot\lnot\psi))&&(\text{定理5})\\
&3.&&\lnot\lnot(\varphi\to\psi)\to\lnot\lnot(\lnot\lnot\varphi\to\lnot\lnot\psi)&&(1,2,MP)\\
&4.&&\lnot\lnot(\varphi\to\psi)&&(\text{前提})\\
&5.&&\lnot\lnot(\lnot\lnot\varphi\to\lnot\lnot\psi)&&(3,4,MP)\\
&6.&&\lnot\lnot\varphi&&(\text{前提})\\
&7.&&\lnot\psi&&(\text{前提})\\
&8.&&\lnot\lnot\varphi\to\lnot\psi\to\lnot(\lnot\lnot\varphi\to\lnot\lnot\psi)&&(\text{定理6})\\
&9.&&\lnot\psi\to\lnot(\lnot\lnot\varphi\to\lnot\lnot\psi)&&(6,8,MP)\\
&10.&&\lnot(\lnot\lnot\varphi\to\lnot\lnot\psi)&&(7,9,MP)\\
&11.&&\bot&&(5,10,MP)
\end{align}
$\vdash_{\mathbf{HM}}\lnot(\varphi\to\psi)\to\lnot\psi$
$\vdash_{\mathbf{HJ}}\lnot(\varphi\to\psi)\to\lnot\lnot\varphi$
$\lnot(\varphi\to\psi),\psi\vdash_{\mathbf{HM}}\bot$を示せばよい.
\begin{align}
&1.&&\psi&&(\text{前提})\\
&2.&&\psi\to(\varphi\to\psi)&&(K)\\
&3.&&\varphi\to\psi&&(1,2,MP)\\
&4.&&\lnot(\varphi\to\psi)&&(\text{前提})\\
&5.&&\bot&&(3,4,MP)
\end{align}
$\lnot(\varphi\to\psi),\lnot\varphi\vdash_{\mathbf{HJ}}\bot$を示せばよい.
\begin{align}
&1.&&\bot\to\psi&&(EFQ)\\
&2.&&(\bot\to\psi)\to(\varphi\to(\bot\to\psi))&&(K)\\
&3.&&\varphi\to(\bot\to\psi)&&(1,2,MP)\\
&4.&&\varphi\to\bot&&(\text{前提})\\
&5.&&(\varphi\to(\bot\to\psi))\to(\varphi\to\bot)\to(\varphi\to\psi)&&(S)\\
&6.&&(\varphi\to\bot)\to(\varphi\to\psi)&&(3,5,MP)\\
&7.&&\varphi\to\psi&&(4,6,MP)\\
&8.&&\lnot(\varphi\to\psi)&&(\text{前提})\\
&9.&&\bot&&(7,8,MP)
\end{align}
$\vdash_{\mathbf{HJ}}(\lnot\lnot\varphi\to\lnot\lnot\psi)\to\lnot\lnot(\varphi\to\psi)$
$\lnot\lnot\varphi\to\lnot\lnot\psi,\lnot(\varphi\to\psi)\vdash_{\mathbf{HJ}}\varphi$を示せばよい.
\begin{align}
&1.&&\lnot(\varphi\to\psi)&&(\text{前提})\\
&2.&&\lnot(\varphi\to\psi)\to\lnot\psi&&(\text{定理8})\\
&3.&&\lnot\psi&&(1,2,MP)\\
&4.&&\lnot(\varphi\to\psi)\to\lnot\lnot\varphi&&(\text{定理8})\\
&5.&&\lnot\lnot\varphi&&(1,4,MP)\\
&6.&&\lnot\lnot\varphi\to\lnot\lnot\psi&&(\text{前提})\\
&7.&&\lnot\lnot\psi&&(5,6,MP)\\
&8.&&\bot&&(3,7,MP)
\end{align}
$\vdash_{\mathbf{HJ}}\lnot\lnot(\lnot\lnot\varphi\to\varphi)$
\begin{align} &1.&&\lnot\lnot\lnot\lnot\varphi\to\lnot\lnot\varphi&&(\text{定理4})\\ &2.&&(\lnot\lnot\lnot\lnot\varphi\to\lnot\lnot\varphi)\to\lnot\lnot(\lnot\lnot\varphi\to\varphi)&&(\text{定理9})\\ &3.&&\lnot\lnot(\lnot\lnot\varphi\to\varphi)&&(1,2,MP) \end{align}
$\vdash_{\mathbf{HK}}\bot\to\varphi$
$\bot\vdash_{\mathbf{HK}}\varphi$を示せばよい.
\begin{align}
&1.&&\bot&&(\text{前提})\\
&2.&&\bot\to(\lnot\varphi\to\bot)&&(K)\\
&3.&&\lnot\varphi\to\bot&&(1,2,MP)\\
&4.&&\lnot\lnot\varphi\to\varphi&&(DNE)\\
&5.&&\varphi&&(3,4,MP)
\end{align}
このことから$\Gamma\vdash_{\mathbf{HJ}}\varphi\implies\Gamma\vdash_{\mathbf{HK}}\varphi$が成り立ちます.
$\varphi,\psi,\chi,\varphi_1,\varphi_2$を任意の論理式, $\xi,\zeta$を任意の変項, $\tau$を任意の項とする.
\begin{align}
&(S)&&(\varphi\to\psi\to\chi)\to(\varphi\to\psi)\to(\varphi\to\chi)\\
&(K)&&\varphi\to(\psi\to\varphi)\\
&(DI)&&\varphi_i\to\varphi_1\lor\varphi_2&&(i=1,2)\\
&(DE)&&(\varphi\to\chi)\to(\psi\to\chi)\to(\varphi\lor\psi\to\chi)\\
&(CI)&&\varphi\to\psi\to(\varphi\land\psi)\\
&(CE)&&\varphi_1\land\varphi_2\to\varphi_i&&(i=1,2)\\
&(UI)&&\forall\zeta(\psi\to\varphi[\zeta/\xi])\to(\psi\to\forall\xi\varphi)&&(\zeta\notin fv(\psi)\cup fv(\forall\xi\varphi))\\
&(UE)&&\forall\xi\varphi\to\varphi[\tau/\xi]\\
&(EI)&&\varphi[\tau/\xi]\to\exists\xi\varphi\\
&(EE)&&\forall\zeta(\varphi[\zeta/\xi]\to\psi)\to(\exists\xi\varphi\to\psi)&&(\zeta\notin fv(\psi)\cup fv(\forall\xi\varphi))
\end{align}
\begin{align}
&(MP)&\varphi,\varphi\to\psi&\implies\psi\\
&(GEN)&\varphi[\zeta/\xi]&\implies\forall\xi\varphi
\end{align}
ただし, $\zeta$は$\forall\xi\varphi$および演繹の前提に自由変項として現れない.
\begin{align}
&(EFQ)&&\bot\to\varphi\\
&(DNE)&&\lnot\lnot\varphi\to\varphi
\end{align}
とし, $\mathbf{HJ}$は$\mathbf{HM}$に$(EFQ)$を公理として加えたもの, $\mathbf{HK}$は$\mathbf{HM}$に$(DNE)$を公理として加えたものと定める.
$n$項述語$\theta$, 項$\tau_1,\ldots,\tau_n$に対して$(\theta(\tau_1,\ldots,\tau_n))^*\equiv\theta(\tau_1,\ldots,\tau_n)$と定める.
論理式$\varphi$に対し, $\varphi^*$を以下のように帰納的に定める.
\begin{align}
(\varphi\to\psi)^*&\equiv\varphi^*\to\psi^*\\
(\varphi\lor\psi)^*&\equiv\varphi^*\lor\psi^*\\
(\varphi\land\psi)^*&\equiv\varphi^*\land\psi^*\\
\forall\xi\varphi^*&\equiv\forall\xi\lnot\lnot\varphi^*\\
\exists\xi\varphi^*&\equiv\exists\xi\varphi^*
\end{align}
また, 論理式列$\Gamma\equiv\varphi_1,\ldots,\varphi_n$に対し, $\Gamma^*\equiv{\varphi_1}^*,\ldots,{\varphi_n}^*$と定める.
$fv(\varphi^*)=fv(\varphi)$および$\varphi^*[\tau/\xi]\equiv(\varphi[\tau/\xi])^*$が成り立ちますが, ここでは証明しません.
任意の論理式列$\Gamma$, 論理式$\varphi$に対し,
$\Gamma\vdash_{\mathbf{HK}}\varphi\iff\Gamma^*\vdash_{\mathbf{HJ}}\lnot\lnot\varphi^*$
Glivenkoの定理を証明します.
まず, $\Gamma$が空列の場合に示せば十分であることを確認します.
定理7 $\vdash_{\mathbf{HM}}\lnot\lnot(\varphi\to\psi)\to(\lnot\lnot\varphi\to\lnot\lnot\psi)$および定理9 $\vdash_{\mathbf{HJ}}(\lnot\lnot\varphi\to\lnot\lnot\psi)\to\lnot\lnot(\varphi\to\psi)$を用いる.
$\Gamma\equiv\varphi_1,\ldots,\varphi_n$とすると, 演繹定理から
\begin{align}
\Gamma\vdash_{\mathbf{HK}}\varphi
&\iff\vdash_{\mathbf{HK}}\varphi_1\to\cdots\to\varphi_n\to\varphi\\
&\iff\vdash_{\mathbf{HJ}}\lnot\lnot(\varphi_1\to\cdots\to\varphi_n\to\varphi)^*\\
&\iff\vdash_{\mathbf{HJ}}\lnot\lnot({\varphi_1}^*\to\cdots\to{\varphi_n}^*\to\varphi^*)\\
&\iff\vdash_{\mathbf{HJ}}\lnot\lnot{\varphi_1}^*\to\cdots\to\lnot\lnot{\varphi_n}^*\to\lnot\lnot\varphi^*\\
&\implies\vdash_{\mathbf{HJ}}{\varphi_1}^*\to\cdots\to{\varphi_n}^*\to\lnot\lnot\varphi^*\\
&\iff\Gamma^*\vdash_{\mathbf{HJ}}\lnot\lnot\varphi^*
\end{align}
および
\begin{align}
\Gamma^*\vdash_{\mathbf{HJ}}\lnot\lnot\varphi^*
&\iff\vdash_{\mathbf{HJ}}{\varphi_1}^*\to\cdots\to{\varphi_n}^*\to\lnot\lnot\varphi^*\\
&\iff\vdash_{\mathbf{HJ}}(\varphi_1\to\cdots\to\varphi_n\to\lnot\lnot\varphi)^*\\
&\implies\vdash_{\mathbf{HJ}}\lnot\lnot(\varphi_1\to\cdots\to\varphi_n\to\lnot\lnot\varphi)^*\\
&\iff\vdash_{\mathbf{HK}}\varphi_1\to\cdots\to\varphi_n\to\lnot\lnot\varphi\\
&\iff\Gamma\vdash_{\mathbf{HK}}\lnot\lnot\varphi\\
&\iff\Gamma\vdash_{\mathbf{HK}}\varphi
\end{align}
となる.
任意の論理式$\varphi$に対し, $\vdash_{\mathbf{HK}}\varphi\to\varphi^*$かつ$\vdash_{\mathbf{HK}}\varphi^*\to\varphi$が成り立つ.
論理式$\varphi$に対し, $d(\varphi)\in\mathbb{N}\setminus\{0\}$を以下のように帰納的に定める.
$d(\varphi)$による帰納法で示す.
$d(\varphi)=1$のとき, $\varphi\equiv\theta(\tau_1,\ldots,\tau_n)$または$\varphi\equiv\bot$であり, どちらの場合でも$\varphi^*\equiv\varphi$であるため補題は成立する.
$d\geq 2$として, $d(\varphi)=1,\ldots,d-1$のときに補題が成立しているとする. $d(\varphi)=d$のときに補題が成立することを示す.
まず$\psi\to\chi,\psi^*\vdash_{\mathbf{HK}}\chi^*$を示す.
\begin{align}
&1.&&\psi^*&&(\text{前提})\\
&2.&&\psi^*\to\psi&&(\text{帰納法の仮定})\\
&3.&&\psi&&(1,2,MP)\\
&4.&&\psi\to\chi&&(\text{前提})\\
&5.&&\chi&&(3,4,MP)\\
&6.&&\chi\to\chi^*&&(\text{帰納法の仮定})\\
&7.&&\chi^*&&(5,6,MP)
\end{align}
演繹定理より$\vdash_{\mathbf{HK}}\varphi\to\varphi^*$である.
$\vdash_{\mathbf{HK}}\varphi^*\to\varphi$についても同様である.
\begin{align}
&1.&&\psi^*\to\psi^*\lor\chi^*&&(DI)\\
&2.&&(\psi^*\to\psi^*\lor\chi^*)\to(\psi\to(\psi^*\to\psi^*\lor\chi^*))&&(K)\\
&3.&&\psi\to(\psi^*\to\psi^*\lor\chi^*)&&(1,2,MP)\\
&4.&&\psi\to\psi^*&&(\text{帰納法の仮定})\\
&5.&&(\psi\to(\psi^*\to\psi^*\lor\chi^*))\to(\psi\to\psi^*)\to(\psi\to\psi^*\lor\chi^*)&&(S)\\
&6.&&(\psi\to\psi^*)\to(\psi\to\psi^*\lor\chi^*)&&(3,5,MP)\\
&7.&&\psi\to\psi^*\lor\chi^*&&(4,6,MP)\\
&8.&&\chi^*\to\psi^*\lor\chi^*&&(DI)\\
&9.&&(\chi^*\to\psi^*\lor\chi^*)\to(\chi\to(\chi^*\to\psi^*\lor\chi^*))&&(K)\\
&10.&&\chi\to(\chi^*\to\psi^*\lor\chi^*)&&(8,9,MP)\\
&11.&&\chi\to\chi^*&&(\text{帰納法の仮定})\\
&12.&&(\chi\to(\chi^*\to\psi^*\lor\chi^*))\to(\chi\to\chi^*)\to(\chi\to\psi^*\lor\chi^*)&&(S)\\
&13.&&(\chi\to\chi^*)\to(\chi\to\psi^*\lor\chi^*)&&(10,12,MP)\\
&14.&&\chi\to\psi^*\lor\chi^*&&(11,13,MP)\\
&15.&&(\psi\to\psi^*\lor\chi^*)\to(\chi\to\psi^*\lor\chi^*)\to(\psi\lor\chi\to\psi^*\lor\chi^*)&&(DE)\\
&16.&&(\chi\to\psi^*\lor\chi^*)\to(\psi\lor\chi\to\psi^*\lor\chi^*)&&(7,15,MP)\\
&17.&&\psi\lor\chi\to\psi^*\lor\chi^*&&(14,16,MP)
\end{align}
したがって$\vdash_{\mathbf{HK}}\varphi\to\varphi^*$である.
$\vdash_{\mathbf{HK}}\varphi^*\to\varphi$についても同様である.
まず$\psi\land\chi\vdash_{\mathbf{HK}}\psi^*\land\chi^*$を示す.
\begin{align}
&1.&&\psi\land\chi&&(\text{前提})\\
&2.&&\psi\land\chi\to\psi&&(CE)\\
&3.&&\psi&&(1,2,MP)\\
&4.&&\psi\to\psi^*&&(\text{帰納法の仮定})\\
&5.&&\psi^*&&(3,4,MP)\\
&6.&&\chi\land\chi\to\psi&&(CE)\\
&7.&&\chi&&(1,6,MP)\\
&8.&&\chi\to\chi^*&&(\text{帰納法の仮定})\\
&9.&&\chi^*&&(7,8,MP)\\
&10.&&\psi^*\to\chi^*\to\psi^*\land\chi^*&&(CI)\\
&11.&&\chi^*\to\psi^*\land\chi^*&&(5,10,MP)\\
&12.&&\psi^*\land\chi^*&&(9,11,MP)
\end{align}
演繹定理より$\vdash_{\mathbf{HK}}\varphi\to\varphi^*$である.
$\vdash_{\mathbf{HK}}\varphi^*\to\varphi$についても同様である.
まず$\forall\xi\psi\vdash_{\mathbf{HK}}\forall\xi\lnot\lnot\psi^*$を示す.
\begin{align}
&1.&&\forall\xi\psi&&(\text{前提})\\
&2.&&\forall\xi\psi\to\psi&&(UE)\\
&3.&&\psi&&(1,2,MP)\\
&4.&&\psi\to\psi^*&&(\text{帰納法の仮定})\\
&5.&&\psi^*&&(3,4,MP)\\
&6.&&\psi^*\to\lnot\lnot\psi^*&&(\text{定理2})\\
&7.&&\lnot\lnot\psi^*&&(5,6,MP)\\
&8.&&\forall\xi\lnot\lnot\psi^*&&(7,GEN)
\end{align}
演繹定理より$\vdash_{\mathbf{HK}}\varphi\to\varphi^*$である.
次に$\forall\xi\lnot\lnot\psi^*\vdash_{\mathbf{HK}}\forall\xi\psi$を示す.
\begin{align}
&1.&&\forall\xi\lnot\lnot\psi^*&&(\text{前提})\\
&2.&&\forall\xi\lnot\lnot\psi^*\to\lnot\lnot\psi^*&&(UE)\\
&3.&&\lnot\lnot\psi^*&&(1,2,MP)\\
&4.&&\lnot\lnot\psi^*\to\psi^*&&(DNE)\\
&5.&&\psi^*&&(3,4,MP)\\
&6.&&\psi^*\to\psi&&(\text{帰納法の仮定})\\
&7.&&\psi&&(5,6,MP)\\
&8.&&\forall\xi\psi&&(7,GEN)
\end{align}
演繹定理より$\vdash_{\mathbf{HK}}\varphi^*\to\varphi$である.
\begin{align}
&1.&&\psi\to\psi^*&&(\text{帰納法の仮定})\\
&2.&&\psi^*\to\exists\xi\psi^*&&(EI)\\
&3.&&(\psi^*\to\exists\xi\psi^*)\to(\psi\to\psi^*)\to(\psi\to\exists\xi\psi^*)&&(B)\\
&4.&&(\psi\to\psi^*)\to(\psi\to\exists\xi\psi^*)&&(2,3,MP)\\
&5.&&\psi\to\exists\xi\psi^*&&(1,4,MP)\\
&6.&&\forall\xi(\psi\to\exists\xi\psi^*)&&(5,GEN)\\
&7.&&\forall\xi(\psi\to\exists\xi\psi^*)\to(\exists\xi\psi\to\exists\xi\psi^*)&&(EE)\\
&8.&&\exists\xi\psi\to\exists\xi\psi^*&&(6,7,MP)
\end{align}
したがって$\vdash_{\mathbf{HK}}\varphi\to\varphi^*$である.
$\vdash_{\mathbf{HK}}\varphi^*\to\varphi$についても同様である.
$\vdash_{\mathbf{HJ}}\lnot\lnot\varphi^*$と仮定する. このとき, $\vdash_{\mathbf{HK}}\lnot\lnot\varphi^*$である.
\begin{align}
&1.&&\lnot\lnot\varphi^*&&(\text{仮定})\\
&2.&&\lnot\lnot\varphi^*\to\varphi^*&&(DNE)\\
&3.&&\varphi^*&&(1,2,MP)\\
&4.&&\varphi^*\to\varphi&&(\text{補題13})\\
&5.&&\varphi&&(3,4,MP)
\end{align}
したがって, $\vdash_{\mathbf{HK}}\varphi$である.
つづいて, $\vdash_{\mathbf{HK}}\varphi\implies\vdash_{\mathbf{HJ}}\lnot\lnot\varphi^*$を示します.
証明の概略は, 上で述べた演繹定理の証明と同じです.
$\varphi_1,\ldots,\varphi_n$が$\mathbf{HK}$における$\varphi$の証明であるとする. このとき, $\lnot\lnot{\varphi_1}^*,\ldots,\lnot\lnot{\varphi_n}^*$に適切に論理式を補充したものが$\mathbf{HJ}$における$\lnot\lnot\varphi^*$の証明である.
定理2 $\vdash_{\mathbf{HM}}\varphi\to\lnot\lnot\varphi$を思い出します.
以下は$\mathbf{HJ}$の定理である.
\begin{align}
&(S^*)&&\lnot\lnot((\varphi^*\to\psi^*\to\chi^*)\to(\varphi^*\to\psi^*)\to(\varphi^*\to\chi^*))\\
&(K^*)&&\lnot\lnot(\varphi^*\to(\psi^*\to\varphi^*))\\
&(DI^*)&&\lnot\lnot({\varphi_i}^*\to{\varphi_1}^*\lor{\varphi_2}^*)&&(i=1,2)\\
&(DE^*)&&\lnot\lnot((\varphi^*\to\chi^*)\to(\psi^*\to\chi^*)\to(\varphi^*\lor\psi^*\to\chi^*))\\
&(CI^*)&&\lnot\lnot(\varphi^*\to\psi^*\to(\varphi^*\land\psi^*))\\
&(CE^*)&&\lnot\lnot({\varphi_1}^*\land{\varphi_2}^*\to{\varphi_i}^*)&&(i=1,2)\\
&(UI^*)&&\lnot\lnot(\forall\zeta(\psi^*\to\varphi^*[\zeta/\xi])\to(\psi^*\to\forall\xi\varphi^*))&&(\zeta\notin fv(\psi)\cup fv(\forall\xi\varphi))\\
&(UE^*)&&\lnot\lnot(\forall\xi\varphi^*\to\varphi^*[\tau/\xi])\\
&(EI^*)&&\lnot\lnot(\varphi^*[\tau/\xi]\to\exists\xi\varphi^*)\\
&(EE^*)&&\lnot\lnot(\forall\zeta(\varphi^*[\zeta/\xi]\to\psi^*)\to(\exists\xi\varphi^*\to\psi^*))&&(\zeta\notin fv(\psi)\cup fv(\forall\xi\varphi))
\end{align}
$S^*$などはこの記事独自の記号です.
定理10 $\vdash_{\mathbf{HJ}}\lnot\lnot(\lnot\lnot\varphi\to\varphi)$を思い出します.
以下は$\mathbf{HJ}$の定理である.
\begin{align}
&(DNE^*)&&\lnot\lnot(\lnot\lnot\varphi^*\to\varphi^*)
\end{align}
つづいて, 定理7 $\vdash_{\mathbf{HJ}}\lnot\lnot(\varphi\to\psi)\to(\lnot\lnot\varphi\to\lnot\lnot\psi)$を思い出します.
以下は$\mathbf{HJ}$の定理である.
\begin{align}
&(MP^*)&&\lnot\lnot\varphi^*\to\lnot\lnot(\varphi^*\to\psi^*)\to\lnot\lnot\psi^*\\
&(GEN^*)&&\lnot\lnot\varphi^*[\zeta/\xi]\to\lnot\lnot\forall\xi\lnot\lnot\varphi^*
\end{align}
ただし, $\zeta$は$\forall\xi\varphi$および演繹の前提に自由変項として現れない.
演繹定理より$\lnot\lnot\varphi^*,\lnot\lnot(\varphi^*\to\psi^*)\vdash_{\mathbf{HJ}}\lnot\lnot\psi^*$を示せばよい.
\begin{align}
&1.&&\lnot\lnot\varphi^*&&(\text{前提})\\
&2.&&\lnot\lnot(\varphi^*\to\psi^*)&&(\text{前提})\\
&3.&&\lnot\lnot(\varphi^*\to\psi^*)\to(\lnot\lnot\varphi^*\to\lnot\lnot\psi^*)&&(\text{定理7})\\
&4.&&\lnot\lnot\varphi^*\to\lnot\lnot\psi^*&&(2,3,MP)\\
&5.&&\lnot\lnot\psi^*&&(1,4,MP)
\end{align}
演繹定理より$\lnot\lnot\varphi^*[\zeta/\xi]\vdash_{\mathbf{HJ}}\lnot\lnot\forall\xi\lnot\lnot\varphi^*$を示せばよい.
\begin{align}
&1.&&\lnot\lnot\varphi^*[\zeta/\xi]&&(\text{前提})\\
&2.&&\forall\xi\lnot\lnot\varphi^*&&(1,GEN)\\
&3.&&\forall\xi\lnot\lnot\varphi^*\to\lnot\lnot\forall\xi\lnot\lnot\varphi^*&&(\text{定理2})\\
&4.&&\lnot\lnot\forall\xi\lnot\lnot\varphi^*&&(2,3,MP)
\end{align}
これでGlivenkoの定理の証明の準備が整ったので証明をします.
$\varphi_1,\ldots,\varphi_n$が$\mathbf{HK}$における$\varphi$の証明であるとする.
$\varphi_1,\ldots,\varphi_n$が演繹の条件のうちどれをみたしているかで場合分けする.