21/05/27 07:15:55.61 dKVKdotp.net
メモ：21世紀の数学は”hol”（高階論理）ですね（＾＾
（旧ガロアすれにも貼った気がするが）
（参考）
URLﾘﾝｸ(staff.fnwi.uva.nl)
Taichi Uemura
Introduction
PhD candidate at Institute for Logic, Language and Computation, University of Amsterdam.
For contact, see my ILLC page.
URLﾘﾝｸ(staff.fnwi.uva.nl)
トポスと高階論理
Taichi Uemura
2018 年 12 月 9 日
この文書は Category Theory Advent Calendar 2018 (URLﾘﾝｸ(adventar.org)) の 9 日目の記事です。前
は 7 日目の@mod poppo さんの「アプリカティブ関手ってなに？モノイド圏との関係は？調べてみました！」でした。次は 11 日
目の@yf0fyf さんの「直観主義線型論理の圏論的意味論について」です。
概要
トポスの内部言語とその応用を紹介します。
目次
0 はじめに 1
1 高階論理 2
2 トポス 5
3 高階論理のモデル 6
4 内部言語 8
5 トポスの性質 10
6 おわりに 11
0 はじめに
トポス (topos) とは、有限極限と部分対象分類子と羃対象 (power object) を持つ圏である。簡潔な定義な
がら、トポスは驚くほど豊かな構造が持つことが知られている [MLM92, Joh02a]。
例えば、
・ トポスはデカルト閉である (定理 31);
・ トポスのスライスはまたトポスである (定理 32)。よって、トポスは局所デカルト閉 (locally