Modified bar recursion

Modified bar recursion has been used to give a realizability interpretation of the classical axioms of countable and dependent choice. In this paper we survey the main results concerning this scheme of bar recursion and its relations to well-known functionals. In particular we show that Spector's bar recursion can be defined primitive recursively via the scheme of modified bar recursion, but not the other way around. Key words: 1991 MSC:

• Type: Journal
• Year: 2006
• Where: MSCS
• Authors: Ulrich Berger, Paulo Oliva
• Keywords: Bar Recursion, Classical Axioms, MSCS 2006, Realizability Interpretation