具有谓词归纳和判断平等的CC证明无关模型
Proof-irrelevant model of CC with predicative induction and judgmental equality
摘要：
我们提出了一个集理论，证明无关模型的构造演算（CC）的预测归纳和判断的Zermelo-Fraenkel集理论与公理可数许多不可访问的基数平等。我们使用Aczel的跟踪编码，它是为任何函数类型通用定义的，无论是非谓词的。直接和具体的解释同时归纳和相互递归的功能也提供了扩展Dybjer的解释的基础上Aczel的规则集。我们的模型可以看作是真值表方法的高阶推广。我们提供了一个相对简单的类型论的一致性证明，它可以作为一个定理证明的基础。
英文摘要：
We present a set-theoretic, proof-irrelevant model for Calculus of Constructions (CC) with predicative induction and judgmental equality in Zermelo-Fraenkel set theory with an axiom for countably many inaccessible cardinals. We use Aczel's trace encoding which is universally defined for any function type, regardless of being impredicative. Direct and concrete interpretations of simultaneous induction and mutually recursive functions are also provided by extending Dybjer's interpretations on the basis of Aczel's rule sets. Our model can be regarded as a higher-order generalization of the truth-table methods. We provide a relatively simple consistency proof of type theory, which can be used as the basis for a theorem prover.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
