Computing Bounds from Arithmetical Proofs

Computational Logic SeminarTuesday, March 19, 20132:00 pmGraduate Center, room 3209

Stan Wainer

Computing Bounds from Arithmetical Proofs

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