Speaker: Stan Weiner, University of Leeds
Title: Computing Bounds from Arithmetical Proofs.
Abstract: We explore the role of the function $a+2^x$, and its generalizations to higher number classes, in analyzing and measuring the computational content of a broad spectrum of arithmetical theories. Newer formalizations of such theories, based on the well-known normal/safe variable separation of Bellantoni-Cook, enable uniform proof-theoretical treatments of poly-time arithmetics, through Peano arithmetic, and up to finitely iterated inductive definitions.
Reference: Schwichtenberg and Wainer, “Proofs and Computations”, ASL Perspectives in Logic, CUP 2012.