How to develop Proof‐Theoretic Ordinal Functions on the basis of admissible ordinals
Michael Rathjen · Mathematical logic quarterly · 1993
Abstract In ordinal analysis of impredicative theories so‐called collapsing functions are of central importance. Unfortunately, the definition procedure of these functions makes essential use of uncountable cardinals whereas the notation system that they call into being corresponds to a recursive ordinal. It has long been claimed that, instead, one should manage to develop such functions directly on the basis of admissible ordinals. This paper is meant to show how this can be done. Interpreting the collapsing functions as operating directly on admissible sets also renders a new and perspicuous approach to well‐ordering proofs possible. MSC: 03F15, 03F35.