Proofs that Modify Proofs, 1/2

TL;DR

This paper conducts an ordinal analysis of a fragment of the μ-calculus related to parameter-free Π^1_2-comprehension, extending proof modification techniques to analyze proof systems' strength.

Contribution

It introduces an ordinal analysis approach for a fragment of the μ-calculus, interpreting functions on proofs as proofs in an expanded system, advancing proof modification methods.

Findings

Ordinal analysis of μ-calculus fragment established

Interpretation of functions on proofs as proofs in expanded systems

Method applied to systems of varying strength, including Π^1_1-comprehension

Abstract

This paper is a prelude and elaboration on Proofs that Modify Proofs. Here we present an ordinal analysis of a fragment of the $\mu$-calculus around the strength of parameter-free $\Pi^1_2$-comprehension using the same approach as that paper, interpreting functions on proofs as proofs in an expanded system. We build up the ordinal analysis in several stages, beginning by illustrating the method systems at the strength of paremeter-free $\Pi^1_1$-comprehension and full $\Pi^1_1$-comprehension.