Abstract

The Curry-Howard correspondence, realizability and Gödel’s functional interpretations are all examples of how one can capture or interpret logical dependence through functional dependence. In an intuitionistic setting this correspondence might not seem so surprising since an intuitionistic logical dependence is normally defined through functional one. This becomes much more subtle when one moves to classical logic, arithmetic, and analysis, where proofs by contradiction combined that use induction or choice principles can have unexpected higher-order functional interpretations [1,2]. More recently we have been applying such techniques developed in for the proof theory of classical analysis into the field of strategic game theory [3,4]. This talk aims to explain the basic techniques and concepts, and how they have been applied to improve the modelling of multi-player strategic games.

[1] Paulo Oliva and Thomas Powell, A constructive interpretation of Ramsey’s theorem via the product of selection functions, Mathematical Structures in Computer Science, 24 pages, 2014

[2] Martín Escardó and Paulo Oliva, Bar recursion and products of selection functions, The Journal of Symbolic Logic, 80(1):1-28, 2015

[3] Jules Hedges, Paulo Oliva, Evguenia Winschel, Viktor Winschel and Philipp Zahn, Higher-order decision theory, Submitted for publication (see ArXiv), 2015

[4] Jules Hedges, Paulo Oliva, Evguenia Winschel, Viktor Winschel and Philipp Zahn, Representing strategic games with higher-order functions, Submitted for publication (see ArXiv), 2015