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.

Symbol	Unicode	Name	Meaning
⟨a⟩	—	Action	After action a
Kᵢ	—	Knows	Player i knows
⟨⟨i⟩⟩	—	Can ensure	Strategic ability
I	—	Information set	Indistinguishable nodes
H	—	Histories	Game tree
uᵢ	—	Payoff	Utility function

Metatheory. Model checking: PTIME for specific fragments. Epistemic games: higher complexity. Connects to ATL and STIT. Complete axiomatizations for fragments. Solution concepts expressible.

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

Limitations. Perfect/imperfect information distinction crucial. Complexity with many players. Continuous payoffs not native. Tool support limited. Real games often more complex. Learning not modeled.