归纳形式拓扑的可实现语义，Church论题和选择公理
摘要：在本文中，我们提出了一种Kleene实现语义，用于扩展的intensional level的Minimalist Foundation（mtt），该mtt还加入了归纳生成的形式拓扑、Church's thesis和axiom of choice。这种语义是扩展自先前工作中用于表明intensional level的Minimalist Foundation与axiom of choice和formal Church's thesis的一致性的语义。这里的主要创新之处在于，这种语义在Aczel构建的CZF（具体集合论）的基础上进行形式化表示。
作者：Maria Emilia Maietti, Samuele Maschio and Michael Rathjen
论文ID：1905.11966
分类：Logic
分类简称：math.LO
提交时间：2023-06-22