Taking up ordinal notations derived from Skolem hull operators familiar in the field of infinitary proof theory we develop a toolkit of ordinal arithmetic that generally applies whenever ordinal structures are analyzed whose combinatorial complexity does not exceed the strength of the system of set theory. The original purpose of doing so was inspired by the analysis of ordinal structures based on elementarity invented by T.J. Carlson, see [T.J. Carlson, Elementary patterns of resemblance, Annals of Pure and Applied Logic 108 (...) 19–77], [G. Wilken, Σ1-Elementarity and Skolem hull operators, Annals of Pure and Applied Logic 145 162–175], and [G. Wilken, Assignment of ordinals to patterns of resemblance, The Journal of Symbolic Logic ]. Within the arithmetical context laid bare in this work, the “-numbers” play a role analogous to the role epsilon numbers play in the ordinal arithmetic based on the notion of Cantor normal form. (shrink)

1. Pohlers and The Problem. I first met Wolfram Pohlers at a workshop on proof theory organized by Walter Felscher that was held in Tübingen in early April, 1973. Among others at that workshop relevant to the work surveyed here were Kurt Schütte, Wolfram’s teacher in Munich, and Wolfram’s fellow student Wilfried Buchholz. This is not meant to slight in the least the many other fine logicians who participated there.2 In Tübingen I gave a couple of survey lectures on results (...) and problems in proof theory that had been occupying much of my attention during the previous decade. The following was the central problem that I emphasized there: The need for an ordinally informative, conceptually clear, proof-theoretic reduction of classical theories of iterated arithmetical inductive definitions to corresponding constructive systems. As will be explained below, meeting that need would be significant for the then ongoing efforts at establishing the constructive foundation for and proof-theoretic ordinal analysis of certain impredicative subsystems of classical analysis. I also spoke in Tübingen about. (shrink)

This article provides a detailed comparison between two systems of collapsing functions. These functions play a crucial role in proof theory, in the analysis of patterns of resemblance, and the analysis of maximal order types of well partial orders. The exact correspondence given here serves as a starting point for far reaching extensions of current results on patterns and well partial orders. © 2011 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim.

We introduce and analyze two theories for typed inductive definitions and establish their proof-theoretic ordinal to be the small Veblen ordinal \. We investigate on the one hand the applicative theory \ of functions, inductive definitions, and types. It includes a simple type structure and is a natural generalization of S. Feferman’s system \\). On the other hand, we investigate the arithmetical theory \ of typed inductive definitions, a natural subsystem of \, and carry out a wellordering proof within \ (...) that makes use of fundamental sequences for ordinal notations in an ordinal notation system based on the finitary Veblen functions. The essential properties for describing the ordinal notation system are worked out. (shrink)