Zenn
📘

Glivenkoの定理の証明とCPS変換との関係

に公開
論理学
型理論
証明論
命題論理
curryhoward対応
tech

本稿で断り無しに「古典論理」といったらそれは古典命題論理であり、断り無しに「直観主義論理」といったらそれは直観主義命題論理を意図しています。

古典論理と直観主義論理をつなぐ「Glivenkoの定理」。
その証明の流れと、プログラム変換手法として知られる CPS変換（継続渡し形式）との驚くべき関係を紹介します。

Glivenkoの定理とは？

命題論理におけるGlivenkoの定理の主張：

φ が古典論理 LK で証明可能ならば、その二重否定 ¬¬φ は直観主義論理 LJ でも証明可能。

これは、形式的には次のように表されます：

Γ ⊢ φ（LKで証明可能） ⇒ Γ ⊢ ¬¬φ（LJで証明可能）

証明の全体構造

Glivenkoの定理の証明は以下の2方向があります。

  1. 直観主義 ⇒ 古典（容易）

    • ¬¬φ が直観主義論理で証明可能なら、φ は古典論理でも証明可能。

  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の定理（グリベンコの定理）の証明・紹介」という解説動画を公開しています。

▶️ YouTubeで視聴する（約8分）

  • 古典命題論理と直観主義論理の関係性
  • 二重否定翻訳とGlivenkoの定理の具体的な証明
  • 証明論・型理論・計算機科学に通じる思考の楽しさ

などをコンパクトにまとめており、初学者にも理解しやすい構成です。

📌 動画内目次

00:00 アイキャッチ
00:20 はじめの挨拶
00:54 動画の概要
01:22 体系LK, LJ
02:26 グリベンコの定理の主張の紹介
02:56 グリベンコの定理の証明
07:30 余談
07:50 おわりの挨拶
08:10 エンド・クレジット

🔗 参考資料とリンク

Discussion