A Finite Axiomatization of Inductive-Recursive Definitions
A Finite Axiomatization of Inductive-Recursive Definitions
复制标题
归纳递归定义的有限公理化
DOI：
--
复制
发表时间：
1999
期刊：
影响因子：
--
通讯作者：
A. Setzer
中科院分区：
文献类型：
--
作者：
P. Dybjer;A. Setzer
归纳-递归是一种模式，它形式化了马丁-洛夫类型论中引入新集合的原则。它指出，我们可以归纳地定义一个集合，同时通过结构递归将一个函数从这个集合定义为任意类型。这大大扩展了归纳定义集的概念，并允许我们引入宇宙和高阶宇宙（但不是Mahlo宇宙）。本文给出归纳递归定义的有限公理化。我们证明了一致性，通过构建一个集理论模型，利用一个Mahlo基数。
Induction-recursion is a schema which formalizes the principles for introducing new sets in Martin-Lof's type theory. It states that we may inductively define a set while simultaneously defining a function from this set into an arbitrary type by structural recursion. This extends the notion of an inductively defined set substantially and allows us to introduce universes and higher order universes (but not a Mahlo universe). In this article we give a finite axiomatization of inductive-recursive definitions. We prove consistency by constructing a set-theoretic model which makes use of one Mahlo cardinal.