集合的形式化 #3 集合 (1)

    在 ZFC 中，“集合”本身作为一个类型，与相关公理一同被声明。在这个框架下，自然数、函数等对象都具有类型“集合”。若要在 Coq 中形式化集合，采用 ZFC 的方式可能会造成一些不必要的麻烦。因此，我们将采用另一种方式形式化集合。

    在以上代码中，对于每一个类型，该类型的“集合”被定义为一个归纳类型，每一个该类型上的集合与这个类型的一个谓词（性质）一一对应。对于类型 T 、其上的集合 S（即 S : 集合 T）、具有类型 T 的对象 x，x 属于 S 定义为 x 满足【S 对应的谓词】。定义集合建构式 { x | P x } 为谓词 P 对应的集合。（注：这一段的表述可能显得十分混乱，一部分原因是自然语言中“集合”一词往往指代 {0}、{1, 2} 等具体集合，而形式化时“集合”一词作为一个对象表示的是这些具体集合具有的类型）

    这种定义方式使得集合的使用更加灵活（可以构建任何类型上的集合），但也使得 { x, { x } } 等概念成为语法错误（设 x : A，则 { x } : 集合 A，二者类型不统一，无法组成集合）。

    利用函数外延公理，可以证明集合外延定理，进而得到更加实用的 SetExt。

    与集合相关的部分基本概念的定义如下：

    基本性质如下：

    集合与量词结合时的部分性质如下：