Proofs, Programs and Abstract Complexity

Programs and Abstract Complexity A. Beckmann University of Wales Swansea Swansea, UK Axiom systems are ubiquitous in mathematical logic, one famous and well studied example being first order Peano arithmetic. Foundational questions asked about axiom systems comprise analysing their provable consequences, describing their class of provable recursive functions (i.e. for which programs can termination be proven from the axioms), and characterising their consistency strength. One branch of proof theory, called ordinal analysis, has been quite successful in giving answers to such questions, often providing a unifying approach to them. The main aim of ordinal analysis is to reduce such questions omputation of so called proof theoretic ordinals, which can be viewed as abstract measures of the complexity inherent in axiom systems. Gentzen’s famous consistency proof of arithmetic using transfinite induction up to (a notation of) Cantor’s ordinal 0, can be viewed as the first computation ...

• Type: Conference
• Year: 2007
• Where: CSL
• Authors: Arnold Beckmann
• Keywords: Axiom Systems, CSL 2007, Peano Arithmetic, Proof Theoretic Ordinals