Modified Bar Recursion

Abstract

We introduce a variant of Spector's bar recursion (called "modified bar recursion'') in finite types to give a realizability interpretation of the classical axiom of countable choice allowing for the extraction of witnesses from proofs of Sigma_1 formulas in classical analysis. As a second application of modified bar recursion we present a bar recursive definition of the fan functional. Moreover, we show that modified bar recursion exists in M (the model of strongly majorizable functionals) and is not S1-S9 computable in C (the model of total functionals). Finally, we show that modified bar recursion defines Spector's bar recursion primitive recursively.