使用Church的论题和选择公理进行归纳和余归纳拓扑生成
摘要：用于预测构造性数学的极简基础MF的扩展MFcind及其相关的归纳和伪归纳定义被考虑在内，以生成Sambin's Positive拓扑。特别是MFcind的内涵层mTTcind通过扩展具有归纳定义的另一个理论mTTind来进行定义，后者通过仅增加归纳定义来扩展MF的内涵层mTT。在先前的工作中，我们已经证明了mTTind通过在Aczel的CZF + REA中进行解释与形式化Church's论题CT和选择公理AC一致。我们的目标是通过通过不同的解释来将mTTcind + CT + AC的一致性降低到CZF + REA的一致性，以展示对mTTind添加伪归纳定义不会增加其一致性的预期。实际上，我们通过两种方法达到了我们的目标。一个方法是首先将mTTcind + CT + AC解释为扩展了并集常规扩展公理REA\_U和相对化依赖选择公理RDC的CZF理论，然后将CZF + REA\_U + RDC解释为带有Palmgren's超宇宙S的Martin-L"of类型理论的MLS*版本。最后一步是将MLS*解释回CZF + REA。另一种方法是首先直接将mTTcind + AC + CT解释为扩展了CT的Palmgren's超宇宙版本的Martin-L"of类型理论，然后将其解释回CZF + REA。第一种方法的一个关键优势是CZF + REA\_U + RDC理论也支持MFcind的外延层的预期集合论解释。最后，我们证明了除mTTcind + AC + CT外，所有考虑的理论都具有相同的证明论基础强度。
作者：Maria Emilia Maietti, Samuele Maschio, Michael Rathjen
论文ID：2103.16592
分类：Logic
分类简称：math.LO
提交时间：2023-06-22