Bar recursive extensions of Goedel's system T

Thomas Powell

(Institut des Hautes √Čtudes Scientifiques)

Extensions of Goedel's system T with variants of bar recursion play a crucial role in proof theory, where they are used to give a computational interpretation to strong subsystems of mathematics based on the axiom of countable choice. The canonical example of this is Spector's bar recursion, devised in the 1960s to solve the Dialectica interpretation of the double negation shift. However, the last decade or so has seen the development of a much broader variety of such extensions, including modified bar recursion, the symmetric `demand-driven' functional of Berardi, Bezem and Coquand, the update and open recursors of Berger and more recently the products of selection functions of Escardo and Oliva. In this talk I discuss aspects of the computability theory of bar recursion and its variants, and in particular I give an account of recent work on establishing the relationship between these variants and classifying extensions of system T according to primitive recursive definability.
Wednesday 18th December 2013, 11:00
Board Room (314)
Department of Computer Science