On structural proof theory of the modal logic K+ extended with infinitary derivations

TL;DR

This paper extends the modal logic K+ with infinitary derivations, introduces a sequent calculus allowing non-well-founded proofs, and proves cut-elimination, connecting cyclic proofs with traditional proofs.

Contribution

It presents a novel sequent calculus for K+ with infinitary and non-well-founded proofs, and establishes a cut-elimination theorem for this extended logic.

Findings

Cut-elimination theorem established for the extended calculus

Non-well-founded proofs correspond to cyclic proofs of K+

The calculus generalizes ordinary proofs of K+

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.