17 July 2007

Talk by Stéphane le Roux

Acyclicity of preferences, Nash equilibria, and Subgame perfect equilibria: two Proofs of the Equivalence

Stéphane le Roux

Sequential game and Nash equilibrium are basic key concepts in game theory. In 1953, Kuhn showed that every sequential game has a Nash equilibrium. Traditionally, sequential games involve real-valued payoff functions. I replace them with abstract atomic objects and generalise Kuhn’s result to such an extent that I get an equivalence property. I provide two proofs very different from a proof theoretic viewpoint. I have fully formalised the first proof using Coq. In the end of the talk, I may describe the Coq formalism representing the core concepts of this development.

July 17th, 2007.