Computational Logic SeminarTuesday, March 19, 20132:00 pmGraduate Center, room 3209
Computing Bounds from Arithmetical Proofs
Stan Wainer
The Leeds Logic Group, University of Leeds
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.
Posted by
on March 15th, 2013