Closure of system T under the bar recursion rule
- Date: Wednesday 1 November 2017, 16:00 – 17:00
- Location: Mathematics Level 8, MALL 1, School of Mathematics
- Type: Logic, Seminars, Pure Mathematics
- Cost: Free
Paulo Oliva, Queen Mary University of London. Part of the logic seminar series.
Bar recursion (BR) is a form of recursive definition proposed by Spector  to extend system T so as to give a computational interpretation to proofs in classical analysis. It follows that T + BR is strictly more expressive than system T. Bar recursion can be viewed as form of recursion on well-founded trees. A celebrated result of Schwichtenberg  implies that if we restrict to T-definable trees, then BR of lowest type will not take us outside T-definability. This closure property is proven in  via a reduction to an infinitary version of system T, following by the use of ordinal recursion, and the translation of these back into system T. In  we have given a more direct proof, with an explicit construction that given a term in T + BR of restricted type, will convert that into a T term.
 Spector, C., Provably recursive functionals of analysis, Recursive Function Theory: Proc. Symposia in Pure Mathematics, 5, 127, 1962
 Schwichtenberg, H., On bar recursion of types 0 and 1, The Journal of Symbolic Logic, 44, 325329, 1979
 Oliva, P. and Steila, S., A direct proof of Schwichtenbergs bar recursion closure theorem, The Journal of Symbolic Logic, to appear.