Proof-theoretic analysis of KPM
The aim of this paper is the ordinal analysis of the formal system KPM of a Kripke-Platek set theory which describes the properties of the collection \(L_{\mu}\) of constructible sets of order \(<\mu\) axiomatically, where \(\mu\) is the first recursive Mahlo ordinal. Ordinal analysis of a theory T means determining the proof-theoretical ordinal \(| T|\) of the theory. In this case the following definition suggests \(itself:\) \(| T|:=\inf \{\alpha |\) for all \(\Sigma\)-sentences of \({\mathcal L}(T\vdash B^{{\mathcal A}}\Rightarrow L_{\alpha}\vDash B)\}\), \({\mathcal L}\) being the language of set theory, \({\mathcal A}\) a constant for \(L_{\omega_ 1^{CK}}\), \(\omega_ 1^{CK}\) the least nonrecursive ordinal, and \(B^{{\mathcal A}}\) the formula which results from B by restricting all occurring unrestricted quantifiers to \({\mathcal A}\). This definition of \(| T|\) is equivalent to the usual \(one:\) \(| T|:=\sup \{| \prec |:\) \(T\vdash ``\prec\) is a primitive recursive well-ordering of \(\prec \}\), where \(| \prec |\) is the order type of \(\prec.\) The ordinal analysis is carried out by performing cut-elimination. Since KPM is not closed with respect to the cut-elimination operation, a system RS(M) of a ramified set theory is introduced with infinite derivations, in which KPM is embedded. For the ordinal analysis of RS(M) the method of local predicativity is applied. The ordinals used were introduced by the author in an earlier paper. He repeats the definition, thus the exposition here is self-contained.
- A new system of proof-theoretic ordinal functions
- scientific article; zbMATH DE number 4039890 (Why is no real title available?)
- scientific article; zbMATH DE number 4079410 (Why is no real title available?)
- scientific article; zbMATH DE number 193575 (Why is no real title available?)
- scientific article; zbMATH DE number 3494394 (Why is no real title available?)
- scientific article; zbMATH DE number 3572133 (Why is no real title available?)
- Nichtbeweisbarkeit von gewissen kombinatorischen Eigenschaften endlicher Bäume;Unprovability of certain combinatorial properties of finite trees
- Ordinal notations based on a hierarchy of inaccessible cardinals
- Ordinal notations based on a weakly Mahlo cardinal
- Proof theory and ordinal analysis
- Proof theory. An introduction
- ϱ-inaccessible ordinals, collapsing functions and a recursive notation system
- Inaccessibility in constructive set theory and type theory
- A uniform approach for characterizing the provably total number-theoretic functions of KPM and (some of) its subsystems
- Collapsing functions based on recursively large ordinals: A well-ordering proof for KPM
- Proof theory of reflection
- The strength of some Martin-Löf type theories
- Proof theory for theories of ordinals. I: Recursively Mahlo ordinals
- Induction-recursion and initial algebras.
- Functional interpretation of Aczel's constructive set theory
- Reduction of finite and infinite derivations
- Epsilon substitution for \(ID_1\) via cut-elimination
- An ordinal analysis of stability
- Realization of constructive set theory into explicit mathematics: A lower bound for impredicative Mahlo universe
- Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 8--14, 2020 (hybrid meeting)
- Proof theory and ordinal analysis
- Primitive recursive analogues of regular cardinals based on ordinal representation systems for KPi and KPM
- Theories and ordinals in proof theory
- Notes on some second-order systems of iterated inductive definitions and \(\Pi_1^1\)-comprehensions and relevant subsystems of set theory
- Relativized ordinal analysis: the case of power Kripke-Platek set theory
- 1998 European Summer Meeting of the Association for Symbolic Logic
- scientific article; zbMATH DE number 510775 (Why is no real title available?)
- Wellordering proofs for metapredicative Mahlo
- AN ORDINAL ANALYSIS OF ADMISSIBLE SET THEORY USING RECURSION ON ORDINAL NOTATIONS
- Recent Advances in Ordinal Analysis: Π12— CA and Related Systems
- How to characterize provably total functions by local predicativity
- Monotone inductive definitions in explicit mathematics
- scientific article; zbMATH DE number 888989 (Why is no real title available?)
- Pure Proof Theory Aims, Methods and Results: Extended Version of Talks Given at Oberwolfach and Haifa
- scientific article; zbMATH DE number 1390277 (Why is no real title available?)
- An Upper Bound for the Proof-Theoretic Strength of Martin-Löf Type Theory with W-type and One Universe
- Zur Beweistheorie Von KPM
- Zur Beweistheorie von KP+ $$ \varPi_{3} $$-Ref
- Simplified Cut Elimination for Kripke-Platek Set Theory
- Well-Ordering Principles in Proof Theory and Reverse Mathematics
- Proof theory of constructive systems: inductive types and univalence
- Extending the system T\(_0\) of explicit mathematics: The limit and Mahlo axioms
- Simplified collapsing functions and their applications
- The constructive Hilbert program and the limits of Martin-Löf type theory
- Verificaton, falsification, and cancellation in KT
- Ordinal notations based on a weakly Mahlo cardinal
This page was built for publication: Proof-theoretic analysis of KPM
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q803124)
