Sequent Calculi for Global Modal Consequence Relations

The global consequence relation of a normal modal logic Lambda is formulated as a global sequent calculus which extends the local sequent theory of Lambda with global sequent rules. All global sequent calculi of normal modal logics admits global cut elimination. This property is utilized to show that decidability is preserved from the local to global sequent theories of any normal modal logic over K4. The preservation of Craig interpolation property from local to global sequent theories of any normal modal logic is shown by proof-theoretic method.