The Journal of Symbolic Logic

Research Article

A Buchholz derivation system for the ordinal analysis of KP + Π3-reflection

Markus Michelbrink

Department of Computer Science, University of Wales Swansea, Singleton Park, Swansea, SA2 8PP, United Kingdom, E-mail:


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 + Π3-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 + Π3-Reflection as <-recursive functions where < is the ordering on Rathjen's ordinal notation system . Further we show a conservation result for -sentences.

(Received September 23 2005)

Key words and phrases

  • finitary proof theory;
  • ordinal analysis;
  • impredicative theories