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.
Discrete Mathematics & Theoretical Computer Science