証明可能性の構造的理解に向けて：圏論的アプローチ (in Japanese)Towards a structural understanding of provability: A categorical approach

@misc{ikeda-wakate2025,
  author       = {Ikeda, Yuto},
  title        = {証明可能性の構造的理解に向けて：圏論的アプローチ [{Towards} a Structural Understanding of Provability: A Categorical Approach]},
  howpublished = {Talk at 数学基礎論若手の会 2025},
  year         = {2025},
  month        = oct,
  note         = {(in Japanese)},
  url          = {https://ikeda.ac/talks/wakate2025/}
}

Abstract

Gödelの第二不完全性定理に端を発する証明可能性論理の研究は，様相論理との結びつきを通して豊かな成果をもたらしてきた一方で，証明可能性述語の性質がその具体的な構成に強く依存するという「内包性 (intensionality)」の問題も明らかにした．この内包性は，第二不完全性定理の証明の複雑さの根源であり，特定の表現や構成に依存する議論を分離することを難しくしている．

この課題に対し，圏論的論理学が有効な視点を提供する可能性がある．その先駆けとして，Joyalは自身の講義の中で，理論の内部記述構造を，内部圏 (internal category) を用いて解釈し，第二不完全性定理の特別な場合について，その圏論的証明を与えた．また，Rameshによる近年の研究は，Joyalの手法を広範に一般化し，第二不完全性定理やLöbの定理を成立させるシンプルな圏論的構造を提案している．この枠組みは，古典的なLöbの定理に抽象的な視点を与えるだけでなく，証明可能性論理GLのKripke意味論や，ガード付き再帰の圏論的モデルといった，異なる文脈で表れる種々の「Gödel–Löb的現象」を部分的に統一する．

これらの成果にもかかわらず，証明可能性の圏論的分析は未開拓な領域が大きい．本発表では，これらの先行研究を足がかりに，今後の研究の可能性を展望する．加えて，メタプログラミングの理論的モデルである様相𝜆計算と，古典的な証明可能性論理GLとの間に既知の対応がある中で，圏論的枠組みが両者の直接的な橋渡しの役割を果たす可能性についても議論する．