Observations

Есть такая Последовательность Гудстейна.

Берем какое-нибудь число, например, 42, выражаем его в двоичной системе: 2⁵+2³+2; показатели тоже разложим в двоичную,
2²²⁺¹+2^{21 + 1}+2. 

Это было начало. Дальше делаем вот что:
- меняем 2 на 3
- вычитаем единицу

Ну и там снова представляем в виде таких башенок. Затем меняем 3 на 4, опять вычитаем единицу, ну и т.д.

Понятно, что в конце концов дойдем до нуля.
Далеко не очевидно, что в аксиоматике Пеано это не докажешь. (Я честно не знаю, как доказывают, что она доходит до нуля, см линк.)

Ну вот. И можно сделать машину Тьюринга, которая строит эту последовательность. Понятно, что эта машина КОНЧАЕТ. Непонятно, как это доказать.