Invited Talk: Thomas Studer

Syntactic Cut-Elimination for Common Knowledge

(joint work with Kai Brünnler)

There is no syntactic cut-elimination procedure available for the classical sequent systems for logic of common knowledge. We present an infinitary sequent system with sequents that are essentially trees and with inference rules that apply deeply indside of these trees. This deep system allows to give a straightforeward syntactic cut-elimination procedure. The embedding of a Hilbert system into the deep system yields an upper bound of \phi 2 0 on the depth of proofs, where \phi is the Veblen function.