Article contents
The bounded functional interpretation of the double negation shift
Published online by Cambridge University Press: 12 March 2014
Abstract
We prove that the (non-intuitionistic) law of the double negation shift has a bounded functional interpretation with bar recursive functional of finite type. As an application, we show that full numerical comprehension is compatible with the uniformities introduced by the characteristic principles of the bounded functional interpretation for the classical case.
- Type
- Research Article
- Information
- Copyright
- Copyright © Association for Symbolic Logic 2010
References
REFERENCES
- 2
- Cited by