
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.
infinitary sequent calculus, nested sequents, Logic, common knowledge, Veblen function, Logics of knowledge and belief (including belief change), logic of common kowledge, proof-depth, cut elimination, Theoretical Computer Science, deep sequents, infinitary sequent system, Cut-elimination and normal-form theorems, Modal logic (including the logic of norms), logic of common belief, Computer Science(all)
infinitary sequent calculus, nested sequents, Logic, common knowledge, Veblen function, Logics of knowledge and belief (including belief change), logic of common kowledge, proof-depth, cut elimination, Theoretical Computer Science, deep sequents, infinitary sequent system, Cut-elimination and normal-form theorems, Modal logic (including the logic of norms), logic of common belief, Computer Science(all)
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 22 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Top 10% | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Top 10% | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Top 10% |
