Modified Bar Recursion Ulrich Berger Paulo B. Oliva April 2002

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

Available as PostScript, PDF, DVI.