Thursday, 3 February 2011, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B101
Abstract: Bar recursion (Spector, 1962) is a principle of definition by recursion on well-founded trees. These trees are implicitly defined by a parameter, a second-order aspect from which bar recursion derives much of its proof-theoretic strength. Technically, bar recursion is an extension of Gödel's system T of primitive recursive functionals. We briefly discuss the semantics of bar recursion, in particular models based on continuity and majorizability. (The full set-theoretic model of T is not a model of bar recursion.) Finally, we sketch normalization proofs for bar recursion. The material of this talk can be found in Chapter 5D of the forthcoming book Lambda Calculus with Types by Barendregt, Dekkers and Statman (eds.).