Modified Bar Recursion

Ulrich Berger
Paulo B. Oliva

April 2002


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 $\mathcal{M}$ (the model of strongly majorizable functionals) and is not S1-S9 computable in $\mathcal{C}$ (the model of total functionals). Finally, we show that modified bar recursion defines Spector's bar recursion primitive recursively

Available as PostScript, PDF, DVI.


Last modified: 2003-06-08 by webmaster.