2021/12/14 by David Fernández–Duque, Fernández-Duque, David, Joost J. Joosten +6
Computer Science · #Computability, Logic, AI Algorithms #FOS: Mathematics #Logic (math.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.2112.07473
openalex publication_date 2021/12/14 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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Σn of Peano arithmetic. In order to prove the latter, we show that standard Hardy functions majorize their variants based on tree ordinals.