圏論的論理学
From Wikipedia, the free encyclopedia
概要
論理への圏論的アプローチには、3つの重要な主題がある。
- 圏論的意味論
- 圏論的論理学は、「圏 C の中で値をとる構造」という概念を導入する。C が集合と写像の圏である特別な場合が、古典的なモデル理論における構造の概念に相当する。この概念は、集合論的なモデルの概念では一般性を欠く、あるいは扱いにくい場合に有用であることが分かっている。R.A.G. Seelyによる非可述的理論（System F など）のモデル化は、圏論的意味論の有用性を示す一例である。
- 内部言語
- これはダイアグラム・チェイスによる証明の形式化・一般化と見ることができる。まず、圏の関連する構成要素に名前を与える適切な内部言語を定義し、次にその内部言語上の論理での主張を対応する圏論的言明に変換するために圏論的意味論を適用する。この方法はトポスの理論で最も成功しており、トポスの内部言語と、トポスにおける直観主義高階論理の意味論とを組み合わせることで、トポスの対象と射をあたかも集合と写像であるかのように推論できる[3]。この手法は、古典論理と両立しない性質をもつ「集合」を含むトポスを扱う上でも成功を収めている。代表例としては、デイナ・スコットによる型なしラムダ計算のモデル（自らの関数空間上にレトラクトする対象によるもの）や、マーティン・ハイランドの実効トポスの内部完全部分圏によるエウジニオ・モッジ–ハイランドのSystem F のモデルが挙げられる。
- 項モデル構成
- 多くの場合、論理の圏論的意味論は、その論理における理論と、適切な種類の圏のインスタンスとの間に対応関係を確立するための基礎を提供する。古典的な例は、単純型付きラムダ計算上のβη-等式論理の理論とデカルト閉圏との対応である。項モデル構成によって理論から得られる圏は通例、適切な普遍性によって同値を除いて特徴づけられる。この方法により、適切な圏論的代数を用いていくつかの論理のメタ理論的性質を証明できるようになった。例えば、フレイドはこの手法により直観主義論理の選言性および存在性の証明を与えた。
これら3つの主題は互いに関連している。ある論理の圏論的意味論とは、その論理における理論の圏と随伴関係にある構造化された圏の圏を記述することにある。この随伴を与える二つの関手は、一方では構造化された圏の内部言語を、他方では理論の項モデルを与える。
関連項目
- トポス理論の歴史
- コヒーレントトポス
