Non-Determinism and Nash Equilibria for Sequential Game over Partial Order

Abstract

In sequential games of traditional game theory, backward induction guarantees existence of Nash equilibrium by yielding a sub-game perfect equilibrium. But if payoffs range over a partially ordered set instead of the reals, then the backward induction predicate does no longer imply the Nash equilibrium predicate. Non-determinism is a solution: a suitable non-deterministic backward induction function returns a non-deterministic strategy profile which is a non-deterministic Nash equilibrium. The main notions and results in this article are constructive, conceptually simple and formalised in the proof assistant Coq.

Keywords

• partial order
• non-determinism
• sequential game
• nash equilibrium
• constructive
• proof assistant
• [info.info-lo] computer science [cs]/logic in computer science [cs.lo]
• [info.info-sc] computer science [cs]/symbolic computation [cs.sc]