Understanding and using Spector’s bar recursive interpretation of classical analysis

Abstract. This note reexamines Spector’s remarkable computational interpretation of full classical analysis. Spector’s interpretation makes use of a rather abstruse recursion schema, so-called bar recursion, used to interpret the double negation shift DNS. In this note bar recursion is presented as a generalisation of a simpler primitive recursive func-tional needed for the interpretation of a finite (intuitionistic) version of DNS. I will also present two concrete applications of bar recursion in the extraction of programs from proofs of ∀∃-theorems in classical analysis.