归纳定义的真值谓词与无限下降证明的逻辑复杂性
计算机科学中的逻辑
2026-03-05 v1 计算复杂性
摘要
关于归纳定义关系和结构的形式推理，广为人知不仅具有数学兴趣，也在计算机科学中至关重要，可用于验证程序和算法的属性。近期吸引注意的包括循环证系统 CLKID-omega 和无限下降证明系统 LKID-omega 等多种归纳定义谓词的证系统。尽管已阐明了它们可证性之间的关系，但其逻辑复杂性鲜有研究。无限下降证明系统 LKID-omega 是一种用于归纳定义的无限证系统，允许证明图中存在无限路径。它是循环证系统的基础。本文表明 LKID-omega 可证性的逻辑复杂性为 (Pi-1-1)-完备。为证明此点，首先表明标准模型中归纳定义的有效性等价于标准项模型中归纳定义的有效性。随后，本文在此等价性基础上，借助归纳定义的数值编码，扩展了 Girard 教科书中给出的 omega 语言真值谓词。这表明标准模型中归纳定义的有效性为 (Pi-1-1) 关系。最后，基于 LKID-omega 对标准模型的完备性，表明 LKID-omega 可证性的逻辑复杂性为 (Pi-1-1)-完备。
引用
@article{arxiv.2603.04015,
title = {Truth Predicate of Inductive Definitions and Logical Complexity of Infinite-Descent Proofs},
author = {Sohei Ito and Makoto Tatsuta},
journal= {arXiv preprint arXiv:2603.04015},
year = {2026}
}
备注
In Proceedings LTT 2026, arXiv:2603.02912