The bounded functional interpretation of the double negation shift

We prove that the (non-intuitionistic) law of the double negation shift has a bounded functional interpretation with bar recursive functionals 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: Journal
• Year: 2010
• Where: JSYML
• Authors: Patrícia Engrácia, Fernando Ferreira
• Keywords: Bar Recursive Functionals, Double Negation Shift, Functional Interpretation, JSYML 2010