Advertisement
Published in:
2009 | OriginalPaper | Chapter
Acyclic Preferences and Existence of Sequential Nash Equilibria: A Formal and Constructive Equivalence
Author : Stéphane Le Roux
Published in: Theorem Proving in Higher Order Logics
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
In a game from game theory, a Nash equilibrium (NE) is a combination of one strategy per agent such that no agent can increase its payoff by unilaterally changing its strategy. Kuhn proved that all (tree-like) sequential games have NE. Osborne and Rubinstein abstracted over these games and Kuhn’s result: they proved a sufficient condition on agents’
preferences
for all games to have NE. This paper proves a
necessary and sufficient condition
, thus accounting for the game-theoretic frameworks that were left aside.
The proof is formalised
using Coq, and contrary to usual game theory it adopts an inductive approach to trees for definitions and proofs. By rephrasing a few game-theoretic concepts, by ignoring useless ones, and by characterising the proof-theoretic strength of Kuhn’s/Osborne and Rubinstein’s development, this paper also
clarifies
sequential game theory. The introduction sketches these clarifications, while the rest of the paper details the formalisation.