On Spector's bar recursion

Paulo Oliva, Thomas Powell

Research output: Contribution to journalArticle

10 Citations (Scopus)

Abstract

We show that Spector's “restricted” form of bar recursion is sufficient (over system T) to define Spector's search functional. This new result is then used to show that Spector's restricted form of bar recursion is in fact as general as the supposedly more general form of bar recursion. Given that these two forms of bar recursion correspond to the (explicitly controlled) iterated products of selection function and quantifiers, it follows that this iterated product of selection functions is T‐equivalent to the corresponding iterated product of quantifiers.
Original languageEnglish
Pages (from-to)356-265
JournalMathematical Logic Quarterly
Volume58
Issue number4-5
DOIs
Publication statusPublished - 2012

Cite this