A Higher-arity Sequent Calculus for Model Linear Logic (Proof theory and proving)

Abstract

We propose a cut-free sequent calculus for multiplicative exponential linear logic with S4 necessity and possibility modalities. The calculus has the so-calld "higher-arity" judgment to formalize the exponentials and S4 modalities neatly. An the properties follow from the model of proofs for a higher-arity sequent calculus of classical modal logic S4, which is also proposed and studied here.