Arithmetical and Hyperarithmetical Worm Battles

TL;DR

This paper extends provability logic $GLP$ to transfinite modalities, establishing soundness and independence results for arithmetical theories like $ACA$ and $I\Sigma_n$, and introduces related combinatorial principles.

Contribution

It demonstrates the soundness of transfinite extensions of $GLP$ and derives new combinatorial principles for arithmetical theories, expanding the understanding of provability logic.

Findings

Transfinite $GLP$ is sound for the interpretation of transfinite modalities.

Independent combinatorial principles are established for $ACA$ and $I\Sigma_n$.

Standard Hardy functions majorize variants based on tree ordinals.

Abstract

Japaridze's provability logic $GLP$ has one modality $[n]$ for each natural number and has been used by Beklemishev for a proof theoretic analysis of Peano aritmetic $(PA)$ and related theories. Among other benefits, this analysis yields the so-called Every Worm Dies $(EWD)$ principle, a natural combinatorial statement independent of $PA$. Recently, Beklemishev and Pakhomov have studied notions of provability corresponding to transfinite modalities in $GLP$. We show that indeed the natural transfinite extension of $GLP$ is sound for this interpretation, and yields independent combinatorial principles for the second order theory $ACA$ of arithmetical comprehension with full induction. We also provide restricted versions of $EWD$ related to the fragments $I\Sigma_n$ of Peano arithmetic. In order to prove the latter, we show that standard Hardy functions majorize their variants based on tree ordinals.