id: 06019355
dt: j
an: 06019355
au: De Smet, Michiel; Weiermann, Andreas
ti: Goodstein sequences for prominent ordinals up to the Bachmann-Howard
    ordinal.
so: Ann. Pure Appl. Logic 163, No. 6, 669-680 (2012).
py: 2012
pu: Elsevier Science B.V. (North-Holland), Amsterdam
la: EN
cc: 
ut: Goodstein sequence; Bachmann-Howard ordinal; unprovability
ci: 
li: doi:10.1016/j.apal.2011.11.006
ab: Goodstein sequences give a well-known and easy-to-state principle that is
    independent of Peano arithmetic. The idea is to code the ordinals below
    $ε_0$ by natural numbers and to mimic a slow stepping-down function on
    the ordinals by a simple combination of elementary operations on the
    natural numbers (change of base and predecessor). In this paper the
    authors generalize the idea of Goodstein sequences to higher ordinals
    and corresponding systems of arithmetic, up through the Howard-Bachmann
    ordinal $φ_{ϵ_{Ω+1}}$ and the system $\mathrm{ID}_1$. The key idea
    is to define the generating rule of the sequences directly on the
    structure of the terms representing the ordinals in some canonical
    ordinal notation system. In particular one has to define the analog of
    the “$-1$" stepping-down operation in this general setting. The
    method allows to define Goodstein sequences corresponding to ordinals
    up through the Howard-Bachmann ordinal. The theorems asserting that the
    sequences terminate are unprovable in the corresponding systems of
    arithmetic, up through $\mathrm{ID}_1$. For example, Goodstein
    sequences with no termination proof in Peano arithmetic plus
    transfinite induction up to $Γ_0$ are obtained along the way. The
    proposed method avoids the problems of uniqueness of representation
    arising if one insists in coding the ordinal terms by integers. As a
    tradeoff, this choice makes the “number-theoretic" nature of the
    resulting statements less immediate compared to the original Goodstein
    sequences for $ε_0$.
rv: Lorenzo Carlucci (Rome)