The failure of cut-elimination in cyclic proof for first-order logic with inductive definitions
Logic in Computer Science
2024-02-16 v4 Logic
Abstract
A cyclic proof system is a proof system whose proof figure is a tree with cycles. The cut-elimination in a proof system is fundamental. It is conjectured that the cut-elimination in the cyclic proof system for first-order logic with inductive definitions does not hold. This paper shows that the conjecture is correct by giving a sequent not provable without the cut rule but provable in the cyclic proof system.
Cite
@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}
}
Comments
18 pages