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

　他の直観主義型理論勉強会シリーズはこちらから。　

複数の仮定付の判断とコンテクスト
集合とカテゴリー

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

　family of sets with $n$ indeces, context

複数の仮定付の判断の解釈

　仮定付判断では述語に相当するものが定義された。複数の仮定付の判断では述語の述語に相当するもので、つまり高階論理が扱えるようになっている。仮定（assumption）の項数が $n$ である仮定付判断も扱えるように一般化する。その解釈は以下のように帰納的に与えられる。

　 $A_1$ は集合である。

　 $A_2(x_1)$ は $A_1$ 上の集合族である（ $A_1$ で添字付けられた集合族である）。

　 $A_3(x_1, x_2)$ は2つの添字 $x_1 \in A_1$ と $x_2 \in A_2(x_1)$ の付いた集合族である。

　…

　 $A_n(x_1, ..., x_{n-1})$ は $n-1$ 個の添字 $x_1 \in A_1, x_2 \in A_2(x_1), ..., x_{n-1} \in A_{n-1}(x_1, ..., x_{n-2})$ の付いた集合族である。

　そしてまたこれまでと同様に判断の4つの形式がある。

　(1) $A(x_1, ..., x_n) \; set \; (x_1 \in A_1, x_2 \in A_2(x_1), ..., x_n \in A_n(x_1, ..., x_{n-1}))$

この意味は、 $A(a_1, ..., a_n)$ が集合であるのは $a_1 \in A_1, a_2 \in A_2(a_1), ..., a_n \in A_n(a_1, ..., a_{n-1}$ であるとき、そして、 $A(a_1, ..., a_n) = A(b_1, ..., b_n)$ であるのは $a_1 = b_1 \in A_1, ..., a_n = b_n \in A_n(a_1, ..., a_n)$ であるとき、ということである。ひとつの仮定付の判断を $n$ 個に自然に拡張している。 $A_n$ のカッコ内は $b_1, ..., b_n$ でもよいと思われる。なんらかの $a_k$ が $b_k$ でもよいかもしれない。ここはそんなにちきんとしなくてよいかも。

　ここで、前回の勉強会では気づかなかったがいま気づいた点がある。「判断の形式の解釈」という節では、 $A \; set$ という判断は $A$ のカノニカルな要素の形成と等しさを規定することで与えられ、 $a \in A$ という判断は $a$ は実行すると $A$ のカノニカルな要素を得るメソッドということであった。しかし仮定付判断では話がちょっと違う。 $B(x) \; set \; (x \in A)$ という判断は $B(a)$ を規定し $B(a)$ と $B(c)$ の等しさを規定することである。つまり、集合族の要素である個々の集合たる $B(a)$ などが（カノニカルな）要素である。たいして $b(x) \in B(x) \; (x \in A)$ は $b(x)$ が要素として取られている。これは実行したら $B(a)$ になるわけではない。仮定付判断はちょっと考え方が違うのだろう。

　 $A(x_1, ..., x_n)$ を $n$ インデックスの集合族と呼ぶ。

コンテクスト

　(1)のような形の判断で $n$ 個の仮定はコンテクストを成すという。これはゲンツェンの推件計算における $\Gamma$ や $\Delta$ と似たようなものである。

　 $x_1 : A_1, x_2 : A_2(x_1) \vdash A(x_1, x_2)$ みたいな書き方をすればゲンツェンの推件計算の類似物とみなせる。

　任意の始切片もコンテクストである。ということは $x_1 \in A_1, x_2 \in A_2(x_1)$ もコンテクスト。

代入

　代入規則も拡張できる。書かれていないが

f:id:cut_elimination:20210509222426p:plain

こんな感じだと思う。この2つ目の規則なのだが、例えば $a_2 = b_2 \in A_2(a_1)$ というのはカッコ内が $b_1$ でもよいと思われる。代入は $n$ 個すべてやらなけらばならないのかはわからない。そのうち何個かだけでもよいのかもしれない。

その他の判断

　残り3つの判断も拡張する。

　(2) $A(x_1, ..., x_n) = B(x_1, ..., x_n) \; (x_1 \in A_1, ..., x_n \in A_n(x_1, ..., x_{n-1})$ （等しい $n$ インデックスの集合族）

　(3) $a(x_1, ..., x_n) \in A(x_1, ..., x_n) \; (x_1 \in A_1, ..., x_n \in A_n(x_1, ..., x_{n-1})$ （ $n$ 項の関数）

　(4) $a(x_1, ..., x_n) = b(x_1, ..., x_n) \in A(x_1, ..., x_n) \; (x_1 \in A_1, ..., x_n \in A(x_1, ..., x_{n-1}))$ （等しい $n$ 項の関数）

対応する代入規則は以下のような感じである。

f:id:cut_elimination:20210509230238p:plain

なんかガタガタしている…。また、記号や添字がややこしいのでミスがあるかもしれない。

集合とカテゴリー

　sets, categogies, simple types, ramified types, function, data types

カテゴリーとは（集合との違い）

　マーティン=レーフ先生のいうカテゴリー（category）は「圏論（category theory）」の「圏（category）」のことではないので注意が必要である。はじめそうかと思ったが、読み進めるとぜんぜん違うことがわかる。どちらかというとアリストテレスやカントの「範疇」を意識した語かもしれない。オブジェクトという用語も圏論と同じでややこしいが、これだけややこしいということは何か歴史的な事情があるのかもしれない。

　しかも集合という概念もかなり独特な捉え方をしている。それは（カノニカルな）要素の形成法の規定（prescribe）というこれまで散々語られてきたやつだが、よく考えれば普通の直観的な集合はそういうものではない。ただの集まりである。どちらかというとカテゴリーのほうが直観的な集合に近いかもしれない。

　ではカテゴリーとは何か。集合の要素にあたるものはカテゴリーではオブジェクトという。

A category is defined by explaining what an object of the category is and when two such objects are equal. A category need not be a set, since we can grasp what it means to be an object of a given category even without exhaustive rules for forming its objects.（11ページ）

カテゴリーは、そのカテゴリーのオブジェクトが何なのか、そして二つのオブジェクトが等しいのはどういうときか、解釈を与えることで定義される。カテゴリーは集合であるとは限らない。あるカテゴリーのオブジェクトであるとはどういうことか把握するには、そのオブジェクトを形成する徹底的な（exhaustive）規則がなくともよいからである。

　つまり、集合というのはカテゴリーよりも強い概念である。なので集合はカテゴリーでもあるが、逆はそうとは限らない。集合の要素をオブジェクトみなせば、集合をカテゴリーとみなせる。これはITT84では次の12ページで述べられている。ややこしいが、カテゴリーの定義の後で例として集合のカテゴリーが挙げられている。これは集合をオブジェクトとしたカテゴリーであって、集合をカテゴリーとみなしているわけではない。もちろん、こうした議論の「集合」は「命題」と置き換えられる。

　これまでに出てきたカテゴリーは以下：

集合（あるいは命題）のカテゴリー　（個々の集合がオブジェクト）
与えられた集合の要素（あるいは命題の証明）のカテゴリー
与えられた集合 $A$ 上の集合族 $B(x) \; (x \in A)$ のカテゴリー
関数 $b(x) \in B(x) \; (x \in A)$ （ただし、 $A \; set, B(x) \; set \; (x \in A)$ ）のカテゴリー
集合族 $C(x, y) \; (x \in A, y \in B(x))$ （ただし、 $A \; set, B(x) \; set \; (x \in A)$ ）のカテゴリー
関数 $c(x, y) \in C(x, y) \; (x \in A, y \in B(x))$ （ただし、 $A$ は集合で $B(x) \; (x \in A)$ と $C(x, y) \; (x \in A, y \in B(x))$ は集合族）のカテゴリー

さらに高次の（higher）カテゴリーもあって、二つの集合を別の一つの集合へうつす2項関数のカテゴリーなどである。これまでには関数 $times$ がそのオブジェクトの一例である。これは集合 $A$ と $B$ をデカルト積 $A \times B$ へうつす2項関数なので。

　これまで判断として定義してきた $a \in A, A \; set, a = b \in A, A = B$ というのは、それがカテゴリーのオブジェクトであること、ないしカテゴリーの等しいオブジェクトであることに関するものである（ $A \;set$ や $A = B$ という判断も要素や要素の等しさの規定を要求する）。

単純型理論と分岐型理論と可述性

　先ほど「集合はカテゴリーでもあるが、逆はそうとは限らない」と書いた。逆方向には反例がある。

... for instance, the category of sets and category of propositions are not sets, since we cannot describe how all their elements are formed.（12ページ）

…例えば、集合のカテゴリーや命題のカテゴリーは集合ではない。何故ならそれらのすべての要素を形成する方法を記述できないからである。

ここでは恐らく2ページ（当ブログでは其ノ壱と其ノ弐）で出てきた"open concept"が念頭にあるのだと思う。論理式の集合ならば論理式の構成に関する帰納的定義から集合を与えることができるだろう。しかし命題や集合はそうはいかない。ただし型は、あるプログラミング言語の型ということであれば型の集合を作れると思う。

　さてその型（type）である。ラッセルの理論では型には単純型（simple types）と分岐型（ramified types）がある。分岐型というのは単純型にさらに階（order）の階層を加えたものである。ラッセルの型理論については其ノ壱と其ノ弐の反省を踏まえてめちゃくちゃ調べた。

cut-elimination.hatenablog.com

さて、型は集合あるいはカテゴリーと同義なのか？マーティン=レーフ先生によれば、集合とカテゴリーを混同してしまうと、単純型理論が非可述的になるという。どうも単純型はカテゴリーで分岐型は集合ということらしい。

When a type is defined as the range of significance of a propositional function, so that types are what the quantifiers range over, then it seems that a type is the same thing as a set. On the other hand, when one speaks about the simple types of propositions, properties of individuals, relations, between individuals etc., it seems as if types and categories are the same.（12ページ）

型を命題関数の意味の範囲として定義して型を量化子の範囲であるとするならば、型は集合と同じになる。対して、命題の型とか個体の性質の型とか個体間の関係の型とか言うときには型とカテゴリーは同じものとみなせる。

"the range of significance of a propositional function"というのがなんなのかよくわからなかったのだが、命題関数が意味を成すために必要な量化の範囲ということと取った。とするとここでいう型は階を含むことになるのでこれは分岐型の話である。集合と分岐型が対応するというのはすぐ後で明示的に語られる。

The important difference between tha ramified types of propositions, properties, relations etc. of some finite order and simple types of all propositions, properties, relations etc. is precisely that the ramified types are (or can be understood as) sets, so that it makes sense to quantify over them, whereas the simple types are mere categories.（12ページ）

命題や性質や関係などが持つ何らかの有限の階の分岐型とすべての命題や性質や関係などの単純型との重大な違いは厳密には、分岐型が集合であって（あるいはそのように理解できて）それらの上の量化をなしうるのに対し単純型はただのカテゴリーであるということである。

この考え方の背景には、その上の量化が可能になるには要素の形成の規定が必要であるということと、そうでなければ「すべての」などとは言えないということがある。其ノ壱や其ノ弐の頃に「無限のドメイン上の量化」が何故できないのかよくわからなかったが、それは無限であれば要素の規定がないと「すべて」の議論ができないという考え方によるのだろう。

　ただし、このような直観主義的な考え方がラッセルの悪循環原理とどのように繋がってくるのかはよくわからない。規定がないと要素と言えないことと、ベリーのパラドクスのような悪循環の回避とに本質的な繋がりはあるのだろうか？『プリンキピア・マテマティカ』の体系では悪循環の回避の副産物として可述性が獲得されたわけで、ITTもジラールのパラドクスという悪循環の論理的パラドクスの回避のために可述性を導入したわけだから、分岐型を基本とするのは当然か。ただしベリーのパラドクスは論理的パラドクスではない。しかし階も型も同じようなものだということも上の記事に書いた。ジラールのパラドクスの回避の話はもうちょっと読み進めねばわからず、可述性の実現も具体的な型が導入されてからいま一度考えたい。現段階ではちょっとまだよくわからないことが多い。

関数はプリミティブ

　ここは難しいので思ったことをつらつら書いた。

　例が挙げられる。 $B^A$ は集合 $A$ から集合 $B$ への関数の集合である。ただし後に $B^A$ は $(\Pi x \in A)B(x)$ の、 $B(x)$ が常に $B$ と等しいとき（すなわち $x$ の値に依存しないとき）の略記として導入される。特に $\{0, 1\} ^A$ は集合だが、 ${\mathcal P}(A)$ はカテゴリーであるという。関数は後に $\Pi$ を使った集合として定義される。これは関数はプリミティブであるということらしい。対して ${\mathcal P}(A)$ や順序対の集まりとして見た関数はそうしたITTにとってプリミティブな関数ではない。これは $\Pi$ を使った定義はカノニカルな要素の形成の規定を与えているのに対し、部分集合の集合としてのベキ集合や順序対による関数定義はただの集まりでしかない、ということだろう。しかし私は現段階ではこれらの違いをあまりうまく説明できない。しかしカテゴリーとみなされるほうはITTの自然演繹のようなスタイルで適切に表現できないのはとりあえずわかってくるだろう。また、関数を順序対の集合として定義するのとラムダ計算のように記号の書き換えとして定義するのとでは存在論的にもパラドクスへの耐久力という点でも違いそうである。

データ型

　コンピュータ科学におけるデータ型はデータ集合であるとのこと。つまりCSにおける型はITTのいう集合である。とするとプログラミングとの対応を考えるならば集合は型と見てよいことになる。また、上でラムダ計算の話を持ち出したが、ラムダ計算の関数型は関数の集合、すなわち関数の分岐型ということになるだろうか。

　ラムダ計算の悪循環やパラドクスや階は今後調べたい。

曇りなき眼で見定めブログ

学生です。勉強したことを書いていく所存です。リンクもコメントも自由です！お手柔らかに。。。更新のお知らせはTwitter@cut_eliminationで