Por Paulo Oliva (Queen Mary, University of London).

Abstract: Functional interpretations such as Gödel’s Dialectica or Kreisel’s modified realizability work by translating logical dependencies into functional dependencies. This means that even if one starts with a purely arithmetical formula A, its interpretation will involve functionals of arbitrary type level, depending on the complexity of the logical dependencies in A. When the interpreted formula already contains quantification over functions or functionals, one has a choice on how to interpret these quantifications. In this talk we review the current approaches, the problems they face (e.g. not validating the extensionality axiom), and propose a new way of interpreting such quantifications.