Sets in Coq, Coq in Sets
Sets in Coq, Coq in Sets
复制标题
Coq 中的集合，Coq 中的集合
DOI：
10.6092/issn.1972-5787/1695
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
Bruno Barras
中科院分区：
文献类型：
--
作者：
Bruno Barras
本文的工作是关于构造演算族的各种类型理论的形式化模型。在这里，我们专注于设置理论模型。长期目标是建立归纳构造演算的正式集合理论模型，这样我们就可以确保Coq与大多数数学家使用的语言一致。
这项工作的一个方面是公理化几个集理论：ZF可能与不可访问的基数，HF，理论的遗传有限集。在这些理论之上，我们开发了一个通常的集合理论的功能，序数和不动点理论的建设。然后，我们证明了健全的几个模型的构造演算，其扩展与无限层次的宇宙，其扩展与归纳类型的自然数，其中递归遵循基于类型的终止方法。
另一个方面是尝试和解除（大部分）这些假设。这里的目标是比较所有这些形式主义的理论优势。正如沃纳已经注意到的，ZF的替换公理在其一般形式下似乎需要一个类型理论的选择公理（TTAC）。
This work is about formalizing models of various type theories of the Calculus of Constructions family. Here we focus on set theoretical models. The long-term goal is to build a formal set theoretical model of the Calculus of Inductive Constructions, so we can be sure that Coq is consistent with the language used by most mathematicians.
One aspect of this work is to axiomatize several set theories: ZF possibly with inaccessible cardinals, and HF, the theory of hereditarily finite sets. On top of these theories we have developped a piece of the usual set theoretical construction of functions, ordinals and fixpoint theory. We then proved sound several models of the Calculus of Constructions, its extension with an infinite hierarchy of universes, and its extension with the inductive type of natural numbers where recursion follows the type-based termination approach.
The other aspect is to try and discharge (most of) these assumptions. The goal here is rather to compare the theoretical strengths of all these formalisms. As already noticed by Werner, the replacement axiom of ZF in its general form seems to require a type-theoretical axiom of choice (TTAC).