On Spector's bar recursion (Q2910991)

Bar recursion, introduced by \textit{C. Spector} [Proc. Sympos. Pure Math. 5, 1--27 (1962; Zbl 0143.25502)], is a generalized form of recursion. It is the computational analogue of the well-known principle of bar induction, in the same sense as primitive recursion is related with the logical principle of induction.NEWLINENEWLINEIn fact, Spector describes in [loc. cit.] two forms of bar recursion: general bar recursion (inspired in the above analogy with bar induction) and restricted bar recursion (enough to construct a Dialectica realizer for the double negation shift).NEWLINENEWLINEOne may be led to think that restricted bar recursion (rBR) is strictly weaker than general bar recursion (gBR). In the present paper, the authors show that this is not the case. They prove that the restricted and the general forms of bar recursion are inter-definable over system T.NEWLINENEWLINEIt is easy to see that rBR follows from gBR over Gödel's T (see also [\textit{U. Kohlenbach}, Applied proof theory. Proof interpretations and their use in mathematics. Berlin: Springer (2008; Zbl 1158.03002); \textit{H. Luckhardt}, Extensional Gödel functional interpretation. A consistency proof of classical analysis. Lect. Notes Math. 306. Berlin-Heidelberg-NewYork: Springer-Verlag (1973; Zbl 0262.02031)]). The main contribution of the paper lies in proving that rBR is in fact as general as gBR. It is accomplished by constructing a term in T + rBR which satisfies (provably in T + rBR) the equation for gBR.NEWLINENEWLINESince these two forms of bar recursion correspond (see [\textit{M. Escardó} and \textit{P. Oliva}, Lect. Notes Comput. Sci. 6158, 141--150 (2010; Zbl 1251.03073)]) to the (explicitly controlled) iterated products of selection functions and quantifiers, we can conclude that this iterated product of selection functions is T-equivalent to the corresponding iterated product of quantifiers.