Skip to Main content Skip to Navigation

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

Abstract : 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.
Document type :
Complete list of metadatas

Cited literature [20 references]  Display  Hide  Download
Contributor : Colette Orange <>
Submitted on : Wednesday, April 17, 2019 - 3:02:46 PM
Last modification on : Wednesday, November 20, 2019 - 2:52:59 AM


Files produced by the author(s)


  • HAL Id : hal-02102600, version 1



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⟩



Record views


Files downloads