Modified Bar Recursion and Classical Dependent Choice
Ulrich Berger and Paulo Oliva

Abstract

We introduce a variant of Spector's bar recursion in finite types (which we call ``modified bar recursion'') to give a realizability interpretation of the classical axiom of dependent choice allowing for the extraction of witnesses from proofs of forall-exists-formulas in classical analysis. As another application, we show that the fan functional can be defined by modified bar recursion together with a version of bar recursion due to Kohlenbach. We also show that the type structure of strongly majorizable functionals is a model for modified bar recursion.

Bib entry

@InCollection{BergerOliva0x,
  author = 	 {Berger, U. and Oliva, P.},
  title = 	 "Modified Bar recursion and classical dependent 
                  choice",
  booktitle =	 "{L}ogic {C}olloquium 2001",
  publisher = "Springer",
  year =	 "to appear"
}

Draft copy: [pdf] [ps]