A generalisation of Nash's theorem with higher-order functionals

TL;DR

This paper extends Nash's theorem to a broader class of simultaneous move games using higher-order functionals, generalizing classical game theory concepts with connections to proof theory.

Contribution

It introduces a normal form construction for these generalized games and proves its soundness, linking game theory with higher-order functionals and proof-theoretic interpretations.

Findings

Generalization of Nash's theorem to selection function-based games

Normal form construction for the new class of games

Minimax strategies computed via the Berardi-Bezem-Coquand functional

Abstract

The recent theory of sequential games and selection functions by Mar- tin Escardo and Paulo Oliva is extended to games in which players move simultaneously. The Nash existence theorem for mixed-strategy equilibria of finite games is generalised to games defined by selection functions. A normal form construction is given which generalises the game-theoretic normal form, and its soundness is proven. Minimax strategies also gener- alise to the new class of games and are computed by the Berardi-Bezem- Coquand functional, studied in proof theory as an interpretation of the axiom of countable choice.