A simplified version of local predicativity
Wilfried Buchholz · Cambridge University Press eBooks · 1993
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.