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.
Original language | English |
---|---|
Pages (from-to) | 1-28 |
Number of pages | 28 |
Journal | Journal of Symbolic Logic |
Volume | 80 |
Issue number | 01 |
DOIs | |
Publication status | Published - 1 Mar 2015 |