Bar recursion and products of selection functions

Martín Escardó, Paulo Oliva

Research output: Contribution to journalArticlepeer-review

11 Citations (Scopus)


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 languageEnglish
Pages (from-to)1-28
Number of pages28
JournalJournal of Symbolic Logic
Issue number01
Publication statusPublished - 1 Mar 2015


Dive into the research topics of 'Bar recursion and products of selection functions'. Together they form a unique fingerprint.

Cite this