一句话：证明马尔可夫原理在含自然数和一个宇宙的依赖类型论中不可派生，并给出保持一致性的扩展及规范化论证。
本文研究马尔可夫原理（Markov's principle）能否在含自然数类型和一个宇宙的依赖类型论中推导出来。一种思路是观察该原理在 Cantor 空间上的层模型（sheaf model）中不成立，因为它在模型的泛型点处失效。作者转而设计了一个类型论扩展，直观上向类型论加入 Cantor 空间的泛型点，并通过规范化论证证明该扩展是一致的。在此扩展中，马尔可夫原理并不成立，因此它不能在原依赖类型论中被证明。该结果给出了马尔可夫原理相对于该类类型论的独立性。
In this paper, we show that Markov's principle is not derivable in dependent type theory with natural numbers and one universe. One way to prove this would be to remark that Markov's principle does not hold in a sheaf model of type theory over Cantor space, since Markov's principle does not hold for the generic point of this model. Instead we design an extension of type theory, which intuitively extends type theory by the addition of a generic point of Cantor space. We then show the consistency of this extension by a normalization argument. Markov's principle does not hold in this extension, and it follows that it cannot be proved in type theory.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{CoquandM17,
title = {The Independence of Markov's Principle in Type Theory},
author = {Thierry Coquand and Bassel Mannaa},
journal = {Logical Methods in Computer Science},
volume = {Volume 13, Issue 3},
year = {2017},
doi = {10.23638/lmcs-13(3:10)2017}
}