圏論的論理学（けんろんてきろんりがく、）は、圏論の道具立てと概念を数理論理学の研究に応用する数学の一分野である。また理論計算機科学との結びつきでも注目されている。 大まかに言えば、圏論的論理学は構文論と意味論の双方を圏によって表現し、解釈を関手によって表現する。この圏論的な枠組みは、論理的および型理論的な構成に対して豊かな概念的背景を提供する。この分野が現在のような姿で認識されるようになったのは、およそ1970年頃からである。
概要
論理への圏論的アプローチには、3つの重要な主題がある。 圏論的意味論 圏論的論理学は、「圏 C の中で値をとる構造」という概念を導入する。C が集合と写像の圏である特別な場合が、古典的なモデル理論における構造の概念に相当する。この概念は、集合論的なモデルの概念では一般性を欠く、あるいは扱いにくい場合に有用であることが分かっている。による非可述的理論（System F など）のモデル化は、圏論的意味論の有用性を示す一例である。
前圏論的な論理における結合子は随伴関手の概念を用いる方が明確に理解でき、量化子もまた随伴関手を用いた方が最もよく理解できることが判明した。
内部言語 これはダイアグラム・チェイスによる証明の形式化・一般化と見ることができる。まず、圏の関連する構成要素に名前を与える適切な内部言語を定義し、次にその内部言語上の論理での主張を対応する圏論的言明に変換するために圏論的意味論を適用する。この方法はトポスの理論で最も成功しており、トポスの内部言語と、トポスにおける直観主義高階論理の意味論とを組み合わせることで、トポスの対象と射をあたかも集合と写像であるかのように推論できる。この手法は、古典論理と両立しない性質をもつ「集合」を含むトポスを扱う上でも成功を収めている。代表例としては、デイナ・スコットによる型なしラムダ計算のモデル（自らの関数空間上にする対象によるもの）や、のの内部によるエウジニオ・モッジ–ハイランドのSystem F のモデルが挙げられる。
項モデル構成 多くの場合、論理の圏論的意味論は、その論理における理論と、適切な種類の圏のインスタンスとの間に対応関係を確立するための基礎を提供する。古典的な例は、単純型付きラムダ計算上の-の理論とデカルト閉圏との対応である。項モデル構成によって理論から得られる圏は通例、適切な普遍性によって同値を除いて特徴づけられる。この方法により、適切な圏論的代数を用いていくつかの論理のメタ理論的性質を証明できるようになった。例えば、はこの手法により直観主義論理のの証明を与えた。
これら3つの主題は互いに関連している。ある論理の圏論的意味論とは、その論理における理論の圏と随伴関係にある構造化された圏の圏を記述することにある。この随伴を与える二つの関手は、一方では構造化された圏の内部言語を、他方では理論の項モデルを与える。
関連項目
注釈
参考文献 書籍
主要論文
さらに読む
比較的入門しやすい書籍だが、やや古い。多相型・依存型上の高階論理への圏論的アプローチは、本書刊行後に大きく発展した。 計算機科学者による包括的なモノグラフ。一階論理と高階論理の双方、および多相型・依存型を扱う。多相型・依存型を扱う上で不可欠となる、圏論的論理学の普遍的道具としてのに重点が置かれている。 オンライン版はJohn Bell's homepageで参照可能。 予備的版。