一阶逻辑带归纳定义循环证明中消去切割的失败
计算机科学中的逻辑
2024-02-16 v4 逻辑
摘要
循环证明系统是一种证明图为带环树的证明系统。证明系统中的消去切割是基础性的。据推测，一阶逻辑带归纳定义的循环证明系统中的消去切割不成立。本文通过给出一个不使用切割规则不可证但在循环证明系统中可证的相继式，表明该猜想是正确的。
引用
@article{arxiv.2106.11798,
title = {The failure of cut-elimination in cyclic proof for first-order logic with inductive definitions},
author = {Yukihiro Oda and James Brotherston and Makoto Tatsuta},
journal= {arXiv preprint arXiv:2106.11798},
year = {2024}
}
备注
18 pages