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 
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 
(the model of strongly majorizable
functionals) and is not S1-S9 computable in 
(the model of total
functionals). Finally, we show that modified bar recursion defines Spector's
bar recursion primitive recursively
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 (the model of strongly majorizable
functionals) and is not S1-S9 computable in (the model of total
functionals). Finally, we show that modified bar recursion defines Spector's
bar recursion primitive recursivelyAvailable as PostScript, PDF, DVI.