-
Views
-
Cite
Cite
Daniyar Shamkanov, On structural proof theory of the modal logic K+ extended with infinitary derivations, Logic Journal of the IGPL, 2024;, jzae121, https://doi.org/10.1093/jigpal/jzae121
- Share Icon Share
Abstract
We consider an extension of the modal logic of transitive closure |$\textsf{K}^{+}$| with certain infinitary derivations and present a sequent calculus for this extension, which allows non-well-founded proofs. We establish continuous cut-elimination for the given calculus using fixed-point theorems for contractive mappings. The infinitary derivations mentioned above are well founded and countably branching, while the non-well-founded proofs of the sequent calculus can only be finitely branching. The ordinary derivations in |$\textsf{K}^{+}$|, as we show additionally, correspond to the non-well-founded proofs of the calculus that are regular and cut-free. Therefore, in this article, we explore the relationship between deductive systems for |$\textsf{K}^{+}$| with well-founded infinitely branching derivations and (regular) non-well-founded finitely branching proofs.