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

A notation system \underbar{PRJ}(P) for ordinals is defined where P is a fixed given primitive recursive well-ordering of the natural numbers without last element. The terms of the system are called iterated projective ordinal notations, using the expression projective instead of collapsing. The elements \(\nu\) of P act as projective points \(\Omega_{\nu}\), the so-called projective functions \(D_{\nu}\) constitute terms less than \(\Omega_{\nu}\). The functions \(D_{\nu}\) are similar to the \(\psi\)-functions of \textit{W. Buchholz} [Ann. Pure Appl. Logic 32, 195-207 (1986; Zbl 0655.03038)] but are developed generalizing the D-functions of the author [ibid. 38, No.1, 1-121 (1988)]. The well-ordering proof for \underbar{PRJ}(P) is given using on one hand the fact that the set \({\mathfrak T}^ 2(P)\) of the binary trees labelled by elements of P is a well-quasi-ordering with respect to some suitably modified embedding relation [cf. the author's paper in J. Symb. Logic 55, p. 157 (1990)], and on the other hand \underbar{PRJ}(P) is mapped into \({\mathfrak T}^ 2(P)\) in such a way that the relation between trees is carried over to the ordinal terms. The relation between the notations of the system \underbar{PRJ}(P) and the Veblen-Bachmann-hierarchy is outlined. The functions \(\phi_{\alpha}\) of this hierarchy and fundamental sequences are defined in \underbar{PRJ}(P) and illustrated by an example. The \(\epsilon\)- and \(\Gamma\)-numbers are denoted in the setting of \underbar{PRJ}(P). The system OT(P) of ordinal terms defined by Buchholz [loc. cit.] for \(P=\omega\) is described in \underbar{PRJ}(P) and an embedding is established. Finally, using the well-known idea of Friedman's, it is shown that some \(\Pi^ 0_ 2\)-sentences concerning the well-quasi-ordering of certain sets of binary trees labelled with ordinals cannot be proved in the corresponding theories of iterated inductive definitions. The proof uses the restriction of the already mentioned mapping from \underbar{PRJ}(P) to \({\mathfrak T}^ 2(P)\) to some ordinal \(\alpha +1\in P.\) The whole paper demonstrates the connections between ordinal notations and labelled trees in a very conclusive way.