Syntactic Cut-elimination for Common Knowledge

We see a cut-free infinitary sequent system for common knowledge. Its sequents are essentially trees and the inference rules apply deeply inside of these trees. This allows to give a syntactic cut-elimination procedure which yields an upper bound of ϕ20 on the depth of proofs, where ϕ is the Veblen function.