Peano Arithmetic & Paris — Part 10: Goodstein & Kirby-Paris Indicators

graph TD DefHereditary["Def: Hereditary base-n notation (exponents recursively in base-n)"] DefBump["Def: Bump: replace base n with n+1 in hereditary representation"] DefGoodsteinSeq["Def: Goodstein sequence G_m: bump base, subtract 1, repeat"] DefOrdMap["Def: f(u,k): hereditary base-k → ordinal (replace k with ω)"] LemOrdDec["Lem: P_m(n) = f(G_m(n), n+1) strictly decreases"] LemWellFound["Lem: Ordinals well-founded ⇒ no infinite descending chain"] ThmGoodstein["Thm: Goodstein (1944): every G_m terminates at 0"] DefIndicator["Def: Indicator (Kirby-Paris): for nonstandard models of PA"] LemIndicator["Lem: Main indicator lemma: connects termination to ε₀"] DefNonStandard["Def: Nonstandard model of PA: contains infinite elements"] LemGoodsteinImpl["Lem: Goodstein termination implies ε₀ well-founded"] LemEps0["Lem: PA ⊬ ε₀ well-founded (Gentzen)"] ThmKirbyParis["Thm: Kirby-Paris: Goodstein unprovable in PA"] CorProvable["Cor: Goodstein provable in ACA₀, ZFC"] DefHereditary --> DefBump DefBump --> DefGoodsteinSeq DefHereditary --> DefOrdMap DefGoodsteinSeq --> DefOrdMap DefOrdMap --> LemOrdDec LemOrdDec --> LemWellFound LemWellFound --> ThmGoodstein DefIndicator --> LemIndicator DefNonStandard --> LemIndicator LemIndicator --> LemGoodsteinImpl ThmGoodstein --> LemGoodsteinImpl LemGoodsteinImpl --> ThmKirbyParis LemEps0 --> ThmKirbyParis ThmKirbyParis --> CorProvable classDef definition fill:#b197fc,color:#fff,stroke:#9775fa classDef lemma fill:#74c0fc,color:#fff,stroke:#4dabf7 classDef theorem fill:#51cf66,color:#fff,stroke:#40c057 classDef corollary fill:#1abc9c,color:#fff,stroke:#16a085 class DefHereditary,DefBump,DefGoodsteinSeq,DefOrdMap,DefIndicator,DefNonStandard definition class LemOrdDec,LemWellFound,LemIndicator,LemGoodsteinImpl,LemEps0 lemma class ThmGoodstein,ThmKirbyParis theorem class CorProvable corollary