Martin-Löf扩展类型论的Kripke语义
Kripke Semantics for Martin-Löf's Extensional Type Theory
摘要：
众所周知，简单类型论对于非标准集值模型是完备的。标准模型的完备性仅适用于某些扩展类的模型，例如，闭范畴类。类似地，依赖类型论对于局部carnival闭范畴也是完备的。然而，通常很难建立依赖类型论解释的连贯性，即，来证明平等表达的解释确实是平等的。已经使用了几类模型来解决这个问题。我们的调查作出贡献，给出了一个语义，是标准的，连贯的，并足够普遍的完整性，同时保持相对容易计算。我们的模型解释类型的马丁-洛夫的外延依赖类型论作为集索引的偏序集，或等价地，作为纤维化的偏序集。这种语义可以看作是对Kripke模型中直觉一阶逻辑解释的依赖类型论的推广。这就产生了一个简单的连贯的模型理论，相对于它，简单的和依赖的类型论是健全的和完备的。
英文摘要：
It is well-known that simple type theory is complete with respect to non-standard set-valued models. Completeness for standard models only holds with respect to certain extended classes of models, e.g., the class of cartesian closed categories. Similarly, dependent type theory is complete for locally cartesian closed categories. However, it is usually difficult to establish the coherence of interpretations of dependent type theory, i.e., to show that the interpretations of equal expressions are indeed equal. Several classes of models have been used to remedy this problem. We contribute to this investigation by giving a semantics that is standard, coherent, and sufficiently general for completeness while remaining relatively easy to compute with. Our models interpret types of Martin-Löf's extensional dependent type theory as sets indexed over posets or, equivalently, as fibrations over posets. This semantics can be seen as a generalization to dependent type theory of the interpretation of intuitionistic first-order logic in Kripke models. This yields a simple coherent model theory, with respect to which simple and dependent type theory are sound and complete.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
