Bar recursion and products of selection functions

Research output: Contribution to journalArticle

Authors

Colleges, School and Institutes

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.

Details

Original languageEnglish
Pages (from-to)1-28
Number of pages28
JournalJournal of Symbolic Logic
Volume80
Issue number01
Publication statusPublished - 1 Mar 2015