A note on iterated consistency and infinite proofs (Q1734260)

Consider a transfinite sequence of arithmetical theories \(\mathbf T_\alpha=\mathbf{PRA}+\forall_{\gamma<\alpha} \mathrm{Con}(\mathbf T_\gamma)\). Then any arithmetical sentence \(\varphi\) is characterised by ordinals \(\alpha\) such that \(\mathbf T_\alpha\vdash\varphi\). The author applies the infinitary system \(\mathbf Z^*\) introduced by \textit{W. Buchholz} [Arch. Math. Logic 30, No. 5--6, 277--296 (1991; Zbl 0726.03038)] for the estimation of such ordinals for \(\Pi_1\) sentences. Namely, it is proved that any \(\Pi_1\)-formula with a cut-free \(\mathbf Z^*\)-proof of height \(\alpha\) has a (finitary) proof in \(\mathbf T_\alpha\). It is explained how a similar argument can be used for \(\Pi_n\)-sentences (\(n\ge2\)).