Systems of iterated projective ordinal notations and combinatorial statements about binary labeled trees

We introduce the appropriate iterated version of the system of ordinal notations from G1] whose order type is the familiar Howard ordinal. As in G1], our ordinal notations are partly inspired by the ideas from P] where certain crucial properties of the traditional Munich' ordinal notations are isolated and used in the cut-elimination proofs. As compared to the corresponding impredicative Munich' ordinal notations (see e.g. B1, B2, J, Sch1, Sch2, BSch]), our ordinal notations arearbitrary terms in the appropriate simple term algebra based on the notion of collapsing functions (which we would rather identify as projective functions). In Sect. 1 below we define the systems of ordinal notationsPRJ(), for any primitive recursive limit wellordering. In Sect. 2 we prove the crucial well-foundness property by using the appropriate well-quasi-ordering property of the corresponding binary labeled trees G3]. In Sect. 3 we interprete inPRJ() the familiar Veblen-Bachmann hierarchy of ordinal functions, and in Sect. 4 we show that the corresponding Buchholz's system of ordinal notationsOT() is a proper subsystem ofPRJ(), although it has the same order type according to G3] together with the interpretation from Sect. 2 in the terms of labeled trees. In Sect. 5 we use Friedman's approach in order to obtain an appropriate purely combinatorial statement which is not provable in the theory of iterated inductive definitions ID_< , for arbitrarily large limit ordinal. Formal theories, axioms, etc. used below are familiar in the proof theory of subsystems of analysis (see BFPS, T, BSch]).