Labeled sequent calculi for modal logics and implicit contractions (Q377468)

The author investigates an issue directly concerning Negri's labeled sequent calculi, see [\textit{S. Negri}, J. Philos. Log. 34, No. 5--6, 507--544 (2005; Zbl 1086.03045)], based on Kleene's G3-style calculi [\textit{S. C. Kleene}, Introduction to metamathematics. Amsterdam: North-Holland Publishing Co. (1952; Zbl 0047.00703)] related to the standard modal systems K, D, T, K4, S4 and S5. The main result is that labeled calculi for the modal logics K and D remain complete w.r.t. valid tree-labeled sequents, that is, valid sequents whose relational part encodes a tree-like (not necessarily rooted) structure. The result is obtained when the unique rule containing a harmful implicit contraction is modified into a contraction-free one making the proof-search space finite.