Cut-elimination for knowledge logics with interaction

Abstract

In the article, multimodal logics K4n and S4n with the central agent axiom are analysed. The Hilbert type calculi are presented, then the Gentzen type calculi with cut are derived, and the proofs of the cut-eliminationtheorems are outlined. The work shows that it is possible to construct an analytical Gentzen type calculi for these logics.

Keywords

• K4n
• S4n
• interaction axiom
• cut elimination
• central agen.