University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > Logical dependence via functional dependence

Logical dependence via functional dependence

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Dominic Mulligan.

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

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2020 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity