THE HERBRAND FUNCTIONAL INTERPRETATION OF THE DOUBLE NEGATION SHIFT
From MaRDI portal
Publication:4977221
DOI10.1017/jsl.2017.8zbMath1419.03051arXiv1410.4353OpenAlexW2963708890MaRDI QIDQ4977221
Martín Hötzel Escardó, Paulo Oliva
Publication date: 3 August 2017
Published in: The Journal of Symbolic Logic (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1410.4353
Structure of proofs (03F07) Functionals in proof theory (03F10) Second- and higher-order arithmetic and fragments (03F35)
Related Items
The strength of countable saturation, Higher-order games with dependent types, To be or not to be constructive, that is not the question, Smart Choices and the Selection Monad, Unnamed Item
Cites Work
- Unnamed Item
- Unnamed Item
- A functional interpretation for nonstandard arithmetic
- Notions of computation and monads
- Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
- Inductive theorem proving based on tree grammars
- Strong functors and monoidal monads
- On Spector's bar recursion
- Sequential games and optimal strategies
- On a generalization of quantifiers
- ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
- Selection functions, bar recursion and backward induction
- The bounded functional interpretation of the double negation shift
- Computational Interpretations of Analysis via Products of Selection Functions
- Strongly majorizable functionals of finite type: A model for barrecursion containing discontinuous functionals
- Effective bounds from ineffective proofs in analysis: An application of functional interpretation and majorization
- On the computational content of the axiom of choice
- BAR RECURSION AND PRODUCTS OF SELECTION FUNCTIONS
- Modified bar recursion
