Proof-theoretic analysis of KPM

DOI10.1007/BF01621475zbMath0727.03036OpenAlexW2064023341MaRDI QIDQ803124

Michael Rathjen

Publication date: 1991

Published in: Archive for Mathematical Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf01621475

zbMATH Keywords

cut-eliminationconstructible setsproof-theoretical ordinalfirst recursive Mahlo ordinallocal predicativityordinal analysis of the formal system KPM of a Kripke-Platek set theoryramified set theory

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Recursive ordinals and ordinal notations (03F15)

Related Items

1998 European Summer Meeting of the Association for Symbolic Logic, Proof theory of reflection, Wellordering proofs for metapredicative Mahlo, The strength of some Martin-Löf type theories, Well-Ordering Principles in Proof Theory and Reverse Mathematics, Primitive recursive analogues of regular cardinals based on ordinal representation systems for KPi and KPM, Epsilon substitution for \(ID_1\) via cut-elimination, Relativized ordinal analysis: the case of power Kripke-Platek set theory, Proof theory for theories of ordinals. I: Recursively Mahlo ordinals, Induction-recursion and initial algebras., Recent Advances in Ordinal Analysis: Π¹₂— CA and Related Systems, How to characterize provably total functions by local predicativity, Monotone inductive definitions in explicit mathematics, Pure Proof Theory Aims, Methods and Results: Extended Version of Talks Given at Oberwolfach and Haifa, Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 8--14, 2020 (hybrid meeting), Simplified collapsing functions and their applications, An ordinal analysis of stability, Theories and ordinals in proof theory, Proof theory and ordinal analysis, Extending the system T\(_0\) of explicit mathematics: The limit and Mahlo axioms, Notes on some second-order systems of iterated inductive definitions and \(\Pi_1^1\)-comprehensions and relevant subsystems of set theory, Proof Theory of Constructive Systems: Inductive Types and Univalence, Functional interpretation of Aczel's constructive set theory, Reduction of finite and infinite derivations, Inaccessibility in constructive set theory and type theory, An Upper Bound for the Proof-Theoretic Strength of Martin-Löf Type Theory with W-type and One Universe, Zur Beweistheorie Von KPM, Realization of constructive set theory into explicit mathematics: A lower bound for impredicative Mahlo universe, The constructive Hilbert program and the limits of Martin-Löf type theory, Collapsing functions based on recursively large ordinals: A well-ordering proof for KPM

Cites Work

• Ordinal notations based on a weakly Mahlo cardinal
• A new system of proof-theoretic ordinal functions
• Ordinal notations based on a hierarchy of inaccessible cardinals
• Proof theory. An introduction
• Proof theory and ordinal analysis
• ϱ-inaccessible ordinals, collapsing functions and a recursive notation system
• Nichtbeweisbarkeit von gewissen kombinatorischen Eigenschaften endlicher Bäume;Unprovability of certain combinatorial properties of finite trees
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item