Extensive Game Logic

Origin. Bonanno's modal logic of extensive games (2001, 2002); Harrenstein, van der Hoek, Meyer, and Witteveen on game-theoretic reasoning in modal logic (2002, 2003); van Benthem's "Games in dynamic-epistemic logic" (2001) and Logic in Games (2014). Logic for extensive form games. Tree-structured games with perfect/imperfect information. Epistemic reasoning about game positions. Backward induction, subgame perfection.

Models. Games as trees with information. Extensive form: game tree with nodes, actions, players. Information sets: what player knows when acting. Payoffs at terminal nodes. Logic reasons about strategies, knowledge, equilibria.

Formalism.

Extensive form game: Γ = (N, H, Z, P, fc, (Iᵢ), (uᵢ))

• N: players
• H: histories (nodes)
• Z ⊆ H: terminal histories
• P: H\Z → N (player function)
• fc: choice function
• Iᵢ: information sets for player i
• uᵢ: Z → ℝ (payoffs)

Modal operators:

• ⟨a⟩φ: after action a, φ holds
• Kᵢφ: player i knows φ
• ⟨⟨i⟩⟩φ: player i has strategy for φ

Information and strategy: At information set I: player knows I but not exact node. Strategy: function from information sets to actions.

Backward induction: [BI]φ: φ holds under backward induction. Captures rational play in perfect information games.

Subgame perfection: Strategy is equilibrium in every subgame. Expressible via nested strategic quantification.

Symbols.

Metatheory. The classical results the logics formalize are Zermelo's (1913), that every finite perfect-information game is determined by backward induction, and Kuhn's (1953), that every such game has a subgame perfect equilibrium in pure strategies and that behavioural and mixed strategies coincide under perfect recall. Bonanno (2001, 2002) gave sound and complete axiomatizations of modal logics whose frames are game trees, with backward induction characterized by a frame condition rather than an algorithm. Aumann (1995) proved that common knowledge of rationality entails the backward induction outcome in generic perfect-information games; van Benthem recast the same procedure dynamically, as the fixed point reached by iterated public announcement of rationality, which makes backward induction a limit of an epistemic process rather than a primitive. On the computational side, two-player zero-sum extensive games with imperfect information and perfect recall are solvable in time polynomial in the tree via the sequence form of Koller, Megiddo, and von Stengel (1994).

Applies to. Game theory formalization. Mechanism design. Security games. Economic modeling. Multi-agent systems. Negotiation protocols. Auction theory.

Limitations. Backward induction needs perfect information and a finite horizon, and its epistemic justification is contested: Aumann's theorem and the objections of Stalnaker and Binmore turn on how a player revises beliefs after an event the analysis has already declared irrational, which the standard models leave undefined. Under imperfect information subgame perfection has almost no force, since a game with large information sets has few proper subgames, so sequential or perfect Bayesian equilibrium must be imposed instead — and these quantify over belief systems the modal language does not contain. Kuhn's equivalence of behavioural and mixed strategies fails without perfect recall, so absent-minded agents fall outside the theory. The tree is exponential in any succinct description of the game, so linear-time procedures over it are not tractable in the input. Payoffs are real numbers, and no propositional modal language expresses comparisons among them.

© 2026 Lingenic LLC