Arithmetical and Hyperarithmetical Worm Battles
Arithmetical and Hyperarithmetical Worm Battles
Abstract Japaridzeās provability logic ${\operatorname {GLP}}$ has one modality $[n]$ for each natural number and has been used by Beklemishev for a proof theoretic analysis of Peano arithmetic (${\operatorname {PA}}$) and related theories. Among other benefits, this analysis yields the so-called Every Worm Dies (${\operatorname {EWD}}$) principle, a natural combinatorial ā¦