The proof theory of common knowledge

Michel Martí

Thomas Studer

pp. 433-455

in: Hans van Ditmarsch, Paul-Gabriel Sandu (eds), Jaakko Hintikka on knowledge and game-theoretical semantics, Berlin, Springer, 2018

Abstract

Common knowledge of a proposition A can be characterized by the following infinitary conjunction: everybody knows A and everybody knows that everybody knows A and everybody knows that everybody knows that everybody knows A and so on. We present a survey of deductive systems for the logic of common knowledge. In particular, we present two different Hilbert-style axiomatizations and two infinitary cut-free sequent systems. Further we discuss the problem of syntactic cut-elimination for common knowledge. The paper concludes with a list of open problems.