 This fact is the basis for proving that Backward Induction is definable in First Order Fix point logic LFP(FFO) (van Benthem &amp; Gheerbrant 2010). Results in this line of research connect game solution and game-theoretic equilibria with fixed-point logics of computation. In simple settings, such as that of Zermelo’s Theorem mentioned earlier, modal fixed-point logics akin to μ-calculus suffice.