The Herbrand functional interpretation of the double negation shift

DOI10.1017/JSL.2017.8MaRDI QIDQ4977221zbMATH OpenOpenAlexFDO

Authors Martín Escardo, Paulo Oliva

Publication date 3 August 2017

Published in Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1410.4353

zbMATH Keywords

bar recursiondialectica interpretationHerbrand functional interpretationmonads

Mathematics Subject Classification ID

Structure of proofs (03F07) Functionals in proof theory (03F10) Second- and higher-order arithmetic and fragments (03F35)

Abstract: This paper considers a generalisation of selection functions over an arbitrary strong monad $T$, as functionals of type $J_R^{T}X=(XoR)oTX$. 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=(XoR)oR$. 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 power set monad $mathcalP(cdot)$. These are used to show that when $TX=mathcalP(X)$ the explicitly controlled product of $T$-selection functions calculates a witness to the Herbrand functional interpretation of the double negation shift.

Recommendations

• The bounded functional interpretation of the double negation shift
• Higher order functions and Brouwer's thesis
• On the Herbrand functional interpretation
• The Peirce translation and the double negation shift
• Bar recursion and products of selection functions

Cites work

• A functional interpretation for nonstandard arithmetic
• Bar recursion and products of selection functions
• Computational Interpretations of Analysis via Products of Selection Functions
• Effective bounds from ineffective proofs in analysis: An application of functional interpretation and majorization
• scientific article; zbMATH DE number 3231083 (Why is no real title available?)
• scientific article; zbMATH DE number 3335898 (Why is no real title available?)
• Inductive theorem proving based on tree grammars
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Modified bar recursion
• Notions of computation and monads
• On a generalization of quantifiers
• On Spector's bar recursion
• On the computational content of the axiom of choice
• Selection functions, bar recursion and backward induction
• Sequential games and optimal strategies
• Strong functors and monoidal monads
• Strongly majorizable functionals of finite type: A model for barrecursion containing discontinuous functionals
• The bounded functional interpretation of the double negation shift
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES

Cited in

(7)

• To be or not to be constructive, that is not the question
• The strength of countable saturation
• Backward induction for repeated games
• Higher-order games with dependent types
• Smart Choices and the Selection Monad
• What monads can and cannot do with a few extra pages
• Uniform functional interpretations

This page was built for publication: The Herbrand functional interpretation of the double negation shift

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4977221)