一句话：提出带破坏的博弈逻辑 GLs，证明其表达力等价于模态 μ-演算，并给出完备的 Hilbert 证明演算。
论文在 Parikh 博弈逻辑基础上引入单一原语“设置陷阱/破坏”，得到带破坏的博弈逻辑 GLs，用于建模玩家可在游戏过程中改变规则的无限破坏博弈。作者证明 GLs 的表达力严格强于经典博弈逻辑，且恰好等价于模态 μ-演算，从而揭示模态不动点逻辑中的嵌套递归与破坏博弈中的对抗性动态规则变化之间的紧密联系。文中提出自然的 Hilbert 风格证明演算，并通过语法等表达性归约证明其完备性；作为推论，还得到 Parikh 博弈逻辑演算的一个简单扩展的完备性。
Game logic with sabotage (GLs) 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. GLs 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, GLs 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 GLs is presented and proved complete using syntactic equiexpressiveness reductions. The completeness of a simple extension of Parikh's calculus for game logic follows.