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.