INTERRELATION BETWEEN WEAK FRAGMENTS OF DOUBLE NEGATION SHIFT AND RELATED PRINCIPLES

We investigate two weak fragments of the double negation shift schema, which are motivated, respectively, from Spector’s consistency proof of ACA0 and from the negative translation of RCA0, as well as double negated variants of logical principles. Their interrelations over both intuitionistic arithmetic and analysis are completely solved.

THE HERBRAND FUNCTIONAL INTERPRETATION OF THE DOUBLE NEGATION SHIFT

This paper considers a generalisation of selection functions over an arbitrary strong monad T, as functionals of type $J_R^T X = (X \to R) \to TX$. 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 = (X \to R) \to R$. 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 powerset monad ${\cal P}_{\rm{f}} \left( \cdot \right)$. These are used to show that when $TX = {\cal P}_{\rm{f}} \left( X \right)$ the explicitly controlled product of T-selection functions calculates a witness to the Herbrand functional interpretation of the double negation shift.

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 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.