An extended predicative definition of the Mahlo universe
An extended predicative definition of the Mahlo universe
复制标题
Mahlo 宇宙的扩展预测定义
DOI：
--
复制
发表时间：
--
期刊：
影响因子：
--
通讯作者：
Anton Setzer
中科院分区：
文献类型：
--
作者：
Reinhard Kahle;Anton Setzer
在本文中，我们使用扩展的谓词方法开发显式数学中的Mahlo宇宙。我们的方法不同于类型论中通常的构造，在类型论中Mahlo宇宙有一个构造函数，它将Mahlo宇宙中集合族的所有总函数引用到它自己；在缺乏进一步分析的情况下，这样的构造是不可预测的。通过扩展的预测方法，我们的意思是宇宙是从下面构建的，即使它们具有不可预测的特征
In this article we develop a Mahlo universe in Explicit Mathematics using extended predicative methods. Our approach differs from the usual construction in type theory, where the Mahlo universe has a constructor that refers to all total functions from families of sets in the Mahlo universe into itself; such a construction is, in the absence of a further analysis, impredicative. By extended predicative methods we mean that universes are constructed from below , even if they have impredicative characteristics