Two Day Workshop for Category Theory and Logic（二日目）

本日は集合論・型理論・圏論の相互の翻訳可能性について。

1. 集合論をメタ理論として、集合論の内部に直観主義的高階論理(IHOL)の翻訳を作成することは簡単。はい、いつもの型理論の集合論的モデル（をみたいに翻訳する）です。この翻訳によって定められる集合論内部の理論は、集合論において集合が持つ「型理論的情報」を全てこの枠組みにおいて捉えることが可能。
2. 型理論をメタ理論として、圏論の翻訳を型理論内部に作るには、トポスの出番。圏がトポスであれば、IHOL内部に翻訳可能である。さらこの翻訳は非常に望まししい性質を持つ。つまりトポスに翻訳されたIHOLは、IHOLのモデルとして健全かつ完全になる。
3. 圏論をメタ理論として集合論をその内部に翻訳する。これが最近はやりの代数的集合論（algebraic set theory）である。直観主義上の集合論BIST（urerementsを許し、基本的な公理はZFと同じだが、分出公理を持たず、代わりに-separation公理を持つ）は、トポイにうまく翻訳が可能である。すなわち、BISTである論理式が証明可能であることと、任意のトポイεに対しその上のイデアルを使って定義されるモデル上でが真になることが同値になる。

これらの意味で、以上の三つの基礎的な体系は相互に翻訳可能であり、従ってどの種類の体系がもっとも「基礎たり得る」とはいえない。

• これらの基礎的体系の「数学的内容」とは、この相互翻訳によっても失われないような定理のことだとしよう。この定義の意味で、三者は「同一の数学的内容を持つ」。
• 圏論は、他の処理論に比べ、数学的内容を「直接的に」表現する。
• 集合論と型理論は、トポスで扱えないような余計な（付加的な）内容も扱えるという特色を持つ。

ところで、「三つが相互に翻訳可能」というと、なんか、一つのメタ理論の中で、三者の相互翻訳可能性が定理として言える、というものなのだろうと想像していたのですが、そういうわけではなく、「どの理論を基点にとっても、他の二つをその中に埋め込める」と言う意味で、Awodey氏は「その意味でこれは数学的な定理だ」と言われていました。