Abstract

Non-determined game logic is the logic of two player board games where the game may end in a draw: unlike the case with determined games, a loss of one player does not necessarily constitute of a win of the other player. A calculus for non-determined game logic is given in [4] and shown to be complete. The calculus adds a new rule for the treatment of greatest fixpoints, and a new unfolding axiom for iterations of the universal player. The technique of the completeness proof is inspired by the canonical model construction for propositional dynamic logic (PDL). In this paper, this is extended to the logic of determined games. It is proved that the calculus for nondetermined game logic, together with the axiom of determinacy, is complete for determined game logic. Next, it is shown that the axioms and rules of the new calculus can all be derived from the calculus proposed by Parikh in [5], for which the completeness was still open. This proves Parikh’s conjecture that his calculus is complete for determined games.