paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Separating Markov's Principles

分离 Markov 原理
LICS Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science2024匹配度 1/10 · 该论文研究构造数学与类型论中 Markov 原理的强度分离，属于形式语义和定理证明工程，但未涉及 LLM/Agent、静态分析、浮点程序分析或贝叶斯程序分析，与用户研究画像的核心交叉方向基本无关。引用 6 inbox
Liron Cohen, Yannick Forster, Dominik Kirst, Bruno Da Rocha Paiva, Vincent Rahli
形式语义定理证明与证明工程
crossref: 2026-09-12dblp: 2026-09-12

AI 速览

一句话：澄清构造数学中三种 Markov 原理变体的强度关系，并证明它们严格分离。

构造数学中有多种关于可判定谓词与 Σ⁰₁ 的定义，导致形式上不等价的 Markov 原理，文献常混淆这一点。本文将三种自然变体 MPP、MPB、MPPR 分别与 Post 定理的不同表述、计算终止稳定性、Σ⁰₁ 理论相对模型语义的完备性，以及扩展自然数与树的有限性原理建立等价。作者在 Martin-Löf 构造类型论（MLTT）中证明 MPP 严格强于 MPB，MPB 严格强于 MPPR，从而实现上述定理的分离。分离通过带效应类型论中的 MLTT 模型构造完成，重复使用可追溯至 Kreisel 的效应技术既反驳又满足受限变体。所有结果均由证明助手机器验证。

问题
构造数学中 Σ⁰₁ 与可判定谓词有多种定义，使 Markov 原理出现不等价变体，并导致文献中的错误断言。
方法
在 MLTT 中建立三种变体与 Post 定理、终止稳定性、语义完备性和有限性原理的等价，并用带效应类型论的模型构造证明严格强度分离。
评估
通过构造区分 MPP、MPB、MPPR 的模型，并在证明助手中机器验证全部等价与分离结果。
原文摘要（Abstract）

Markov's principle (MP) is an axiom in some varieties of constructive mathematics, stating that Σ01 propositions (i.e. existential quantification over a decidable predicate on N) are stable under double negation. However, there are various non-equivalent definitions of decidable predicates and thus Σ01 in constructive foundations, leading to non-equivalent Markov's principles. While this fact is well-reported in the literature, it is often overlooked, leading to wrong claims in standard references and published papers. In this paper, we clarify the status of three natural variants of MP in constructive mathematics, by giving respective equivalence proofs to different formulations of Post's theorem, to stability of termination of computations, to completeness of various proof systems w.r.t. some model-theoretic semantics for Σ01-theories, and to finiteness principles for both extended natural numbers and trees. The first definition (MPP) uses a purely propositional definition of Σ01 for predicates on natural numbers N, while the second one (MPB) relies on functions N → B, and the third one (MPPR) on a subset of these functions expressible in an explicit model of computation. We then prove that MPP is strictly stronger than MPB, and that MPB is strictly stronger than MPPR for variants of Martin-Löf's constructive type theory (MLTT), leading to separation results for the above theorems. These separations are achieved through a model construction of MLTT in [EQUATION], a type theory parameterised by effects, which can be syntactically restricted as needed. We replicate effectful techniques going back to Kreisel twice to refute different logical principles (first MPB, then MPP), while simultaneously satisfying variants of those principles (first MPPR, then MPB) when effects are restricted. All our results are checked by a proof assistant.

链接与引用

DOI 原文 · PDF（开放获取） · DBLP

BibTeX 
@inproceedings{00010KPR24,
  title = {Separating Markov's Principles},
  author = {Liron Cohen and Yannick Forster and Dominik Kirst and Bruno Da Rocha Paiva and Vincent Rahli},
  booktitle = {LICS},
  year = {2024},
  doi = {10.1145/3661814.3662104}
}