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 (30)

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

This page was built for publication: Proof-theoretic analysis of KPM