「直観主義型理論（ITT, Intuitionistic Type Theory）」勉強会ノート其ノ八「複数の仮定付の判断とコンテクスト」「集合とカテゴリー」（復習編）

　こちらの復習編。他の回はカテゴリー「直観主義型理論」からどうぞ。

f:id:cut_elimination:20210414213220j:plain

複数の仮定付の判断とコンテクスト

B(x)の要素問題

　予習編で、仮定付判断の例えば $B(x) \;set \; x \in A$ の要素は [B(a)] だが $b(x) \in B(x) \; (x \in A)$ という判断もあって妙だと書いた。 $B(x)$ の要素は何なのか。しかしこれは仮定のスコープの問題のようである。前者は $(B(x) \; set \; (x \in A))$ のように見て、後者は $(b(x) \in B(x) \; (x \in A))$ と見るとわかりやすい。後者の仮定 $(x \in A)$ は $b(x)$ にまで及んでおり、決して $b(x) \in (B(x) \; (x \in A))$ ではない。

仮定の順番問題

　複数の仮定は導出で縦に書くべきではないかという意見が出た。前回の私のはすべて横に並べている。しかし $x_1 \in A_1$ と $x_2 \in A_2(x_1)$ では前者のほうが先に来るべきなような気がする。となるとこれらは上下に書くべきなのか。 $x_1:A_1, x_2:A_2(x_1) \vdash A(x_1, x_2)$ というゲンツェン風の書き方をするとこれは exchange 規則の意味づけの問題であるように思われる。これも検討課題である。あと $A \to (B \to C)$ と $B \to (A \to C)$ を同一視すべきかどうか、とか。

集合とカテゴリー

カテゴリーとオブジェクト

　カテゴリーとオブジェクトというのは存在論でよく出てくる語ではあるが、カテゴリーの要素をオブジェクト（対象）というわけではない。対象といっても「具体的対象」とか「抽象的対象」とかいろいろあり、そしてこれらのそれぞれがカテゴリーといえる。

現代存在論講義I—ファンダメンタルズ

作者:倉田剛
発売日: 2017/04/07
メディア: 単行本（ソフトカバー）

↑こちらを参照。

　マックレーンが category という語をどこから持ってきたのかとかちょっと気になる。

有意義性の範囲

　予習編でよくわかっていなかった "the range of significance of propositional function" というフレーズは、ラッセルがよく使うものらしい。1908年の論文 "Mathematical Logic as Based on the Theory of Types"（リンクはPDF）でも似たような表現を多用している。

カテゴリーではなくクラスでいいのでは？

　カテゴリーはクラスとは違うのだろうか。クラスはもともと命題関数によって定義されるものとしてフレーゲやラッセルが使っていたもの（だと思う）が、これと集合の違いは公理的集合論の整備によって明確になった。カテゴリーも「すべての集合の集合」を禁ずるためのもののようなので発想は同じである。ただし命題関数を基礎としたクラスと同等性を基礎としたカテゴリーでは思想としてもモノとしても違う感じ。

単純型と分岐型

　 $x \in x$ という命題関数は単純型理論では許されるけど分岐型理論ではダメなものの例ではなかろうか？

ベキ集合を関数で表す

　なぜ $\{0, 1\}^A$ はよくて ${\mathcal P}(A)$ はダメなのか？関数はプリミティブなので、定義域と値域が決まっていれば関数の集合が作れるのだろう。 ${\mathcal P}(A)$ は定義域と値域を指定する表現ではない。

単純型理論は分岐型理論では？

　マーティン=レーフ先生のいうカテゴリー＝単純型、集合＝分岐型の図式がラッセルやラムジーやチャーチの型理論と一致しているのかどうか微妙である。一致しているとしても自明ではないだろう。プログラミングの型は集合だと書いてあるので、つまり分岐型なのだろう。例えば単純型付ラムダ計算の型はBN記法で定義できるので、マーティン=レーフ先生のいう分岐型なのではないかと思う。しかしじゃあチャーチの単純型って分岐型なのだろうか？

　やはり型理論の歴史を紐解くべきか？