Implicit quantification for modal reasoning in large games

Reasoning about equilibria in normal form games involves the study of players’ incentives to deviate unilaterally from any profile. In the case of large anonymous games, the pattern of reasoning is different. Payoffs are determined by strategy distributions rather than strategy profiles. In such a game each player would strategise based on expectations of what fraction of the population makes some choice, rather than respond to individual choices by other players. A player may not even know how many players there are in the game. Logicising such strategisation involves many challenges as the set of players is potentially unbounded. This suggests a logic of quantification over player variables and modalities for player deviation, but such a logic is easily seen to be undecidable. Instead, we propose a propositional modal logic using player types as names and implicit quantification over players. With modalities for player deviation and transitive closure, the logic can be used to specify game equilibrium and interesting patterns of reasoning in large games. We show that the logic is decidable and present a complete axiomatisation of the valid formulas.