3
大学数学基礎解説
文献あり

Glivenkoの定理

239
0
$$\newcommand{sgn}[0]{\operatorname{sgn}} $$

Hilbert流の体系におけるGlivenkoの定理の証明について書きます.
論理学について知らない方でも読めるように書いたつもりなので, 知っている方は「証明の準備」の節から読んでください.

定義

HMの記号

名前 $a,b,c,\ldots$
変項 $x,y,z,\ldots$
$n$項演算子 $f,g,h,\ldots$
$n$項述語 $F,G,H,\ldots$
零項真理函数 $\bot$
二項真理函数 $\to,\lor,\land$
量化子 $\forall,\exists$

一階述語論理の項
  • $\alpha$が名前ならば$\alpha$は項である.
  • $\xi$が変項ならば$\xi$は項である.
  • $\omicron$$n$項演算子で$\tau_1,\ldots,\tau_n$が項ならば$\omicron(\tau_1,\ldots,\tau_n)$は項である.
  • 上記以外は項ではない.
一階述語論理の論理式
  • $\theta$$n$項述語で$\tau_1,\ldots,\tau_n$が項ならば$\theta(\tau_1,\ldots,\tau_n)$は論理式である.
  • $\rho$$n$項真理函数で$\varphi_1,\ldots,\varphi_n$が論理式ならば$\rho(\varphi_1,\ldots,\varphi_n)$は論理式である.
  • $\xi$が変項で$\varphi$が論理式ならば$\forall\xi\varphi,\exists\xi\varphi$は論理式である.
  • 上記以外は論理式ではない.

${\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$において$()$の有無は無視することがあります.

HMの公理

$\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$などに具体的な論理式を代入したものが公理となります.

HMの推論規則

\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$に対して以下のいずれかが成り立つものである.

  • $\varphi_i$$\mathbf{HM}$の公理である.
  • $\varphi_i$$\Gamma$に含まれる.
  • $i$未満の整数$j,k$が存在し, $\varphi_i$$\varphi_j,\varphi_k$から推論規則$(MP)$によって導かれる.
  • $i$未満の整数$j$が存在し, $\varphi_i$$\varphi_j$から推論規則$(GEN)$によって導かれる.
$\Gamma$をこの演繹における前提という. また, $\Gamma$が空列のときの演繹を証明という. $\mathbf{HM}$における$\varphi$の証明が存在するとき, $\varphi$$\mathbf{HM}$定理とよぶ.
$\mathbf{HJ},\mathbf{HK}$についても同様に定める.

$\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_1,\ldots,\varphi_n$$\varphi,\Gamma$から$\psi$への演繹であるとする. このとき, $\varphi\to\varphi_1,\ldots,\varphi\to\varphi_n$に適切に論理式を補充したものが$\Gamma$から$\varphi\to\psi$への演繹である.

まず, $\vdash_{\mathbf{HM}}\varphi\to\varphi$を示す. 以下が証明である.
\begin{align} &1.&&\varphi\to(\varphi\to\varphi)\to\varphi&&(K)\\ &2.&&(\varphi\to(\varphi\to\varphi)\to\varphi)\to(\varphi\to(\varphi\to\varphi))\to(\varphi\to\varphi)&&(S)\\ &3.&&(\varphi\to(\varphi\to\varphi))\to(\varphi\to\varphi)&&(1,2,MP)\\ &4.&&\varphi\to(\varphi\to\varphi)&&(K)\\ &5.&&\varphi\to\varphi&&(3,4,MP) \end{align}
$\varphi_1,\ldots,\varphi_n$が演繹の条件のうちどれをみたしているかで場合分けする.
  • $\varphi_i$$\mathbf{HM}$の公理であるとき
    以下のように$\varphi\to\varphi_{i-1}$$\varphi\to\varphi_i$の間に論理式を追加する.
    \begin{align} &\quad\vdots\\ &\varphi\to\varphi_{i-1}\\ &\varphi_i&&(\text{公理})\\ &\varphi_i\to(\varphi\to\varphi_i)&&(K)\\ &\varphi\to\varphi_i&&(MP)\\ &\quad\vdots \end{align}
  • $\varphi_i$$\Gamma$に含まれているとき
    \begin{align} &\quad\vdots\\ &\varphi\to\varphi_{i-1}\\ &\varphi_i&&(\text{前提})\\ &\varphi_i\to(\varphi\to\varphi_i)&&(K)\\ &\varphi\to\varphi_i&&(MP)\\ &\quad\vdots \end{align}
  • $\varphi_i$$\varphi$であるとき
    \begin{align} &\quad\vdots\\ &\varphi\to\varphi_{i-1}\\ &\varphi\to(\varphi\to\varphi)\to\varphi&&(K)\\ &(\varphi\to(\varphi\to\varphi)\to\varphi)\to(\varphi\to(\varphi\to\varphi))\to(\varphi\to\varphi)&&(S)\\ &(\varphi\to(\varphi\to\varphi))\to(\varphi\to\varphi)&&(MP)\\ &\varphi\to(\varphi\to\varphi)&&(K)\\ &\varphi\to\varphi&&(MP)\\ &\quad\vdots \end{align}
  • $i$未満の整数$j,k$が存在し, $\varphi_i$$\varphi_j,\varphi_k$から推論規則$(MP)$によって導かれているとき
    $\varphi_k\equiv\varphi_j\to\varphi_i$であるとして一般性を失わない.
    \begin{align} &\quad\vdots\\ &\varphi\to\varphi_{i-1}\\ &(\varphi\to\varphi_j\to\varphi_i)\to(\varphi\to\varphi_j)\to(\varphi\to\varphi_i)&&(S)\\ &(\varphi\to\varphi_j)\to(\varphi\to\varphi_i)&&(MP)\\ &\varphi\to\varphi_i&&(MP)\\ &\quad\vdots \end{align}
  • $i$未満の整数$j$が存在し, $\varphi_i$$\varphi_j$から推論規則$(GEN)$によって導かれているとき
    $\varphi_j=\psi[\zeta/\xi],\varphi_i=\forall\xi\psi$とおく.
    \begin{align} &\quad\vdots\\ &\varphi\to\varphi_{i-1}\\ &\forall\zeta(\varphi\to\psi[\zeta/\xi])&&(GEN)\\ &\forall\zeta(\varphi\to\psi[\zeta/\xi])\to(\varphi\to\forall\xi\psi)&&(UI)\\ &\varphi\to\forall\xi\psi&&(MP)\\ &\quad\vdots \end{align}
以上より, 演繹定理が示された. $\mathbf{HJ},\mathbf{HK}$についても同様に証明できる.

$\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$が成り立ちます.

Glivenkoの定理の証明

HMの公理 (再掲)

$\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}

HMの推論規則 (再掲)

\begin{align} &(MP)&\varphi,\varphi\to\psi&\implies\psi\\ &(GEN)&\varphi[\zeta/\xi]&\implies\forall\xi\varphi \end{align}
ただし, $\zeta$$\forall\xi\varphi$および演繹の前提に自由変項として現れない.

HJ,HKの公理 (再掲)

\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])^*$が成り立ちますが, ここでは証明しません.

Glivenkoの定理

任意の論理式列$\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}
となる.


はじめに, $\vdash_{\mathbf{HJ}}\lnot\lnot\varphi^*\implies\vdash_{\mathbf{HK}}\varphi$を示します.

任意の論理式$\varphi$に対し, $\vdash_{\mathbf{HK}}\varphi\to\varphi^*$かつ$\vdash_{\mathbf{HK}}\varphi^*\to\varphi$が成り立つ.

論理式$\varphi$に対し, $d(\varphi)\in\mathbb{N}\setminus\{0\}$を以下のように帰納的に定める.

  • $n$項述語$\theta$, 項$\tau_1,\ldots,\tau_n$に対し, $d(\theta(\tau_1,\ldots,\tau_n))=1$.
  • $n$項真理函数$\rho$, 論理式$\varphi_1,\ldots,\varphi_n$に対し, $d(\rho(\varphi_1,\ldots,\varphi_n))=\max\{d(\varphi_1),\ldots,d(\varphi_n)\}+1$. ただし, 零項真理函数$\bot$に対して$d(\bot)=1.$
  • 論理式$\varphi$, 変項$\xi$に対し, $d(\forall\xi\varphi)=d(\varphi)+1$, $d(\exists\xi\varphi)=d(\varphi)+1$.
(補題13)

$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$のときに補題が成立することを示す.

  • $\varphi\equiv\psi\to\chi$であるとき
    証明

    まず$\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$についても同様である.

  • $\varphi\equiv\psi\lor\chi$であるとき
    証明

    \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$についても同様である.

  • $\varphi\equiv\psi\land\chi$であるとき
    証明

    まず$\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$についても同様である.

  • $\varphi\equiv\forall\xi\psi$であるとき
    証明

    まず$\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$である.

  • $\varphi\equiv\exists\xi\psi$であるとき
    証明

    \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^*\implies\vdash_{\mathbf{HK}}\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の定理の証明の準備が整ったので証明をします.

($\vdash_{\mathbf{HK}}\varphi\implies\vdash_{\mathbf{HJ}}\lnot\lnot\varphi^*$)

$\varphi_1,\ldots,\varphi_n$$\mathbf{HK}$における$\varphi$の証明であるとする.
$\varphi_1,\ldots,\varphi_n$が演繹の条件のうちどれをみたしているかで場合分けする.

  • $\varphi_i$$\mathbf{HK}$の公理$X$であるとき
    命題14,15より, $X^*$$\mathbf{HJ}$の定理である.
    \begin{align} &\quad\vdots\\ &\lnot\lnot{\varphi_{i-1}}^*\\ &\lnot\lnot{\varphi_i}^*&&(\text{命題14,15})\\ &\quad\vdots \end{align}
  • $i$未満の整数$j,k$が存在し, $\varphi_i$$\varphi_j,\varphi_k$から推論規則$(MP)$によって導かれているとき
    $\varphi_k\equiv\varphi_j\to\varphi_i$であるとして一般性を失わない. 以下のように$\lnot\lnot{\varphi_{i-1}}^*$$\lnot\lnot{\varphi_i}^*$の間に論理式を追加する.
    \begin{align} &\quad\vdots\\ &\lnot\lnot{\varphi_{i-1}}^*\\ &\lnot\lnot{\varphi_j}^*\to\lnot\lnot({\varphi_j}^*\to{\varphi_i}^*)\to\lnot\lnot{\varphi_i}^*&&(MP^*)\\ &\lnot\lnot({\varphi_j}^*\to{\varphi_i}^*)\to\lnot\lnot{\varphi_i}^*&&(MP)\\ &\lnot\lnot{\varphi_i}^*&&(MP)\\ &\quad\vdots \end{align}
  • $i$未満の整数$j$が存在し, $\varphi_i$$\varphi_j$から推論規則$(GEN)$によって導かれているとき
    $\varphi_j=\psi[\zeta/\xi],\varphi_i=\forall\xi\psi$とおく.
    \begin{align} &\quad\vdots\\ &\lnot\lnot{\varphi_{i-1}}^*\\ &\lnot\lnot\psi^*[\zeta/\xi]\to\lnot\lnot\forall\xi\lnot\lnot\psi^*&&(GEN^*)\\ &\lnot\lnot\forall\xi\lnot\lnot\psi^*&&(MP)\\ &\quad\vdots \end{align}
以上より, Glivenkoの定理が示された.

参考文献

[1]
戸次大介, 数理論理学, 東京大学出版会, 2023
投稿日:24日前
OptHub AI Competition

この記事を高評価した人

高評価したユーザはいません

この記事に送られたバッジ

バッジはありません。

投稿者

tria_math
tria_math
565
50353
大学3年生

コメント

他の人のコメント

コメントはありません。
読み込み中...
読み込み中