算术下直觉主义归纳定义与直觉主义循环证明的等价性
计算机科学中的逻辑
2017-12-12 v1 逻辑
摘要
循环证明系统为我们提供了表示归纳定义与高效证明搜索的另一种方式。2011 年 Brotherston 与 Simpson 猜想经典循环证明系统的可证性与 Martin-Lof 归纳定义经典系统的可证性等价。本文研究直觉主义逻辑下的该猜想。本文首先指出同一作者 FOSSACS 2017 论文的反模型表明直觉主义逻辑下的该猜想一般不成立。随后本文证明在算术下直觉主义逻辑下的猜想成立，即当两个系统均包含 Heyting 算术 HA 时，直觉主义循环证明系统的可证性与 Martin-Lof 归纳定义直觉主义系统的可证性相同。为此，本文还证明 HA 可证明关于归纳的 Podelski-Rybalchenko 定理与关于归纳的 Kleene-Brouwer 定理。这些结果立即给出同一作者 LICS 2017 论文中经典逻辑下算术中猜想的另一种证明。
引用
@article{arxiv.1712.03502,
title = {Equivalence of Intuitionistic Inductive Definitions and Intuitionistic Cyclic Proofs under Arithmetic},
author = {Stefano Berardi and Makoto Tatsuta},
journal= {arXiv preprint arXiv:1712.03502},
year = {2017}
}