Functional interpretations, linear logic and games
Paulo Oliva ( Department of Computer Science, Queen Mary University of London )
- 14:00 7th November 2008 ( week 4, Michaelmas Term 2008 )Lecture Theater B
In this talk I will describe how functional interpretations, such as Kreisel's modified realizability and Goedel's Dialectica interpretation, allow us to view mathematical statements as one-move two-player games. Intuitively, one player tries to prove the statement, while the other looks for counterexamples. I will argue that in constructive mathematics the games can be such that one of the players has an advantage, i.e. games are not symmetric. In the case of mathematics based on linear logic, however, the games are naturally symmetric, and players must choose their moves simultaneously. The goal has been to unify different functional interpretations into a single framework, which has recently led to a hybrid interpretation. I will also describe some concrete examples of how functional interpretations (via proof mining) have been successfully applied to current mathematics.
Share this:
