Logic Winter School
アブストラクト
圏論的論理学の基本的なアイディアと重要なトピックについて、圏論的詳細に立ち入り過ぎない範囲で概説する。
Lecture 1. 圏論的一階述語論理 (1)
[Keyword] 命題論理と束、等式論理の函手的意味論、整合論理
Lecture 2. 圏論的一階述語論理 (2)
[Keyword] 随伴としての量化子、整合圏、整合圏におけるモデル、整合圏の内部論理
Lecture 3. 高階直観主義論理とトポス
[Keyword] トポス、Kripke-Joyal意味論、トポスにおける数学、トポスと集合論
Lecture 4. 圏論的論理学の拡がり
[Keyword] 種々の論理に対する圏論的意味論、圏論的一階述語論理の発展的応用、分類トポス、理論と翻訳の双圏
構成的数学は構成的論理（直観主義論理）に基づく数学である。構成的数学では通常の数学と比べ証明できる定理は少なくなるが、（定理の）証明とプログラムの間に自然な対応（カリー・ハワードの同型対応）がある。計算と親和性のある構成的数学における、いくつかの主要な話題について解説する。
Lecture 1. 構成的論理
[Keyword] 自然演繹体系、背理法、Goedel-Gentzenの翻訳とその一般化
Lecture 2. 構成的集合論
[Keyword] Basic and Elementary Constructive Set Theories (BCST and ECST)、 Constructive Zermelo-Fraenkel Set Theory (CZF)、 選択公理と排中律、Non-deterministic Inductive Definitions (NID)とFormal Topology
Lecture 3. 構成的解析学
[Keyword] 実数、距離空間、Ishihara's tricks、ノルム空間、Banach空間、Hilbert空間、Hahn-Banachの定理、開写像・閉グラフ定理
Lecture 4. 構成的逆数学
[Keyword] Omniscience Principles、様々な連続性、様々なコンパクト性、実数の２進展開、中間値の定理、単調完備定理
第1回 ポーランド空間とボレル集合族
全体の導入．記述集合論の舞台であるポーランド空間とくに再帰的表示をもつ空間を紹介し、ボレル集合族を定義する．また記述集合論の一般的な用語を導入する．
[Keyword] ポーランド空間、ボレル集合、ベール関数、再帰的表示をもつ空間
第2回 解析集合とススリンの定理
解析集合および射影集合の階層を紹介する．ボレル集合族を特徴づけるススリンの定理を示す．
[Keyword] 解析集合、射影集合、可算順序数、\Pi^1_1-完全集合
第3回 \Pi^1_1 の理論
一般化計算論(Generalized Recursion Theory)の観点から \Pi^1_1 の構造を調べ、近藤-アディソンの一意化定理を証明する．
[Keyword] 整礎木、近藤-アディソンの一意化定理
第4回 ルヴォの分離定理
ススリン-ルジンの分離定理の計算論的精密化であるルヴォの分離定理を証明し、ボレル集合の階層が実効的階層であることを示す．
[Keyword] ボレル集合のコード、ギャンディ位相、切り口問題への応用
古典計算可能性理論（帰納的関数論／再帰理論）から一新された現代的な観点から，計算可能性理論に入門しましょう．古典計算論の基本（計算可能性の定義など）はなんとなく知っているくらいを前提知識とします．
Lecture 1. 計算可能性理論の舞台
[Keyword] 実現可能性解釈，ナンバリング，表現空間，アセンブリ，従属型理論
Lecture 2. 計算可能性理論における空間
[Keyword] 許容表現空間，一様計算可能性，シエルピンスキ空間，synthetic topology
Lecture 3. 計算可能性理論における逆数学
[Keyword] チューリング次数，チューリングイデアル，Weihrauch次数，逆数学，インスタンス還元
Lecture 4. 計算可能性理論のトポス
[Keyword] 実効トポス，実現可能性トポス，Lawvere-Tierney位相
1階算術の超準モデルの古典的な結果が2階算術のモデルへどのように拡張されるか，いくつかの例について証明の手法と共に紹介します．算術の超準モデルの初歩(overspill, 真理定義述語, 再帰的飽和等)はある程度仮定しますが，必要に応じて説明します．
Lecture 1. 指標関数と2階算術
[Keyword] 指標関数(indicator), semi-regular cut, alpha-large set, generic cut, パリス-ハーリントンの定理
Lecture 2. WKLにまつわる同型定理
[Keyword] 再帰的飽和と往復論法, 田中の自己埋め込み定理とその仲間, WKL_0^*の同型定理, I-モデルとB-モデル (後半は時間があれば)