First-Order Game Logic and Modal Mu-Calculus

Abstract

Three decades later, Parikh’s problem has been solved: This paper investigates first-order game logic and first-order Game logic is less expressive than the modal μ-calculus [2], modal μ-calculus, which extend their propositional modal because it embeds into the two-variable fragment of μ-calculus arXiv:2201.10012v2 [cs.LO] 11 Feb 2022 logic counterparts with first-order modalities of interpreted whose variable hierarchy is strict. Completeness of the ax- effects such as variable assignments. Unlike in the proposi- iomatization for game logic was shown recently [12] based tional case, both logics are shown to have the same expres- on cut-free completeness for the modal μ-calculus [1]. sive power and their proof calculi to have the same deduc- While these results about the propositional modal logic tive power. Both calculi are also mutually relatively com- setting are exciting, this paper goes beyond the propositional plete. case of abstract actions a, b, c of unknown effect and consid- In the presence of differential equations, corollaries ob- ers first-order modalities with interpreted effects (such as as- tain usable and complete translations between differential signments x := θ to object variables). First-order modalities game logic, a logic for the deductive verification of hybrid like in first-order dynamic logic are crucial for representing games, and the differential μ-calculus, the modal μ-calculus programs [18, 19, 31] and dynamical systems [30]. for hybrid systems. The differential μ-calculus is complete This paper shows that Parikh’s problem has the oppo- with respect to first-order fixpoint logic and differential game site answer in the first-order case: first-order game logic logic is complete with respect to its ODE-free fragment. and first-order modal μ-calculus have the same expressive power, their calculi have the same deductive power and are CCS Concepts: • Theory of computation → Modal and mutually relatively complete. Consequen