Cut elimination for knowledge logic with interaction

Abstract

In the article the multimodal logic Tn with central agent interaction axiom is analysed. The Hilbert type calculi is presented, then Gentzen type calculi with cut is derived and the proof of cutelimination theorem is outlined. The work shows that it is possible to construct a Gentzen type calculi without cut for this logic.

Keywords

• multimodal logic
• Tn
• interaction axiom
• cut elimination