Agda上でのZF集合論の構成

摘要

Agdaは省略可能な型変数を持つ純關数型言語であ り、カーリーハワード対応に基づく証明支援系として 使うことができる。数学的な命題は型として記述され、 その証明は型を実現するえ項として記述される。ここ では直観主義論理に適した非構成的な仮定を導入し、 ZFC集合論の公理を証明する。集合はデータ構造であ る順序数上の述語（Ordinal definable)として導入する。