The semantic interpretation of the logical connectives and quantifiers as game constructors is well-known and goes back to Lorenzen in the late 50s. The game associated with a given formula consists of two players (Player and Opponent) arguing about the validity of the formula, so that whenever the formula is provable the Player has a winning strategy.

In my recent work on functional interpretations such as modified realizability and the dialectica interpretation I have come across two novel connections between game theory and proof theory, which I would like to discuss in this talk.

The first is an observation that a functional interpretation can be seen is a higher-order version of the Lorenzen games, where the game only has two rounds but the two players are allowed to choose higher-order functionals as moves. Such interpretation works not only for classical and intuitioinistic logic, but extends nicely to linear logic as well (where it coincides with de Paiva's dialectica categories).

The second connection with game theory comes from recent joint work with Martín Escardó on the computational interpretation of the countable and dependent choice. In there we found that the dialectica interpretation of dependent choice can also be viewed as a statement about existence of an optimal play in a way which generalises the notion of Nash equilibrium from the more traditional von Neumann Game Theory.

The aim of the talk will be to explain these two connections in detail.