Cut elimination for \(\mathrm{S4}_n\) and \(\mathrm{K4}_n\) with the central agent axiom (Q1042695)

Multimodal logic S4\(_n\) has \(n\) modalities \(K_c\) (for the central agent), \(K_1,\ldots,K_{n-1}\), with S4-axioms for each of the modalities plus interaction axioms : \(K_c\rightarrow K_i\) for all \(i\). The corresponding Gentzen-type system admitting cut elimination has the familiar S4-rules plus the interaction rule: from \(K\Gamma\rightarrow A\) infer \(K\Gamma,\Gamma_1\rightarrow \Delta,K_cA\), where \(K\Gamma\) consists of formulas of the form \(K_iB\).