文献あり

Glivenkoの定理

239

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

定義

HMの記号

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

一階述語論理の項

$α$ が名前ならば $α$ は項である.
$ξ$ が変項ならば $ξ$ は項である.
$ο$ が $n$ 項演算子で $τ_{1}, \dots, τ_{n}$ が項ならば $ο (τ_{1}, \dots, τ_{n})$ は項である.
上記以外は項ではない.

一階述語論理の論理式

$θ$ が $n$ 項述語で $τ_{1}, \dots, τ_{n}$ が項ならば $θ (τ_{1}, \dots, τ_{n})$ は論理式である.
$ρ$ が $n$ 項真理函数で $φ_{1}, \dots, φ_{n}$ が論理式ならば $ρ (φ_{1}, \dots, φ_{n})$ は論理式である.
$ξ$ が変項で $φ$ が論理式ならば $\forall ξ φ, \exists ξ φ$ は論理式である.
上記以外は論理式ではない.

$\to (φ, ψ)$ のことは $φ \to ψ$ と書きます. $\lor, \land$ についても同様です.
$φ \to ψ \to χ$ は $φ \to (ψ \to χ)$ を意味します.
結合の強さは ${\forall, \exists} > {\lor, \land} > \to$ の順です. したがって, $(\exists ξ φ \lor ψ \to χ) \to \forall ξ φ \to χ \land χ$ は $(((\exists ξ φ) \lor ψ) \to χ) \to ((\forall ξ φ) \to (χ \land χ))$ を意味します.

$φ \to ⊥$ を $\neg φ$ と略記する.

論理式 $φ$ に対し, $φ$ の自由変項の集合を $f v (φ)$ と表す. また, 変項 $ξ$ , 項 $τ$ に対し, 「 $φ$ に自由変項として現れる $ξ$ をすべて $τ$ に置き換えたもの」を $φ [τ / ξ]$ と書く.

自由変項とは, $\forall$ などによって束縛されていないということです.
$f v (φ), φ [τ / ξ]$ のちゃんとした定義については[1]などを参照してください.

論理式 $φ, ψ$ に対し, $φ$ と $ψ$ が(文字列として)等しいことを $φ \equiv ψ$ と書く.

この $\equiv$ は $HM$ の記号ではなく, メタ数学の記号です. したがって, $φ \equiv ψ$ は論理式ではありません. 後に出てくる $⊢$ なども同様です.
また, $φ \equiv ψ$ において $()$ の有無は無視することがあります.

HMの公理

$φ, ψ, χ, φ_{1}, φ_{2}$ を任意の論理式, $ξ, ζ$ を任意の変項, $τ$ を任意の項とする.
$\begin{aligned} (S) & (φ \to ψ \to χ) \to (φ \to ψ) \to (φ \to χ) \\ (K) & φ \to (ψ \to φ) \\ (D I) & φ_{i} \to φ_{1} \lor φ_{2} & (i = 1, 2) \\ (D E) & (φ \to χ) \to (ψ \to χ) \to (φ \lor ψ \to χ) \\ (C I) & φ \to ψ \to (φ \land ψ) \\ (C E) & φ_{1} \land φ_{2} \to φ_{i} & (i = 1, 2) \\ (U I) & \forall ζ (ψ \to φ [ζ / ξ]) \to (ψ \to \forall ξ φ) & (ζ \notin f v (ψ) \cup f v (\forall ξ φ)) \\ (U E) & \forall ξ φ \to φ [τ / ξ] \\ (E I) & φ [τ / ξ] \to \exists ξ φ \\ (E E) & \forall ζ (φ [ζ / ξ] \to ψ) \to (\exists ξ φ \to ψ) & (ζ \notin f v (ψ) \cup f v (\forall ξ φ)) \end{aligned}$

正確にはこれらは公理ではなく公理図式です. $φ$ などに具体的な論理式を代入したものが公理となります.

HMの推論規則

$\begin{aligned} (M P) & φ, φ \to ψ & ⟹ ψ \\ (G E N) & φ [ζ / ξ] & ⟹ \forall ξ φ \end{aligned}$
ただし, $ζ$ は $\forall ξ φ$ および演繹の前提に自由変項として現れない.

$\begin{aligned} (E F Q) & ⊥ \to φ \\ (D N E) & \neg \neg φ \to φ \end{aligned}$
とし, $HJ$ は $HM$ に $(E F Q)$ を公理として加えたもの, $HK$ は $HM$ に $(D N E)$ を公理として加えたものと定める.

演繹, 証明

$Γ$ を(0個以上の)論理式の列とする.
$HM$ における $Γ$ から $φ$ への演繹とは, 有限個の論理式からなる列 $φ_{1}, \dots, φ_{n}$ であって, $φ_{n} \equiv φ$ をみたし, 任意の $1 \leq i \leq n$ に対して以下のいずれかが成り立つものである.

$φ_{i}$ は $HM$ の公理である.
$φ_{i}$ は $Γ$ に含まれる.
$i$ 未満の整数 $j, k$ が存在し, $φ_{i}$ は $φ_{j}, φ_{k}$ から推論規則 $(M P)$ によって導かれる.
$i$ 未満の整数 $j$ が存在し, $φ_{i}$ は $φ_{j}$ から推論規則 $(G E N)$ によって導かれる.

Γ

をこの演繹における前提という. また,

Γ

が空列のときの演繹を証明という.

HM

における

φ

の証明が存在するとき,

φ

を

HM

の定理とよぶ.

HJ, HK

についても同様に定める.

$HM$ において $Γ$ から $φ$ への演繹が存在することを $Γ ⊢_{HM} φ$ と書く. $HJ, HK$ についても同様に定める.

$Γ ⊢_{HM} φ$ ならば $Γ ⊢_{HJ} φ$ や $Γ ⊢_{HK} φ$ が成り立ちます.

演繹定理

$HM$ における証明において欠かせない演繹定理について解説します.

演繹定理

任意の論理式列 $Γ$ , 論理式 $φ, ψ$ について以下が成り立つ.
$\begin{array}{r} Γ ⊢_{HM} φ \to ψ ⟺ φ, Γ ⊢_{HM} ψ \end{array}$
また, $HJ, HK$ についても同様のことが成り立つ.

$⟹$ の証明
$Γ$ から $φ \to ψ$ への演繹が $φ_{1}, \dots, φ_{n}$ ( $φ_{n} \equiv φ \to ψ$ )であるとする. このとき,
$φ_{1}, \dots, φ_{n - 1}, φ \to ψ, φ, ψ$
は $φ, Γ$ から $ψ$ への演繹である.

$⟸$ の証明
はじめに証明の概略を述べる.

φ_{1}, \dots, φ_{n}

が

φ, Γ

から

ψ

への演繹であるとする. このとき,

φ \to φ_{1}, \dots, φ \to φ_{n}

に適切に論理式を補充したものが

Γ

から

φ \to ψ

への演繹である.

まず,

⊢_{HM} φ \to φ

を示す. 以下が証明である.

\begin{aligned} 1. & φ \to (φ \to φ) \to φ & (K) \\ 2. & (φ \to (φ \to φ) \to φ) \to (φ \to (φ \to φ)) \to (φ \to φ) & (S) \\ 3. & (φ \to (φ \to φ)) \to (φ \to φ) & (1, 2, M P) \\ 4. & φ \to (φ \to φ) & (K) \\ 5. & φ \to φ & (3, 4, M P) \end{aligned}

φ_{1}, \dots, φ_{n}

が演繹の条件のうちどれをみたしているかで場合分けする.

$φ_{i}$ が $HM$ の公理であるとき
以下のように $φ \to φ_{i - 1}$ と $φ \to φ_{i}$ の間に論理式を追加する.
$\begin{aligned} ⋮ \\ φ \to φ_{i - 1} \\ φ_{i} & (公理) \\ φ_{i} \to (φ \to φ_{i}) & (K) \\ φ \to φ_{i} & (M P) \\ ⋮ \end{aligned}$
$φ_{i}$ が $Γ$ に含まれているとき
$\begin{aligned} ⋮ \\ φ \to φ_{i - 1} \\ φ_{i} & (前提) \\ φ_{i} \to (φ \to φ_{i}) & (K) \\ φ \to φ_{i} & (M P) \\ ⋮ \end{aligned}$
$φ_{i}$ が $φ$ であるとき
$\begin{aligned} ⋮ \\ φ \to φ_{i - 1} \\ φ \to (φ \to φ) \to φ & (K) \\ (φ \to (φ \to φ) \to φ) \to (φ \to (φ \to φ)) \to (φ \to φ) & (S) \\ (φ \to (φ \to φ)) \to (φ \to φ) & (M P) \\ φ \to (φ \to φ) & (K) \\ φ \to φ & (M P) \\ ⋮ \end{aligned}$
$i$ 未満の整数 $j, k$ が存在し, $φ_{i}$ が $φ_{j}, φ_{k}$ から推論規則 $(M P)$ によって導かれているとき
$φ_{k} \equiv φ_{j} \to φ_{i}$ であるとして一般性を失わない.
$\begin{aligned} ⋮ \\ φ \to φ_{i - 1} \\ (φ \to φ_{j} \to φ_{i}) \to (φ \to φ_{j}) \to (φ \to φ_{i}) & (S) \\ (φ \to φ_{j}) \to (φ \to φ_{i}) & (M P) \\ φ \to φ_{i} & (M P) \\ ⋮ \end{aligned}$
$i$ 未満の整数 $j$ が存在し, $φ_{i}$ が $φ_{j}$ から推論規則 $(G E N)$ によって導かれているとき
$φ_{j} = ψ [ζ / ξ], φ_{i} = \forall ξ ψ$ とおく.
$\begin{aligned} ⋮ \\ φ \to φ_{i - 1} \\ \forall ζ (φ \to ψ [ζ / ξ]) & (G E N) \\ \forall ζ (φ \to ψ [ζ / ξ]) \to (φ \to \forall ξ ψ) & (U I) \\ φ \to \forall ξ ψ & (M P) \\ ⋮ \end{aligned}$

以上より, 演繹定理が示された.

HJ, HK

についても同様に証明できる.

$φ$ を $HM$ の定理とする.
任意の論理式列 $Γ$ , 論理式 $ψ$ について以下が成り立つ.
$φ, Γ ⊢_{HM} ψ ⟺ Γ ⊢_{HM} ψ$

$⟸$ は自明. $⟹$ を示す.
演繹定理より $Γ ⊢_{HM} φ \to ψ$ であり, $Γ$ から $φ \to ψ$ への演繹を $φ_{1}, \dots, φ_{m}$ , $φ$ の証明を $φ_{1}^{'}, \dots, φ_{n}^{'}$ としたとき, $φ_{1}, \dots, φ_{m - 1}, φ \to ψ, φ_{1}^{'}, \dots, φ_{n - 1}^{'}, φ, ψ$ が $Γ$ から $ψ$ への演繹である.

定理は公理のように用いても問題ないということです. この事実は以後断りなく用います.

証明の準備

Glivenkoの定理の証明に必要となる定理を証明します. 知っている方は流し読みしてください.

$⊢_{HM} φ \to \neg \neg φ$

証明

$φ, \neg φ ⊢_{HM} ⊥$ を示せばよい.
$\begin{aligned} 1. & φ & (前提) \\ 2. & \neg φ & (前提) \\ 3. & ⊥ & (1, 2, M P) \end{aligned}$

$⊢_{HM} (φ \to ψ) \to (\neg ψ \to \neg φ)$

証明

$φ \to ψ, \neg ψ, φ ⊢_{HM} ⊥$ を示せばよい.
$\begin{aligned} 1. & φ & (前提) \\ 2. & φ \to ψ & (前提) \\ 3. & ψ & (1, 2, M P) \\ 4. & \neg ψ & (前提) \\ 5. & ⊥ & (3, 4, M P) \end{aligned}$

$⊢_{HM} \neg \neg \neg φ \to \neg φ$

証明

$\begin{aligned} 1. & φ \to \neg \neg φ & (定理2) \\ 2. & (φ \to \neg \neg φ) \to (\neg \neg \neg φ \to \neg φ) & (定理3) \\ 3. & \neg \neg \neg φ \to \neg φ & (1, 2, M P) \end{aligned}$

$⊢_{HM} (φ \to ψ) \to (\neg \neg φ \to \neg \neg ψ)$

証明

$φ \to ψ ⊢_{HM} \neg \neg φ \to \neg \neg ψ$ を示せばよい.
$\begin{aligned} 1. & φ \to ψ & (前提) \\ 2. & (φ \to ψ) \to (\neg ψ \to \neg φ) & (定理3) \\ 3. & \neg ψ \to \neg φ & (1, 2, M P) \\ 4. & (\neg ψ \to \neg φ) \to (\neg \neg φ \to \neg \neg ψ) & (定理3) \\ 5. & \neg \neg φ \to \neg \neg ψ & (3, 4, M P) \end{aligned}$

$⊢_{HM} φ \to ψ \to \neg (φ \to \neg ψ)$

証明

$φ, ψ, φ \to \neg ψ ⊢_{HM} ⊥$ を示せばよい.
$\begin{aligned} 1. & φ & (前提) \\ 2. & φ \to \neg ψ & (前提) \\ 3. & \neg ψ & (1, 2, M P) \\ 4. & ψ & (前提) \\ 5. & ⊥ & (3, 4, M P) \end{aligned}$

$⊢_{HM} \neg \neg (φ \to ψ) \to (\neg \neg φ \to \neg \neg ψ)$

証明

$\neg \neg (φ \to ψ), \neg \neg φ, \neg ψ ⊢_{HM} ⊥$ を示せばよい.
$\begin{aligned} 1. & (φ \to ψ) \to (\neg \neg φ \to \neg \neg ψ) & (定理5) \\ 2. & ((φ \to ψ) \to (\neg \neg φ \to \neg \neg ψ)) \to (\neg \neg (φ \to ψ) \to \neg \neg (\neg \neg φ \to \neg \neg ψ)) & (定理5) \\ 3. & \neg \neg (φ \to ψ) \to \neg \neg (\neg \neg φ \to \neg \neg ψ) & (1, 2, M P) \\ 4. & \neg \neg (φ \to ψ) & (前提) \\ 5. & \neg \neg (\neg \neg φ \to \neg \neg ψ) & (3, 4, M P) \\ 6. & \neg \neg φ & (前提) \\ 7. & \neg ψ & (前提) \\ 8. & \neg \neg φ \to \neg ψ \to \neg (\neg \neg φ \to \neg \neg ψ) & (定理6) \\ 9. & \neg ψ \to \neg (\neg \neg φ \to \neg \neg ψ) & (6, 8, M P) \\ 10. & \neg (\neg \neg φ \to \neg \neg ψ) & (7, 9, M P) \\ 11. & ⊥ & (5, 10, M P) \end{aligned}$

$⊢_{HM} \neg (φ \to ψ) \to \neg ψ$
$⊢_{HJ} \neg (φ \to ψ) \to \neg \neg φ$

証明

$\neg (φ \to ψ), ψ ⊢_{HM} ⊥$ を示せばよい.
$\begin{aligned} 1. & ψ & (前提) \\ 2. & ψ \to (φ \to ψ) & (K) \\ 3. & φ \to ψ & (1, 2, M P) \\ 4. & \neg (φ \to ψ) & (前提) \\ 5. & ⊥ & (3, 4, M P) \end{aligned}$
$\neg (φ \to ψ), \neg φ ⊢_{HJ} ⊥$ を示せばよい.
$\begin{aligned} 1. & ⊥ \to ψ & (E F Q) \\ 2. & (⊥ \to ψ) \to (φ \to (⊥ \to ψ)) & (K) \\ 3. & φ \to (⊥ \to ψ) & (1, 2, M P) \\ 4. & φ \to ⊥ & (前提) \\ 5. & (φ \to (⊥ \to ψ)) \to (φ \to ⊥) \to (φ \to ψ) & (S) \\ 6. & (φ \to ⊥) \to (φ \to ψ) & (3, 5, M P) \\ 7. & φ \to ψ & (4, 6, M P) \\ 8. & \neg (φ \to ψ) & (前提) \\ 9. & ⊥ & (7, 8, M P) \end{aligned}$

$⊢_{HJ} (\neg \neg φ \to \neg \neg ψ) \to \neg \neg (φ \to ψ)$

証明

$\neg \neg φ \to \neg \neg ψ, \neg (φ \to ψ) ⊢_{HJ} φ$ を示せばよい.
$\begin{aligned} 1. & \neg (φ \to ψ) & (前提) \\ 2. & \neg (φ \to ψ) \to \neg ψ & (定理8) \\ 3. & \neg ψ & (1, 2, M P) \\ 4. & \neg (φ \to ψ) \to \neg \neg φ & (定理8) \\ 5. & \neg \neg φ & (1, 4, M P) \\ 6. & \neg \neg φ \to \neg \neg ψ & (前提) \\ 7. & \neg \neg ψ & (5, 6, M P) \\ 8. & ⊥ & (3, 7, M P) \end{aligned}$

$⊢_{HJ} \neg \neg (\neg \neg φ \to φ)$

証明

$\begin{aligned} 1. & \neg \neg \neg \neg φ \to \neg \neg φ & (定理4) \\ 2. & (\neg \neg \neg \neg φ \to \neg \neg φ) \to \neg \neg (\neg \neg φ \to φ) & (定理9) \\ 3. & \neg \neg (\neg \neg φ \to φ) & (1, 2, M P) \end{aligned}$

$⊢_{HK} ⊥ \to φ$

証明

$⊥ ⊢_{HK} φ$ を示せばよい.
$\begin{aligned} 1. & ⊥ & (前提) \\ 2. & ⊥ \to (\neg φ \to ⊥) & (K) \\ 3. & \neg φ \to ⊥ & (1, 2, M P) \\ 4. & \neg \neg φ \to φ & (D N E) \\ 5. & φ & (3, 4, M P) \end{aligned}$

このことから $Γ ⊢_{HJ} φ ⟹ Γ ⊢_{HK} φ$ が成り立ちます.

Glivenkoの定理の証明

HMの公理 (再掲)

HMの推論規則 (再掲)

HJ,HKの公理 (再掲)

黒田否定変換

$n$ 項述語 $θ$ , 項 $τ_{1}, \dots, τ_{n}$ に対して $(θ (τ_{1}, \dots, τ_{n}))^{*} \equiv θ (τ_{1}, \dots, τ_{n})$ と定める.
論理式 $φ$ に対し, $φ^{*}$ を以下のように帰納的に定める.
$\begin{aligned} (φ \to ψ)^{*} & \equiv φ^{*} \to ψ^{*} \\ (φ \lor ψ)^{*} & \equiv φ^{*} \lor ψ^{*} \\ (φ \land ψ)^{*} & \equiv φ^{*} \land ψ^{*} \\ \forall ξ φ^{*} & \equiv \forall ξ \neg \neg φ^{*} \\ \exists ξ φ^{*} & \equiv \exists ξ φ^{*} \end{aligned}$
また, 論理式列 $Γ \equiv φ_{1}, \dots, φ_{n}$ に対し, $Γ^{*} \equiv {φ_{1}}^{*}, \dots, {φ_{n}}^{*}$ と定める.

$f v (φ^{*}) = f v (φ)$ および $φ^{*} [τ / ξ] \equiv (φ [τ / ξ])^{*}$ が成り立ちますが, ここでは証明しません.

Glivenkoの定理

任意の論理式列 $Γ$ , 論理式 $φ$ に対し,
$Γ ⊢_{HK} φ ⟺ Γ^{*} ⊢_{HJ} \neg \neg φ^{*}$

Glivenkoの定理を証明します.
まず, $Γ$ が空列の場合に示せば十分であることを確認します.

証明

定理7 $⊢_{HM} \neg \neg (φ \to ψ) \to (\neg \neg φ \to \neg \neg ψ)$ および定理9 $⊢_{HJ} (\neg \neg φ \to \neg \neg ψ) \to \neg \neg (φ \to ψ)$ を用いる.
$Γ \equiv φ_{1}, \dots, φ_{n}$ とすると, 演繹定理から
$\begin{aligned} Γ ⊢_{HK} φ & ⟺ ⊢_{HK} φ_{1} \to \dots \to φ_{n} \to φ \\ ⟺ ⊢_{HJ} \neg \neg (φ_{1} \to \dots \to φ_{n} \to φ)^{*} \\ ⟺ ⊢_{HJ} \neg \neg ({φ_{1}}^{*} \to \dots \to {φ_{n}}^{*} \to φ^{*}) \\ ⟺ ⊢_{HJ} \neg \neg {φ_{1}}^{*} \to \dots \to \neg \neg {φ_{n}}^{*} \to \neg \neg φ^{*} \\ ⟹ ⊢_{HJ} {φ_{1}}^{*} \to \dots \to {φ_{n}}^{*} \to \neg \neg φ^{*} \\ ⟺ Γ^{*} ⊢_{HJ} \neg \neg φ^{*} \end{aligned}$
および
$\begin{aligned} Γ^{*} ⊢_{HJ} \neg \neg φ^{*} & ⟺ ⊢_{HJ} {φ_{1}}^{*} \to \dots \to {φ_{n}}^{*} \to \neg \neg φ^{*} \\ ⟺ ⊢_{HJ} (φ_{1} \to \dots \to φ_{n} \to \neg \neg φ)^{*} \\ ⟹ ⊢_{HJ} \neg \neg (φ_{1} \to \dots \to φ_{n} \to \neg \neg φ)^{*} \\ ⟺ ⊢_{HK} φ_{1} \to \dots \to φ_{n} \to \neg \neg φ \\ ⟺ Γ ⊢_{HK} \neg \neg φ \\ ⟺ Γ ⊢_{HK} φ \end{aligned}$
となる.

はじめに,

⊢_{HJ} \neg \neg φ^{*} ⟹ ⊢_{HK} φ

を示します.

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

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

$n$ 項述語 $θ$ , 項 $τ_{1}, \dots, τ_{n}$ に対し, $d (θ (τ_{1}, \dots, τ_{n})) = 1$ .
$n$ 項真理函数 $ρ$ , 論理式 $φ_{1}, \dots, φ_{n}$ に対し, $d (ρ (φ_{1}, \dots, φ_{n})) = max {d (φ_{1}), \dots, d (φ_{n})} + 1$ . ただし, 零項真理函数 $⊥$ に対して $d (⊥) = 1.$
論理式 $φ$ , 変項 $ξ$ に対し, $d (\forall ξ φ) = d (φ) + 1$ , $d (\exists ξ φ) = d (φ) + 1$ .

(補題13)

$d (φ)$ による帰納法で示す.
$d (φ) = 1$ のとき, $φ \equiv θ (τ_{1}, \dots, τ_{n})$ または $φ \equiv ⊥$ であり, どちらの場合でも $φ^{*} \equiv φ$ であるため補題は成立する.

$d \geq 2$ として, $d (φ) = 1, \dots, d - 1$ のときに補題が成立しているとする. $d (φ) = d$ のときに補題が成立することを示す.

$φ \equiv ψ \to χ$ であるとき
証明
まず $ψ \to χ, ψ^{*} ⊢_{HK} χ^{*}$ を示す.
$\begin{aligned} 1. & ψ^{*} & (前提) \\ 2. & ψ^{*} \to ψ & (帰納法の仮定) \\ 3. & ψ & (1, 2, M P) \\ 4. & ψ \to χ & (前提) \\ 5. & χ & (3, 4, M P) \\ 6. & χ \to χ^{*} & (帰納法の仮定) \\ 7. & χ^{*} & (5, 6, M P) \end{aligned}$
演繹定理より $⊢_{HK} φ \to φ^{*}$ である.
$⊢_{HK} φ^{*} \to φ$ についても同様である.
$φ \equiv ψ \lor χ$ であるとき
証明
$\begin{aligned} 1. & ψ^{*} \to ψ^{*} \lor χ^{*} & (D I) \\ 2. & (ψ^{*} \to ψ^{*} \lor χ^{*}) \to (ψ \to (ψ^{*} \to ψ^{*} \lor χ^{*})) & (K) \\ 3. & ψ \to (ψ^{*} \to ψ^{*} \lor χ^{*}) & (1, 2, M P) \\ 4. & ψ \to ψ^{*} & (帰納法の仮定) \\ 5. & (ψ \to (ψ^{*} \to ψ^{*} \lor χ^{*})) \to (ψ \to ψ^{*}) \to (ψ \to ψ^{*} \lor χ^{*}) & (S) \\ 6. & (ψ \to ψ^{*}) \to (ψ \to ψ^{*} \lor χ^{*}) & (3, 5, M P) \\ 7. & ψ \to ψ^{*} \lor χ^{*} & (4, 6, M P) \\ 8. & χ^{*} \to ψ^{*} \lor χ^{*} & (D I) \\ 9. & (χ^{*} \to ψ^{*} \lor χ^{*}) \to (χ \to (χ^{*} \to ψ^{*} \lor χ^{*})) & (K) \\ 10. & χ \to (χ^{*} \to ψ^{*} \lor χ^{*}) & (8, 9, M P) \\ 11. & χ \to χ^{*} & (帰納法の仮定) \\ 12. & (χ \to (χ^{*} \to ψ^{*} \lor χ^{*})) \to (χ \to χ^{*}) \to (χ \to ψ^{*} \lor χ^{*}) & (S) \\ 13. & (χ \to χ^{*}) \to (χ \to ψ^{*} \lor χ^{*}) & (10, 12, M P) \\ 14. & χ \to ψ^{*} \lor χ^{*} & (11, 13, M P) \\ 15. & (ψ \to ψ^{*} \lor χ^{*}) \to (χ \to ψ^{*} \lor χ^{*}) \to (ψ \lor χ \to ψ^{*} \lor χ^{*}) & (D E) \\ 16. & (χ \to ψ^{*} \lor χ^{*}) \to (ψ \lor χ \to ψ^{*} \lor χ^{*}) & (7, 15, M P) \\ 17. & ψ \lor χ \to ψ^{*} \lor χ^{*} & (14, 16, M P) \end{aligned}$
したがって $⊢_{HK} φ \to φ^{*}$ である.
$⊢_{HK} φ^{*} \to φ$ についても同様である.
$φ \equiv ψ \land χ$ であるとき
証明
まず $ψ \land χ ⊢_{HK} ψ^{*} \land χ^{*}$ を示す.
$\begin{aligned} 1. & ψ \land χ & (前提) \\ 2. & ψ \land χ \to ψ & (C E) \\ 3. & ψ & (1, 2, M P) \\ 4. & ψ \to ψ^{*} & (帰納法の仮定) \\ 5. & ψ^{*} & (3, 4, M P) \\ 6. & χ \land χ \to ψ & (C E) \\ 7. & χ & (1, 6, M P) \\ 8. & χ \to χ^{*} & (帰納法の仮定) \\ 9. & χ^{*} & (7, 8, M P) \\ 10. & ψ^{*} \to χ^{*} \to ψ^{*} \land χ^{*} & (C I) \\ 11. & χ^{*} \to ψ^{*} \land χ^{*} & (5, 10, M P) \\ 12. & ψ^{*} \land χ^{*} & (9, 11, M P) \end{aligned}$
演繹定理より $⊢_{HK} φ \to φ^{*}$ である.
$⊢_{HK} φ^{*} \to φ$ についても同様である.
$φ \equiv \forall ξ ψ$ であるとき
証明
まず $\forall ξ ψ ⊢_{HK} \forall ξ \neg \neg ψ^{*}$ を示す.
$\begin{aligned} 1. & \forall ξ ψ & (前提) \\ 2. & \forall ξ ψ \to ψ & (U E) \\ 3. & ψ & (1, 2, M P) \\ 4. & ψ \to ψ^{*} & (帰納法の仮定) \\ 5. & ψ^{*} & (3, 4, M P) \\ 6. & ψ^{*} \to \neg \neg ψ^{*} & (定理2) \\ 7. & \neg \neg ψ^{*} & (5, 6, M P) \\ 8. & \forall ξ \neg \neg ψ^{*} & (7, G E N) \end{aligned}$
演繹定理より $⊢_{HK} φ \to φ^{*}$ である.
次に $\forall ξ \neg \neg ψ^{*} ⊢_{HK} \forall ξ ψ$ を示す.
$\begin{aligned} 1. & \forall ξ \neg \neg ψ^{*} & (前提) \\ 2. & \forall ξ \neg \neg ψ^{*} \to \neg \neg ψ^{*} & (U E) \\ 3. & \neg \neg ψ^{*} & (1, 2, M P) \\ 4. & \neg \neg ψ^{*} \to ψ^{*} & (D N E) \\ 5. & ψ^{*} & (3, 4, M P) \\ 6. & ψ^{*} \to ψ & (帰納法の仮定) \\ 7. & ψ & (5, 6, M P) \\ 8. & \forall ξ ψ & (7, G E N) \end{aligned}$
演繹定理より $⊢_{HK} φ^{*} \to φ$ である.
$φ \equiv \exists ξ ψ$ であるとき
証明
$\begin{aligned} 1. & ψ \to ψ^{*} & (帰納法の仮定) \\ 2. & ψ^{*} \to \exists ξ ψ^{*} & (E I) \\ 3. & (ψ^{*} \to \exists ξ ψ^{*}) \to (ψ \to ψ^{*}) \to (ψ \to \exists ξ ψ^{*}) & (B) \\ 4. & (ψ \to ψ^{*}) \to (ψ \to \exists ξ ψ^{*}) & (2, 3, M P) \\ 5. & ψ \to \exists ξ ψ^{*} & (1, 4, M P) \\ 6. & \forall ξ (ψ \to \exists ξ ψ^{*}) & (5, G E N) \\ 7. & \forall ξ (ψ \to \exists ξ ψ^{*}) \to (\exists ξ ψ \to \exists ξ ψ^{*}) & (E E) \\ 8. & \exists ξ ψ \to \exists ξ ψ^{*} & (6, 7, M P) \end{aligned}$
したがって $⊢_{HK} φ \to φ^{*}$ である.
$⊢_{HK} φ^{*} \to φ$ についても同様である.

(

⊢_{HJ} \neg \neg φ^{*} ⟹ ⊢_{HK} φ

)

$⊢_{HJ} \neg \neg φ^{*}$ と仮定する. このとき, $⊢_{HK} \neg \neg φ^{*}$ である.
$\begin{aligned} 1. & \neg \neg φ^{*} & (仮定) \\ 2. & \neg \neg φ^{*} \to φ^{*} & (D N E) \\ 3. & φ^{*} & (1, 2, M P) \\ 4. & φ^{*} \to φ & (補題13) \\ 5. & φ & (3, 4, M P) \end{aligned}$
したがって, $⊢_{HK} φ$ である.

つづいて, $⊢_{HK} φ ⟹ ⊢_{HJ} \neg \neg φ^{*}$ を示します.
証明の概略は, 上で述べた演繹定理の証明と同じです.

$φ_{1}, \dots, φ_{n}$ が $HK$ における $φ$ の証明であるとする. このとき, $\neg \neg {φ_{1}}^{*}, \dots, \neg \neg {φ_{n}}^{*}$ に適切に論理式を補充したものが $HJ$ における $\neg \neg φ^{*}$ の証明である.

定理2 $⊢_{HM} φ \to \neg \neg φ$ を思い出します.

以下は $HJ$ の定理である.
$\begin{aligned} (S^{*}) & \neg \neg ((φ^{*} \to ψ^{*} \to χ^{*}) \to (φ^{*} \to ψ^{*}) \to (φ^{*} \to χ^{*})) \\ (K^{*}) & \neg \neg (φ^{*} \to (ψ^{*} \to φ^{*})) \\ (D I^{*}) & \neg \neg ({φ_{i}}^{*} \to {φ_{1}}^{*} \lor {φ_{2}}^{*}) & (i = 1, 2) \\ (D E^{*}) & \neg \neg ((φ^{*} \to χ^{*}) \to (ψ^{*} \to χ^{*}) \to (φ^{*} \lor ψ^{*} \to χ^{*})) \\ (C I^{*}) & \neg \neg (φ^{*} \to ψ^{*} \to (φ^{*} \land ψ^{*})) \\ (C E^{*}) & \neg \neg ({φ_{1}}^{*} \land {φ_{2}}^{*} \to {φ_{i}}^{*}) & (i = 1, 2) \\ (U I^{*}) & \neg \neg (\forall ζ (ψ^{*} \to φ^{*} [ζ / ξ]) \to (ψ^{*} \to \forall ξ φ^{*})) & (ζ \notin f v (ψ) \cup f v (\forall ξ φ)) \\ (U E^{*}) & \neg \neg (\forall ξ φ^{*} \to φ^{*} [τ / ξ]) \\ (E I^{*}) & \neg \neg (φ^{*} [τ / ξ] \to \exists ξ φ^{*}) \\ (E E^{*}) & \neg \neg (\forall ζ (φ^{*} [ζ / ξ] \to ψ^{*}) \to (\exists ξ φ^{*} \to ψ^{*})) & (ζ \notin f v (ψ) \cup f v (\forall ξ φ)) \end{aligned}$

$S^{*}$ などはこの記事独自の記号です.

定理10 $⊢_{HJ} \neg \neg (\neg \neg φ \to φ)$ を思い出します.

以下は $HJ$ の定理である.
$\begin{aligned} (D N E^{*}) & \neg \neg (\neg \neg φ^{*} \to φ^{*}) \end{aligned}$

つづいて, 定理7 $⊢_{HJ} \neg \neg (φ \to ψ) \to (\neg \neg φ \to \neg \neg ψ)$ を思い出します.

以下は $HJ$ の定理である.
$\begin{aligned} (M P^{*}) & \neg \neg φ^{*} \to \neg \neg (φ^{*} \to ψ^{*}) \to \neg \neg ψ^{*} \\ (G E N^{*}) & \neg \neg φ^{*} [ζ / ξ] \to \neg \neg \forall ξ \neg \neg φ^{*} \end{aligned}$
ただし, $ζ$ は $\forall ξ φ$ および演繹の前提に自由変項として現れない.

演繹定理より $\neg \neg φ^{*}, \neg \neg (φ^{*} \to ψ^{*}) ⊢_{HJ} \neg \neg ψ^{*}$ を示せばよい.
$\begin{aligned} 1. & \neg \neg φ^{*} & (前提) \\ 2. & \neg \neg (φ^{*} \to ψ^{*}) & (前提) \\ 3. & \neg \neg (φ^{*} \to ψ^{*}) \to (\neg \neg φ^{*} \to \neg \neg ψ^{*}) & (定理7) \\ 4. & \neg \neg φ^{*} \to \neg \neg ψ^{*} & (2, 3, M P) \\ 5. & \neg \neg ψ^{*} & (1, 4, M P) \end{aligned}$
演繹定理より $\neg \neg φ^{*} [ζ / ξ] ⊢_{HJ} \neg \neg \forall ξ \neg \neg φ^{*}$ を示せばよい.
$\begin{aligned} 1. & \neg \neg φ^{*} [ζ / ξ] & (前提) \\ 2. & \forall ξ \neg \neg φ^{*} & (1, G E N) \\ 3. & \forall ξ \neg \neg φ^{*} \to \neg \neg \forall ξ \neg \neg φ^{*} & (定理2) \\ 4. & \neg \neg \forall ξ \neg \neg φ^{*} & (2, 3, M P) \end{aligned}$

これでGlivenkoの定理の証明の準備が整ったので証明をします.

(

⊢_{HK} φ ⟹ ⊢_{HJ} \neg \neg φ^{*}

)

$φ_{1}, \dots, φ_{n}$ が $HK$ における $φ$ の証明であるとする.
$φ_{1}, \dots, φ_{n}$ が演繹の条件のうちどれをみたしているかで場合分けする.

$φ_{i}$ が $HK$ の公理 $X$ であるとき
命題14,15より, $X^{*}$ は $HJ$ の定理である.
$\begin{aligned} ⋮ \\ \neg \neg {φ_{i - 1}}^{*} \\ \neg \neg {φ_{i}}^{*} & (命題14,15) \\ ⋮ \end{aligned}$
$i$ 未満の整数 $j, k$ が存在し, $φ_{i}$ が $φ_{j}, φ_{k}$ から推論規則 $(M P)$ によって導かれているとき
$φ_{k} \equiv φ_{j} \to φ_{i}$ であるとして一般性を失わない. 以下のように $\neg \neg {φ_{i - 1}}^{*}$ と $\neg \neg {φ_{i}}^{*}$ の間に論理式を追加する.
$\begin{aligned} ⋮ \\ \neg \neg {φ_{i - 1}}^{*} \\ \neg \neg {φ_{j}}^{*} \to \neg \neg ({φ_{j}}^{*} \to {φ_{i}}^{*}) \to \neg \neg {φ_{i}}^{*} & (M P^{*}) \\ \neg \neg ({φ_{j}}^{*} \to {φ_{i}}^{*}) \to \neg \neg {φ_{i}}^{*} & (M P) \\ \neg \neg {φ_{i}}^{*} & (M P) \\ ⋮ \end{aligned}$
$i$ 未満の整数 $j$ が存在し, $φ_{i}$ が $φ_{j}$ から推論規則 $(G E N)$ によって導かれているとき
$φ_{j} = ψ [ζ / ξ], φ_{i} = \forall ξ ψ$ とおく.
$\begin{aligned} ⋮ \\ \neg \neg {φ_{i - 1}}^{*} \\ \neg \neg ψ^{*} [ζ / ξ] \to \neg \neg \forall ξ \neg \neg ψ^{*} & (G E N^{*}) \\ \neg \neg \forall ξ \neg \neg ψ^{*} & (M P) \\ ⋮ \end{aligned}$