Séquences de Goodstein et l'arithmétique de Peano

La séquence de Goodstein commence par un nombre naturel donné et se poursuit par des transformations successives grâce à une notation basée sur un système héréditaire de base.

L'arithmétique de Peano (PA) peut prouver chaque instance particulière où une séquence de Goodstein atteint zéro, mais elle ne peut pas prouver cette propriété pour tous les nombres naturels simultanément.

Pour prouver de manière générale que chaque séquence de Goodstein atteint zéro, il est nécessaire d'utiliser un système de preuve plus fort que PA, comme par exemple la théorie des ensembles de Zermelo-Fraenkel (ZF).

Même si PA peut encoder des calculs et prouver des séquences particulières, il lui manque la capacité de prouver la terminaison générale des séquences de Goodstein sans une extension comme le schéma de réflexion uniforme.

Malgré les limitations de PA pour démontrer le théorème de Goodstein dans sa totalité, il peut prouver des formes spécifiques d'induction transfinie pour certaines parties des ordres transfinis, mais pas pour l'ordinal tout entier ε₀.