Complete Game Logic with Sabotage

Game logic with sabotage (GL s ) is introduced as a simple and natural extension of Parikh's game logic with a single additional primitive, which allows players to lay traps for the opponent. GL s can be used to model infinite sabotage games, in which players can change the rules during game play. In contrast to game logic, which is strictly less expressive, GL s is exactly as expressive as the modal 𝜇-calculus. This reveals a close connection between the entangled nested recursion inherent in modal fixpoint logics and adversarial dynamic rule changes characteristic for sabotage games. A natural Hilbert-style proof calculus for GL s is presented and proved complete using syntactic equiexpressiveness reductions. The completeness of a simple extension of Parikh's calculus for game logic follows.