シリーズの第6回で「大枠と方針」とは、だいぶ話が前後してますが、ここであらためて述べておきます。短い記事です。
ハブ記事：
宇宙のラムダ計算の大枠と方針に関するキーワード〈重要語句〉は次です。
- 型付きラムダ計算
- 依存型理論
- 集合論的インフラストラクチャ
- セマンティクス主導
- 集合論的プラトニズム
宇宙のラムダ計算は、なにはともあれ型付きラムダ計算です。型付きラムダ計算は、下部構造として型システム／型理論を必要とします。宇宙のラムダ計算が採用する型理論は依存型理論です。
依存型理論は単純型理論を包摂します。また、Propositions-as-Types の立場により述語論理も包摂します。命題と証明が、型とインスタンスによりシミュレートされます。
依存型理論の定式化も色々ありますが、宇宙のラムダ計算では集合論的依存型理論を採用します。包括圏〈comprehension category〉やファミリー付き圏〈category with families〉を参照はしますが、抽象的なままで扱うわけではなくて、集合論的セマンティクスを一緒に考えます。
集合論的依存型理論のためには、基盤となる集合論的インフラストラクチャが必要です。集合論的インフラストラクチャも色々ありますが、我々が使うのはタルスキー／グロタンディーク集合論〈TG集合論〉です。これは、ZFC集合論に宇宙公理を追加して使いやすくした集合論であり、ZFC集合論の上に載っています。
ラムダ計算も型理論も構文論と意味論の区別があります。構文論だけをやる場合もあれば、構文論と意味論をあまり区別しないで展開することもあります。宇宙のラムダ計算では、セマンティクス主導の方針とします。これは、意味論の世界のなかで構文論を組み立てるということです。ベース部分が集合論的インフラストラクチャなので、集合達の世界は在ります。名前の集合や項の集合などは、意味論の世界のなかに位置づけることができます。構文-意味対応も、意味論の世界（集合論的宇宙）のなかで構成します。
「集合論的インフラストラクチャの上でセマンティクス主導で考える」ということは、集合論的世界は実在していると前提しています。フォン・ノイマン宇宙やグロタンディーク宇宙は実際にそこに在るので遠慮なく使う立場です。この態度はかなり楽観的でプラトニックなものです。集合論的プラトニズムと言えるでしょう。
