ABSTRACT
Contemporary ordinal-theoretic proof theory (i.e., the part of proof theory concerned with ordinal analysises of strong impredicative theories) suffers from the extreme (and as it seems unavoidable) complexity and opacity of its main tool, the ordinal notation systems. This is not only a technical stumbling block which prevents most proof-theorists from a closer engagement in that field, but it also calls the achieved results into question, at least as long as these results do not have interesting consequences, such as e.g., foundational reductions or intuitively graspable combinatorial independence results. The question is, what have we gained by having shown that the proof-theoretic ordinal of a certain formal theory S equals the ordertype || -< || of some specific term ordering -< (disregarding for the moment possible applications of the abovementioned kind). I would say, as long as the ordering is simple and natural (as e.g., the standard orderings of order type £o or To) or occurs already elsewhere in mathematics or theoretical computer science, we have obtained a result of pure mathematics which is interesting and noteworthy by itself. But I’m not sure if the latter can (already) be said about Rathjen’s ([18]) and Arai’s ([3], [2]) most impressive and admirable work on E^-CA and beyond. Rather I think, that extensive efforts should be made aiming at a substantial simplification and deeper understanding of that work, especially of the used ordinal notation systems (term orderings, resp.).
