A new system of proof-theoretic ordinal functions
type: Item
instance of: scholarly article
title: A new system of proof-theoretic ordinal functions
zbMATH Open document ID: 0655.03038
DOI: 10.1016/0168-0072(86)90052-7
author: Wilfried Buchholz
published in: Annals of Pure and Applied Logic
publication date: 1986-01-01T00:00:00Z
full work available at URL: 3841.pdf
review text: 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})\).
Mathematics Subject Classification ID: 03F15
zbMATH DE Number: 4068862
zbMATH Keywords: ordinal functions
zbMATH Keywords: large constructive ordinals
zbMATH Keywords: primitive recursive notation system
Wikidata QID: Q29396669
MaRDI profile type: Publication
OpenAlex ID: W2077219408
cites work: Provable wellorderings of formal theories for transfinitely iterated inductive definitions
cites work: ϱ-inaccessible ordinals, collapsing functions and a recursive notation system
cites work: Ordinals connected with formal theories for transfinitely iterated inductive definitions
cites work: Nichtbeweisbarkeit von gewissen kombinatorischen Eigenschaften endlicher Bäume;Unprovability of certain combinatorial properties of finite trees
DBLP publication ID: journals/apal/Buchholz86
description: scientific article; zbMATH DE number 4068862