  This paper investigates first-order game logic and first-order modal
mu-calculus, which extend their propositional modal logic counterparts with
first-order modalities of interpreted effects such as variable assignments.
Unlike in the propositional case, both logics are shown to have the same
expressive power and their proof calculi to have the same deductive power. Both
calculi are also mutually relatively complete.
  In the presence of differential equations, corollaries obtain usable and
complete translations between differential game logic, a logic for the
deductive verification of hybrid games, and the differential mu-calculus, the
modal mu-calculus for hybrid systems. The differential mu-calculus is complete
with respect to first-order fixpoint logic and differential game logic is
complete with respect to its ODE-free fragment.
