The bounded functional interpretation of the double negation shift
Patrícia Engrácia, Fernando A.F. Ferreira · Journal of Symbolic Logic · 2010
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.