Proof-theoretic analysis of KPM (Q803124)

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.