映射论与ZFC集合论的关联及一致性证明探索

"映射论与ZFC的关系及一致性证明" 映射论（Map Theory）是一种理论计算机科学中的概念，它是无类型λ-演算的扩展，旨在成为计算机科学和数学的共同基础。这一理论由Klaus Grue提出，将一阶逻辑和集合论的基本概念，如真值、逻辑连接词、量词、集合成员关系和集合相等，全部解释为术语。映射论的创新之处在于它能够提供对常见集合论构造的计算解释，包括归纳数据类型的构建。 本篇论文中，作者Thierry Vallée探讨了映射论的两个版本，一个是基于良基集的传统版本，另一个则考虑了非良基集并允许进行共归纳推理，这使得映射论能够直接表示共归纳的数据类型和循环过程。这种扩展对于理解和处理那些在传统集合论中难以处理的结构特别有用。 作者平行介绍了这两个版本的映射论与ZFC（Zermelo-Fraenkel集合论）的关系。ZFC是现代数学中广泛接受的集合论基础，它包含一套公理系统，用于描述集合的性质和操作。论文中展示了如何在映射论中嵌入ZFC，这表明映射论足够强大，可以表达ZFC所能表达的全部数学概念。 在证明方面，Vallée提出了这两个版本的映射论之间的一致性证明。他们相对一致性的一个关键部分是证明存在一个强不可及的基数，这在κ-连续语义中完成。κ-连续语义是Scott连续语义（其中κ=ω，即自然数集合）的推广，适用于任何正则基数κ。这种语义提供了一种理解集合和函数的连续性的方法。 此外，文章还涉及了λ-演算和命题演算的公理、非单调影响、命题演算的嵌入以及量化公理的满足性。在谓词演算部分，讨论了量化域、常数ε和量化器的定义，以及如何解释一阶理论。最后，文中详细阐述了如何在映射论中嵌入ZFC的扩展版本ZFC-ext，以及相关的可拓性公理（MTF）和诱导原理（MTA）。 关键词：映射论、反基础、余归纳、非类型λ-演算、集合论、κ-连续语义、互模拟，这些都是这篇论文探讨的核心概念，它们对于理解映射论与传统集合论之间的联系，以及它们在处理复杂数学构造时的差异至关重要。