Abstract
This paper considers a generalisation of selection functions over an arbitrary strong monad T, as functionals of type JRTX =(X → R)→ TX . It is assumed throughout that R is a T-algebra. We show that JRT is also a strong monad, and that it embeds into the continuation monad KRX =(X → R)→ R. We use this to derive that the explicitly controlled product of T-selection functions is definable from the explicitly controlled product of quantifiers, and hence from Spector's bar recursion. We then prove several properties of this product in the special case when T is the finite powerset monad Pf(·). These are used to show that when TX = Pf (X) the explicitly controlled product of T-selection functions calculates a witness to the Herbrand functional interpretation of the double negation shift.
Original language | English |
---|---|
Pages (from-to) | 590-607 |
Number of pages | 18 |
Journal | Journal of Symbolic Logic |
Volume | 82 |
Issue number | 2 |
DOIs | |
Publication status | Published - 1 Jun 2017 |
Bibliographical note
Publisher Copyright:© 2017 The Association for Symbolic Logic.
Keywords
- Bar recursion
- Dialectica interpretation
- Herbrand functional interpretation
- Monads
ASJC Scopus subject areas
- Philosophy
- Logic