On structural proof theory of the modal logic K+ extended with infinitary derivations
arXiv:2310.10309 · doi:10.1093/jigpal/jzae121
Abstract
We consider an extension of the modal logic of transitive closure K+ with some inifinitary derivations and present a sequent calculus for this extension, which allows non-well-founded proofs. For the given calculus, we obtain the cut-elimination theorem following the lines of so called continuous cut elimination. Our consideration also covers ordinary proofs of K+ since they correspond to cyclic cut-free proofs of the presented sequent calculus.