  Game logic was introduced by Rohit Parikh in the 1980s as a generalisation of
propositional dynamic logic (PDL) for reasoning about outcomes that players can
force in determined 2-player games. Semantically, the generalisation from
programs to games is mirrored by moving from Kripke models to monotone
neighbourhood models. Parikh proposed a natural PDL-style Hilbert system which
was easily proved to be sound, but its completeness has thus far remained an
open problem.
  In this paper, we introduce a cut-free sequent calculus for game logic, and
two cut-free sequent calculi that manipulate annotated formulas, one for game
logic and one for the monotone mu-calculus, the variant of the polymodal
mu-calculus where the semantics is given by monotone neighbourhood models
instead of Kripke structures. We show these systems are sound and complete, and
that completeness of Parikh's axiomatization follows. Our approach builds on
recent ideas and results by Afshari & Leigh (LICS 2017) in that we obtain
completeness via a sequence of proof transformations between the systems. A
crucial ingredient is a validity-preserving translation from game logic to the
monotone mu-calculus.
