Common knowledge logic and game logic

We show the faithful embedding of common knowledge logic CKL into game logic GL, that is. CKL is embedded into GL and GL is a conservative extension of the fragment obtained by this embedding. Then many results in GL are available in CKL, and vice versa. For example, an epistemic consideration of Nash equilibrium for a game with pun: strategies in GL is carried over to CKL. Another important application is to obtain a Gentzen-style sequent calculus formulation of CKL and its cut-elimination. The faithful embedding theorem is proved for the KD4-type propositional CKL and GL, but it holds for some variants of them.