Premium
On Spector's bar recursion
Author(s) -
Oliva Paulo,
Powell Thomas
Publication year - 2012
Publication title -
mathematical logic quarterly
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.473
H-Index - 28
eISSN - 1521-3870
pISSN - 0942-5616
DOI - 10.1002/malq.201100106
Subject(s) - recursion (computer science) , iterated function , mathematics , bar (unit) , product (mathematics) , function (biology) , selection (genetic algorithm) , computer science , algorithm , geometry , mathematical analysis , artificial intelligence , physics , evolutionary biology , meteorology , biology
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.