In this paper we introduce a notation system for the infinitary
derivations occurring in the ordinal analysis of
KP+Π_3-Reflection due to Michael Rathjen. This allows a
finitary ordinal analysis of
KP+Π₃-Reflection. The method used is an
extension of techniques developed by Wilfried Buchholz, namely
operator controlled notation systems for
RS∞-derivations. Similarly to Buchholz we obtain a
characterisation of the provably recursive functions of
KP+Π₃-Reflection as <-recursive
functions where < is the ordering on Rathjen’s
ordinal notation system 𝒯(K). Further we show a conservation
result for Π⁰₂-sentences.
@article{1164060454,
author = {Michelbrink, Markus},
title = {A Buchholz derivation system for the ordinal analysis of KP+P3-reflection},
journal = {J. Symbolic Logic},
volume = {71},
number = {1},
year = {2006},
pages = { 1237-1283},
language = {en},
url = {http://dml.mathdoc.fr/item/1164060454}
}
Michelbrink, Markus. A Buchholz derivation system for the ordinal analysis of KP+Π₃-reflection. J. Symbolic Logic, Tome 71 (2006) no. 1, pp. 1237-1283. http://gdmltest.u-ga.fr/item/1164060454/