Martin-Löf 归纳定义的经典系统不等价于循环证明
计算机科学中的逻辑
2023-06-22 v5
摘要
一种称为 CLKID-omega 的循环证明系统为我们提供了表示归纳定义和高效证明搜索的另一种方式。Brotherston 在 2005 年的论文中表明，CLKID-omega 的可证性包含了 LKID（Martin-Löf 风格带归纳定义的一阶经典逻辑）的可证性，并猜想二者等价。该等价性自 2011 年以来一直是一个开放问题。本文证明 CLKID-omega 与 LKID 确实不等价。本文在由 0、后继、自然数谓词以及一个用于表示 2-Hydra 的二元谓词符号构成的一阶语言中，在这两个系统内考虑一个称为 2-Hydra 的命题。本文通过构造某个该命题为假的海廷模型，证明 2-Hydra 命题在 CLKID-omega 中可证，但在 LKID 中不可证。
引用
@article{arxiv.1712.09603,
title = {Classical System of Martin-Lof's Inductive Definitions is not Equivalent to Cyclic Proofs},
author = {Stefano Berardi and Makoto Tatsuta},
journal= {arXiv preprint arXiv:1712.09603},
year = {2023}
}