Back to Search
Start Over
THE HERBRAND FUNCTIONAL INTERPRETATION OF THE DOUBLE NEGATION SHIFT.
- Source :
- Journal of Symbolic Logic; Jun2017, Vol. 82 Issue 2, p590-607, 18p
- Publication Year :
- 2017
-
Abstract
- This paper considers a generalisation of selection functions over an arbitrary strong monad T, as functionals of type $J_R^T X = (X \to R) \to TX$. It is assumed throughout that R is a T-algebra. We show that $J_R^T$ is also a strong monad, and that it embeds into the continuation monad $K_R X = (X \to R) \to 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 ${\cal P}_{\rm{f}} \left( \cdot \right)$. These are used to show that when $TX = {\cal P}_{\rm{f}} \left( X \right)$ the explicitly controlled product of T-selection functions calculates a witness to the Herbrand functional interpretation of the double negation shift. [ABSTRACT FROM AUTHOR]
Details
- Language :
- English
- ISSN :
- 00224812
- Volume :
- 82
- Issue :
- 2
- Database :
- Supplemental Index
- Journal :
- Journal of Symbolic Logic
- Publication Type :
- Academic Journal
- Accession number :
- 123684472
- Full Text :
- https://doi.org/10.1017/jsl.2017.8