\(\Pi_1^0\)-ordinal analysis beyond first-order arithmetic (Q2862108)

The paper gives an overview of an essential part of a \(\Pi_1^0\) ordinal analysis of \({\mathrm{PA}}\). This analysis is mainly performed within the polymodal provability logic \({\mathrm{GLP}}_\omega\). The system \({\mathrm{GLP}}\) was used as a basis for a simple proof-theoretic analysis of \({\mathrm{PA}}\) [\textit{L. D. Beklemishev}, Ann. Pure Appl. Logic 128, No. 1--3, 103--123 (2004; Zbl 1048.03045)]. The author reflects on ways of extending this analysis beyond \({\mathrm{PA}}\). He proves a result that simplifies the reflection principle, and shows that for an ordinal analysis the full reduction property is not needed.