  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.
