Bien que très coûteux à calculer pour les machines, les suites de Goodstein forment un exemple 'simple' d'algorithme récursif arithmétique (ce sont des suites d'entiers) qui peuvent s'implémenter très facilement dans n'importe quel langage manipulant l'arithmétique. L'algorithme se termine pour toute condition initiale, mais il a été (méta-)démontré que cette propriété n'est pas prouvable à partir des axiomes de Peano. On donnera ici le schéma d'une preuve simple reposant sur la théorie des nombres ordinaux (qui nécessite les axiomes usuels de la théorie des ensembles, par exemple ZF).