はじめに
定理証明支援系で用いられる集合論は、ふつうの選択公理が加わったツェルメロ＝フレンケル集合論（ZFC）ではなく、構成的ツェルメロ＝フレンケル集合論（Constructive Zermelo–Fraenkel；CZF）らしい（同じAczelのNon-wellfounded set theoryとは異なる）。
CZFについては、日本語で情報がほとんどなく、マルティン＝レーフの型理論に自然な解釈をもつというようなことしかわからなかった1。
参考になりそうな資料
- D.Wehr. Aczel's Type-Theoretic Interpretation of Constructive Zermelo-Fraenkel set theory 単純に面白そう。
- Benjamin Werner.Sets in Types, Types in Sets coqのライブラリ coq-zfcの実装者の論文。zfc
- P.Aczel,Rathjen.Notes on constructive set theory 難しそうで読める気がしない。
時間見て、とりあえず上から順に読んでいければいいなぁ。。
Aczelの符号化論文
- P. Aczel. The Type Theoretic Interpretation of Set Theory. In A. MacIntyre, L. Pacholski and J. Paris (editors), Logic Colloquium '77, North-Holland, 1978.
- P. Aczel. The Type Theoretic Interpretation of Set Theory: 2nd Part. In F. Richman (editor), Constructive Mathematics, LNM 873, Springer-Verlag, 1981.
- P. Aczel. The Type Theoretic Interpretation of Set Theory: 3rd Part. In G. Sambin and J. Smith (editors), 25 years of Constructive Type Theory, Oxford University Press, 1996.
- N.Gambino, P.Aczel. The Generalised Type-Theoretic Interpretation of Constructive Set Theory,2005
選択公理
定理証明支援系（Lean）には普通の定義とは違うけれど選択公理はあるらしい。混乱してきた。
現在の疑問点
- CZFが単純にわからない。マルティン＝レーフの型理論の解釈ができるというが、マルティン＝レーフの型理論がわからない。
- Benjamin Werner のcoq-zfcは、Aczelのアプローチをとっている（CZF）のに、なぜZFCだと標榜しているのか？
Lean の型システムの無矛盾性については、Lean 3 の時代の結果として、「$ZFC_{\omega }$が無矛盾であることと、$Lean_{\omega }$ が無矛盾であることが同値であること」が知られている。ただし $ZFC_{\omega }$ とは、「ZFC に、任意の有限個の到達不能基数が存在するという仮定を足したもの」を指し、$Lean_{\omega }$ とは「Lean3の型システムに、任意の有限個の universe があるという仮定を足したもの」を指すものとする。 これは、ZFC の中で Lean3 のモデルが構築でき、Lean3 の中で ZFC が構築できるためである。
とあって、Benjamin Wernerの"Sets in Types, Types in Sets"が引用されている。だが、上の疑問と同じだが、ZFCの中でLean3のモデルが構築できるというのはありそうかなと言う気がするが、「Lean3の中でZFCが構築できる」というのは、本当なのだろうか？