「直観主義型理論（ITT, Intuitionistic Type Theory）」勉強会ノート其ノ弐拾四「宇宙」

　暫定版。

　あんまりわからないのでわかった点だけ箇条書きする。

これまでに導入した型はすべて有限の型である。何故なら型構築演算の反復（iteration）は有限回しかできないから。言語の表現力を上げるには宇宙（universe）を導入して超限の型（transfinite types）を入れる必要がある。
すべての集合の集合は作れない。何故ならそれ自体も集合になってしまい完全に規定できないので。だが圏論などですべての集合の集合は必要になる。
（よくわからないが）宇宙の作り方は、型構築の操作を可能的に超限回反復して閉包を得ること。その方法にはラッセル流とタルスキ流の二通りの方法がある。
ラッセル流は普通に $U$ という型を導入する。型構築演算は $U$ のカノニカルな要素を得る演算でもある。これは分岐型理論と似ている。タルスキ流はタルスキ真理論に由来するらしいけれどよくわからない。
$U$ 自体は $U$ の要素ではない。もしそうだとすると矛盾が発生する（ジラールのパラドクス）。
ペアノの第四公理 $(\forall x \in {\mathbb N})\lnot I({\mathbb N}, 0, x') \; true$ が証明できる。ペアノの第四公理というのは、 $0$ は何ものの後者でもない、というやつ。