Book contents
- Frontmatter
- Contents
- Preface
- Programme of lectures
- Basic proof theory
- A short course in ordinal analysis
- Proofs as Programs
- A simplified version of local predicativity
- A note on bootstrapping intuitionistic bounded arithmetic
- Termination orderings and complexity characterisations
- Logics for termination and correctness of functional programs, II. Logics of strength PRA
- Reflecting the semantics of reflected proof
- Fragments of Kripke-Platek set theory with infinity
- Provable computable selection functions on abstract structures
A simplified version of local predicativity
Published online by Cambridge University Press: 05 November 2011
- Frontmatter
- Contents
- Preface
- Programme of lectures
- Basic proof theory
- A short course in ordinal analysis
- Proofs as Programs
- A simplified version of local predicativity
- A note on bootstrapping intuitionistic bounded arithmetic
- Termination orderings and complexity characterisations
- Logics for termination and correctness of functional programs, II. Logics of strength PRA
- Reflecting the semantics of reflected proof
- Fragments of Kripke-Platek set theory with infinity
- Provable computable selection functions on abstract structures
Summary
The method of local predicativity as developed by Pohlers in [10],[11],[12] and extended to subsystems of set theory by Jäger in [4],[5],[6] is a very powerful tool for the ordinal analysis of strong impredicative theories. But up to now it suffers considerably from the fact that it is based on a large amount of very special ordinal theoretic prerequisites. This is true even for the most recent (very polished) presentation of local predicativity in (Pohlers [15]). The purpose of the present paper is to expose a simplified and conceptually improved version of local predicativity which – besides some very elementary facts on ordinal addition, multiplication, and exponentiation – requires only amazingly little ordinal theory. (All necessary nonelementary ordinal theoretic prerequisites can be developed from scratch on just two pages, as we will show in section 4.) The most important feature of our new approach however seems to be its conceptual clarity and flexibility, and in particular the fact that its basic concepts (i.e. the infinitary system RS∞ and the notion of an H-controlled RS∞-derivation) are in no way related to any system of ordinal notations or collapsing functions. Our intention with this paper is to make the fascinating field of ‘admissible proof theory’ (created by Jäger and Pohlers) more easily accessible for non-proof-theorists, and to provide a technically and conceptually well developed basis for further research in this area.
- Type
- Chapter
- Information
- Proof TheoryA selection of papers from the Leeds Proof Theory Programme 1990, pp. 115 - 148Publisher: Cambridge University PressPrint publication year: 1993
- 26
- Cited by