Game logic is strong enough for parity games (Q1425188): Difference between revisions

This is another paper from the interesting Studia Logica special issue on Game Logics and Game Algebras edited by Marc Pauly and Rohit Parikh. Berwanger investigates Game Logic as developed by \textit{R. Parikh} [Ann. Discrete Math. 24, 111--139 (1985; Zbl 0552.90110)] interpreted on Kripke structures in the alternating hierarchy of the \(\mu\)-calculus as developed by \textit{J. C. Bradfield} [Theor. Comput. Sci. 195, No. 2, 133--153 (1998; Zbl 0915.03017)]. A lot of interesting logics are subsumed by very low levels of the alternating hierarchy. However, for each \(n\), the formula W\(^n\) expressing ``player I has a winning strategy in parity games with \(n\) priorities'' is strictly at level \(n\) of the alternating hierarchy. In this paper, the author proves that W\(^n\) is expressible in Game Logic. Thus, Game Logic is not captured by any finite level of the alternating hierarchy. Since \textit{Marc Pauly} has proved that every formula of game logic is equivalent to an L\(_\mu\) formula with two variables [Logic for social software, Amsterdam: ILLC Publications DS-2001-10 (2001)], Berwanger gets as a corollary that the two-variable fragment of L\(_\mu\) is not captured by any finite level of the alternating hierarchy.