BAR RECURSION AND PRODUCTS OF SELECTION FUNCTIONS

Abstract. We show how two iterated products of selection functions can both be used in conjunction with system T to interpret, via the dialectica interpretation and modified realizability, full classical analysis. We also show that one iterated product is equivalent over system T to Spector’s bar recursion, whereas the other is T-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 be T-equivalent to the iteration of the simple products. §1. Introduction. Gödel’s [13] so-called dialectica interpretation reduces the consis-tency of Peano arithmetic to the consistency of the quantifier-free calculus of function-als T. In order to extend Gödel’s interpretation to full classical analysis PAω + CA, Spector [18] made use of the fact that PAω + CA can be embedded, via the negative translation, into HAω +ACN +DNS. Here PAω and HAω denote Peano and Heytin