扩展构造演算的直觉主义集合论模型
计算机科学中的逻辑
2015-02-17 v3
摘要
Werner 的集合论模型是 ECC 最直观的模型之一。它结合了直谓宇宙的函数视角与非直谓类型 Prop 的塌缩视角。然而，Prop 的这一模型过于粗糙，以至于排中律在其中成立。在本文中，我们将 Prop 解释到一个拓扑空间（Heyting 代数的一种特殊情况）中，使其更具直觉主义色彩而不牺牲简单性。我们证明了可靠性，并展示了我们模型的一些应用。
关键词
引用
@article{arxiv.1412.2235,
title = {An Intuitionistic Set-theoretical Model of the Extended Calculus of Constructions},
author = {Masahiro Sato},
journal= {arXiv preprint arXiv:1412.2235},
year = {2015}
}