Proof Theory: The First Step into ImpredicativitySpringer Science & Business Media, 01.10.2008 - 374 Seiten The kernel of this book consists of a series of lectures on in?nitary proof theory which I gave during my time at the Westfalische ̈ Wilhelms–Universitat ̈ in Munster ̈ . It was planned as a successor of Springer Lecture Notes in Mathematics 1407. H- ever, when preparing it, I decided to also include material which has not been treated in SLN 1407. Since the appearance of SLN 1407 many innovations in the area of - dinal analysis have taken place. Just to mention those of them which are addressed in this book: Buchholz simpli?ed local predicativity by the invention of operator controlled derivations (cf. Chapter 9, Chapter 11); Weiermann detected applications of methods of impredicative proof theory to the characterization of the provable recursive functions of predicative theories (cf. Chapter 10); Beckmann improved Gentzen’s boundedness theorem (which appears as Stage Theorem (Theorem 6. 6. 1) in this book) to Theorem 6. 6. 9, a theorem which is very satisfying in itself - though its real importance lies in the ordinal analysis of systems, weaker than those treated here. Besides these innovations I also decided to include the analysis of the theory (? –REF) as an example of a subtheory of set theory whose ordinal analysis only 2 0 requires a ?rst step into impredicativity. The ordinal analysis of(? –FXP) of non- 0 1 0 monotone? –de?nable inductive de?nitions in Chapter 13 is an application of the 1 analysis of(? –REF). |
Inhalt
1 | |
9 | |
Ordinals | 17 |
Pure Logic | 43 |
Truth Complexity forΠ1 | 69 |
Inductive Definitions | 83 |
The Ordinal Analysis for PA | 105 |
Autonomous Ordinals and the Limits of Predicativity | 131 |
Ordinal Analysis of the Theory for Inductive Definitions | 157 |
Provably Recursive Functions of NT | 207 |
Ordinal Analysis for KripkePlatek Set Theory with Infinity 237 | 236 |
Predicativity Revisited | 297 |
Nonmonotone Inductive Definitions | 333 |
Epilogue 353 | 352 |
363 | |
Andere Ausgaben - Alle anzeigen
Häufige Begriffe und Wortgruppen
according already apply arithmetical assume atomic axiom calculus claim clauses closed complete computation consistency constructible contains Corollary CS(F define denote derivation entails Exercise fact finite set first-order formal formula foundation Hence hierarchy holds true immediately implies induction hypothesis inductive definition inference interpretation introduce iterated language least Lemma Lemma Let less logic Mathematical means natural numbers notation Observe obtain obvious occur operator ordinal analysis par(A predicative premise primitive recursive function Proof proof theory properties provable prove quantifiers relation replace rnk(F rule satisfying scheme second-order Sect semi-formal system sentences sequence set theory stage step structure symbol term Theorem tion transitive tree variables well-founded well-ordering