Pi^0_1 ordinal analysis beyond first order arithmetic

TL;DR

This paper reviews Pi^0_1 ordinal analysis of PA using GLP logic, discusses extending it beyond PA, and simplifies the reflection rules, opening new applications for ordinal analysis.

Contribution

It introduces a simplified reflection rule approach that bypasses the full Reduction Property, enabling extensions of ordinal analysis beyond Peano Arithmetic.

Findings

Simplified reflection rules for ordinal analysis.

Full Reduction Property is not necessary for analysis.

Potential for applying ordinal analysis to stronger theories.

Abstract

In this paper we give an overview of an essential part of a Pi^0_1 ordinal analysis of Peano Arithmetic (PA) as presented by Beklemishev. This analysis is mainly performed within the polymodal provability logic GLP. We reflect on ways of extending this analysis beyond PA. A main difficulty in this is to find proper generalizations of the so-called Reduction Property. The Reduction Property relates reflection principles to reflection rules. In this paper we prove a result that simplifies the reflection rules. Moreover, we see that for an ordinal analysis the full Reduction Property is not needed. This latter observation is also seen to open up ways for applications of ordinal analysis relative to some strong base theory.