类型论中马尔可夫原则的独立性
计算机科学中的逻辑
2023-06-22 v6
摘要
本文中，我们展示了马尔可夫原则在带有自然数和一个全集的依赖类型论中不可推导。一种证明方法是注意到马尔可夫原则在类型论在Cantor空间上的层模型上不成立，因为马尔可夫原则对该模型的泛点不成立。相反，我们设计了类型论的一个扩展，直观上通过添加Cantor空间的泛点来扩展类型论。然后我们通过规范化论证展示了该扩展的一致性。马尔可夫原则在此扩展中不成立，因此可知它不能在类型论中被证明。
引用
@article{arxiv.1602.04530,
title = {The Independence of Markov's Principle in Type Theory},
author = {Thierry Coquand and Bassel Mannaa},
journal= {arXiv preprint arXiv:1602.04530},
year = {2023}
}