本稿で断り無しに「古典論理」といったらそれは古典命題論理であり、断り無しに「直観主義論理」といったらそれは直観主義命題論理を意図しています。
古典論理と直観主義論理をつなぐ「Glivenkoの定理」。
その証明の流れと、プログラム変換手法として知られる CPS変換（継続渡し形式）との驚くべき関係を紹介します。
Glivenkoの定理とは？
命題論理におけるGlivenkoの定理の主張：
φ が古典論理 LK で証明可能ならば、その二重否定 ¬¬φ は直観主義論理 LJ でも証明可能。
これは、形式的には次のように表されます：
Γ ⊢ φ（LKで証明可能） ⇒ Γ ⊢ ¬¬φ（LJで証明可能）
証明の全体構造
Glivenkoの定理の証明は以下の2方向があります。
-
直観主義 ⇒ 古典（容易）
- ¬¬φ が直観主義論理で証明可能なら、φ は古典論理でも証明可能。
-
古典 ⇒ 直観主義（本質的部分）
- φ が古典論理で証明可能なら、¬¬φ が直観主義論理で証明可能。
古典から直観主義への証明ステップ
証明は、古典論理の証明図に対する構造的帰納法で行われます。
最終推論規則によって場合分けします。
ケース例：
-
含意導入（→）
古典: Γ ⊢ A → B ⇒ 直観: Γ, A ⊢ ¬¬B ⇒ ¬¬(A → B) -
否定導入（¬）
古典: Γ, A ⊢ ⊥ ⇒ 直観: Γ ⊢ ¬A -
基底ケース（公理）
- φ が恒真であれば、¬¬φ も LJ で証明可能。
CPS変換との関係
CPSとは？
CPS（Continuation-Passing Style）は、関数が値を返すのではなく、「次に何をするか」（継続）に処理を渡すスタイルです。
// 通常の関数
function f(x) {
return x + 1;
}
// CPSスタイル
function f_cps(x, cont) {
cont(x + 1);
}
Glivenkoの変換と CPS の対応
論理における二重否定は、CPSにおける**「継続の安全性」**に対応します。
| 論理表現 | 意味 | CPS的意味 |
|---|---|---|
| φ | 計算の成功 | 結果が得られる |
| ¬φ = (φ → ⊥) | 例外 | φが走れば矛盾（エラー） |
| ¬¬φ = ((φ → ⊥) → ⊥) | φに矛盾がない | 安全な継続処理が可能 |
結論
- Glivenkoの定理は、古典論理を構成的に扱うための鍵となる理論です。
- CPS変換との対応は、Curry-Howard同型対応（論理と計算の一致）を具体化した好例です。
- 証明論・型理論・計算機科学の交差点に位置するテーマとして、今後も応用が期待されます。
✍ 参考キーワード
- Glivenkoの定理
- 直観主義論理
- CPS変換
- Curry-Howard対応
- 証明論
- 継続
🎥 解説動画：Glivenkoの定理をもっと深く知りたい方へ
本記事の内容を動画でさらに詳しく学びたい方のために、YouTubeにて
**「Glivenkoの定理（グリベンコの定理）の証明・紹介」**という解説動画を公開しています。
- 古典命題論理と直観主義論理の関係性
- 二重否定翻訳とGlivenkoの定理の具体的な証明
- 証明論・型理論・計算機科学に通じる思考の楽しさ
などをコンパクトにまとめており、初学者にも理解しやすい構成です。
📌 動画内目次
00:00 アイキャッチ
00:20 はじめの挨拶
00:54 動画の概要
01:22 体系LK, LJ
02:26 グリベンコの定理の主張の紹介
02:56 グリベンコの定理の証明
07:30 余談
07:50 おわりの挨拶
08:10 エンド・クレジット
🔗 参考資料とリンク
- 資料PDF：https://www.quawai.kyoto/pdfs/material_Glivenko.pdf
- 論計舎ウェブサイト：https://ronkeisha.net
- お問い合わせ：https://ronkeisha.net/contact/
- Twitter（論計舎）：@ronkeisha_info
- Twitter（川井 新）：@squawai