On Spector's bar recursion

Paulo Oliva, Thomas Powell

Research output: Contribution to journalArticlepeer-review

11 Citations (SciVal)


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
Issue number4-5
Publication statusPublished - 2012


Dive into the research topics of 'On Spector's bar recursion'. Together they form a unique fingerprint.

Cite this