Game logic and its applications. II (Q1357377)

This is a sequel to our development of the game logic framework. In Part I [the authors, ibid. 57, No. 2-3, 325-354 (1996; Zbl 0858.03035)] of this paper, we presented the framework in the Hilbert style formulation and showed some applications of the framework to game theory -- the epistemic axiomatization of Nash equilibrium and the undecidability on the playability of a game. To obtain the undecidability results (Theorems 6.2 and 6.3 of Part I), we used a result called term existence theorem. This is a metatheorem stating an evaluation of provability on an existential formula. The Hilbert style formulation is convenient in presentation, but is difficult in managing an evaluation of such provability. In general, it would be better to reformulate the Hilbert style formulation into a Gentzen style sequent calculus for the purpose of evaluating provability. This paper provides a Gentzen style formulation of the game logic framework, and proves the cut-elimination theorem. As its application, we prove the term existence theorem used in Part I.