>>180
つづき

（圏論（トポス）と高階論理）
https://staff.fnwi.uva.nl/t.uemura/
PhD candidate at Institute for Logic, Language and Computation, University of Amsterdam.
トポスと高階論理 Taichi Uemura 2018年12月9日
この文書は Category Theory Advent Calendar 2018 (https://adventar.org/calendars/3168 *) の 9 日目の記事です。
*) Category Theory Advent Calendar 2018 作成者：piano2683
(抜粋)
0 はじめに
トポスとは、有限極限と部分対象分類子と羃対象を持つ圏である。

1 章では高階論理を導入する。
2 章でトポスを定義する。この段階ではトポスの圏論的性質には一切立ち入らない。
3 章で高階論理のトポスでの解釈を与える。
4 章でトポスの内部言語 (internal language) を高階理論として定義し、内部言語で導出できることとトポスの性質との関係をいくつか見る。
5 章でトポスの性質を内部言語を使っていくつか証明する。

基本的な圏論の知識 (極限、部分対象、随伴、デカルト閉圏など) は仮定するが、トポスについては前提知識は仮定しない。
トポスの知識がある人は圏論的な証明と高階論理を使った証明を比べてみると面白いと思います。
(引用終り)

https://ja.wikipedia.org/wiki/%E9%AB%98%E9%9A%8E%E8%BF%B0%E8%AA%9E%E8%AB%96%E7%90%86
高階述語論理
(抜粋)
高階述語論理は表現能力が高いが、その特性、特にモデル理論に関わる部分では、多くの応用について性格が良いとは言えない。クルト・ゲーデルの業績により、古典的高階述語論理は（帰納的に公理化された）健全で完全な証明計算が認められないとされた。しかし、Henkin model によれば、健全で完全な証明計算は存在する。
高階述語論理の例として、アロンゾ・チャーチの Simple Theory of Types や Calculus of Constructions (CoC) がある。

https://ja.wikipedia.org/wiki/%E3%82%A2%E3%83%AD%E3%83%B3%E3%82%BE%E3%83%BB%E3%83%81%E3%83%A3%E3%83%BC%E3%83%81
アロンゾ・チャーチ（Alonzo Church, 1903年6月14日 - 1995年8月11日）はアメリカの論理学者、数学者。ラムダ計算の創案者、「チャーチ＝チューリングのテーゼ」の提唱者として知られる。
(引用終り)
以上