##
Games and Logic

### Paulo Oliva

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 intuitionistic 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Ã³
(and recently Thomas Powell) 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.