Labeled sequent calculi for modal logics and implicit contractions

The paper settles an open question concerning Negri-style labeled sequent calculi for modal logics and also, indirectly, other proof systems which make (more or less) explicit use of semantic parameters in the syntax and are thus subsumed by labeled calculi, like Brünnler’s deep sequent calculi, Poggiolesi’s tree-hypersequent calculi and Fitting’s prefixed tableau systems. Specifically, the main result we prove (through a semantic argument) is that labeled calculi for the modal logics K and D remain complete w.r.t. valid sequents whose relational part encodes a tree-like structure, when the unique rule which contains an harmful implicit contraction—by which the condition that the premises be less complex than the conclusion is violated— is modified into a contraction-free one respecting the latter condition, thus making the proof-search space finite.