1 Department of Computer Science, Faculty of Science, Aarhus University, Aarhus University2 Department of Computer Science, Queen Mary, University of London
We introduce a variant of Spector's Bar Recursion in finite types to give a realizability interpretation of the classical axiom of dependent choice allowing for the extraction of witnesses from proofs of Sigma_1 formulas in classical analysis. We also give a bar recursive definition of the fan functional and study the relationship of our variant of Bar Recursion with others.
Bounded Arithmetic and Complexity Classes. Bacc'02. Proceedings: Meeting on Bounded Arithmetic and Complexity Classes, 2002
Main Research Area:
BACC '02, Meeting on bounded arithmetic and complexity classes, 2002