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