Acyclicity of preferences, Nash equilibria, and subgame perfect equilibria : a formal and constructive equivalence

Stéphane Le Roux (1)

1 LIP - Laboratoire de l'Informatique du Parallélisme

Sequential game and Nash equilibrium are basic key concepts in gametheory. In 1953, Kuhn showed that every sequential game has a Nashequilibrium. The two main steps of the proof are as follows: First, aprocedure expecting a sequential game as an input is defined as "backwardinduction" in game theory. Second, it is proved that the procedureyields a Nash equilibrium. "Backward induction" actually yields Nashequilibria that define a proper subclass of Nash equilibria. In 1965, Seltennamed this proper subclass subgame perfect equilibria. In gametheory, payoffs are rewards usually granted at the end of a game. Althoughtraditional game theory mainly focuses on real-valued payoffsthat are implicitly ordered by the usual total order over the reals, thereis a demand for results dealing with non totally ordered payoffs. In themid 1950's, works of Simon or Blackwell already involved partially orderedpayoffs. This paper further explores the matter: it generalises thenotion of sequential game by replacing real-valued payoff functions withabstract atomic objects, called outcomes, and by replacing the usual totalorder over the reals with arbitrary binary relations over outcomes,called preferences. This introduces a general abstract formalism whereNash equilibrium, subgame perfect equilibrium, and "backward induction"can still be defined. Using a lemma on topological sorting, thispaper proves that the following three propositions are equivalent: 1)Preferences over the outcomes are acyclic. 2) Every sequential gamehas a Nash equilibrium. 3) Every sequential game has a subgame perfectequilibrium. The result is fully computer-certifued using the (highlyreliable) constructive proof assistant called Coq. Beside the additionalguarantee of correctness provided by the proof in Coq, the activity offormalisation also helps clearly identify the useful definitions and themain articulations of the proof.

Mots clés: Abstract sequential game; Constructivism; Induction; Nash equilibrium; Proof assistant; Subgame perfect equilibrium

Domaines: Informatique [cs]

Stéphane Le Roux. Acyclicity of preferences, Nash equilibria, and subgame perfect equilibria : a formal and constructive equivalence. [Research Report] LIP RR-2007-18, Laboratoire de l'informatique du parallélisme. 2007, 2+37p. ⟨hal-02102600⟩