Syntactic cut-elimination for common knowledge (Q1024553)

The logic of common knowledge has been formulated by Alberucci and Jäger in a sequential system with a rule of infinite premises so as to enjoy completeness, from which then follows the cut-elimination theorem indirectly. There are also several variations of the logic formulated in cut-free sequential systems but a syntactical cut-elimination proof has not been shown for any of them. In this paper, the authors formulate the logic in a system on nested sequents (i.e., trees of sequents), featuring inference rules to apply inside of such trees like a Schütte-type formulation, and show that the system allows a straightforward syntactical cut-elimination procedure establishing at the same time a non-trivial bound on the proof-depth charaterized by the Veblen function. The co-embeddability between the system and that of Alberucci and Jäger is also proved, which therefore gives rise to a syntactical proof of cut-elimination for the system of Alberucci and Jäger as well as a non-trivial bound of the proof-depth characterized similarly. It is also noted that the method works for many variations of the logic.