完全依赖型 CC{\omega} 的直觉主义集合论模型
计算机科学中的逻辑
2020-10-26 v1 逻辑
摘要
Werner 的集合论模型是 CIC 最简单的模型之一。它将谓词宇宙的函数视图与不可谓词排序 Prop 的坍缩视图相结合。然而该 Prop 模型过于粗糙，以致排中律成立。沿用我们之前的工作，我们将 Prop 解释为拓扑空间（海廷代数的特例），以在不牺牲简洁性的前提下使模型更具直觉主义色彩。我们改进了该工作，利用 Alexandroff 空间给出依赖积类型的完整解释。我们还通过添加对列表的支持，将方法推广至归纳类型。
引用
@article{arxiv.2010.12504,
title = {An Intuitionistic Set-theoretical Model of Fully Dependent CC{\omega}},
author = {Masahiro Sato and Jacques Garrigue},
journal= {arXiv preprint arXiv:2010.12504},
year = {2020}
}