BAR RECURSION AND PRODUCTS OF SELECTION FUNCTIONS
Martı́n Hötzel Escardó, Paulo B. Oliva · Journal of Symbolic Logic · 2015
Abstract We show how two iterated products of selection functions can both be used in conjunction with systemTto interpret, via the dialectica interpretation and modified realizability, full classical analysis. We also show that one iterated product is equivalent over systemTto Spector’s bar recursion, whereas the other isT-equivalent to modified bar recursion. Modified bar recursion itself is shown to arise directly from the iteration of a different binary product of ‘skewed’ selection functions. Iterations of the dependent binary products are also considered but in all cases are shown to beT-equivalent to the iteration of the simple products.