A new system of proof-theoretic ordinal functions (Q1109029)

In this paper we present a family of ordinal functions \(\psi_ v(v\leq \omega)\), which seems to provide the so far simplest method for denoting large constructive ordinals. These functions are a simplified version of the \(\theta\)-functions, but nevertheless have the same strength as those. In Section 1 we define the functions \(\psi_ v\) and prove their main properties. In Section 2 we define a primitive recursive notation system (OT,\(\prec)\) based on the functions \(\psi_ v\). This system has the great advantage that its ordering relation \(\prec\) is very simple and can be defined without reference to sets of coefficients or any similar concept. OT is introduced as a subset of a larger set T of terms, which plays an important role in Section 3. There we show that the statement \(PRWO(\psi_ 0\Omega_{\omega})\), which says that there exist no primitive recursive infinite descending sequences in (\(\{\) \(x\in OT:\) \(x\prec \psi_ 0\Omega_{\omega}\},\prec)\), is not provable in \(\Pi^ 1_ 1-CA_ 0\). The proof of \(\Pi^ 1_ 1-CA_ 0\nvdash PRWO(\psi_ 0\Omega_{\omega})\) is based on the following results of \textit{W. Buchholz} [ibid. 33, 131-155 (1987; Zbl 0636.03052)]: \(ID_{\nu}\nvdash \forall n \exists k c^ n_{\nu}(k)=0\) (\(\nu\leq \omega)\), where \(c^ n_{\nu}(k)\in T\), for all \(n,k\in {\mathbb{N}}\); and every sequence \((c^ n_{\nu}(k))_{k\in {\mathbb{N}}}\) is primitive recursive. In Section 3 we prove \(c^ n_{\nu}(k)\in OT\) and \((c^ n_{\nu}(k)\neq 0\Rightarrow c^ n_{\nu}(k+1)\prec c^ n_{\nu}(k)).\) Since for all \(\nu <\omega\) we have \(c^ n_{\nu}(k)\prec \psi_ 0\Omega_{\omega}\), it follows that PRWO \((\psi_ 0\Omega_{\omega})\) implies \(\forall \nu <\omega \forall n \exists k c^ n_{\nu}(k)=0\). Since this can be proved in Peano Arithmetic and since \(\Pi^ 1_ 1-CA_ 0\) is conservative over \(\cup_{\nu <\omega}ID_{\nu}\) with respect to arithmetic sentences, we obtain now \(\Pi^ 1_ 1-CA_ 0\nvdash PRWO(\psi_ 0\Omega_{\omega})\).