Природа натуральных чисел

[epros]

epros в сообщении #1595229 писал(а):

она [арифметика Пеано 2 порядка] доказывает теорему Гудстейна, которая недоказуема в арифметике Пеано 1 порядка. Как Вы думаете, что должно появиться нового в цепочке вывода, чтобы это могло произойти, с учётом того, что в аксиоматике ничего нового не появилось?

В продолжение этой интересной темы о "природе натуральных чисел" с точки зрения аксиоматик разной силы я хочу слегка упростить свой вопрос о теореме Гудстейна (см. цитату выше). Действительно, арифметика Пеано первого порядка - уже достаточно сильная теория, а поэтому неразрешимое в ней утверждение получается достаточно нетривиальным. А ведь есть примеры попроще.

Вот есть такая функция Аккермана, которая представляет собой простейший пример общерекурсивной, но не примитивно рекурсивной функции. Это выражается в том, что значение функции определяется рекурсивно, но могут возникнуть некоторые трудности с доказательством того, что эта рекурсия обязательно закончится. И действительно, есть такие версии аксиоматики арифметики, в которых всюду определённость функции Аккермана недоказуема. Самый простой пример - примитивно рекурсивная арифметика (PRA) - представляет собой теорию натуральных чисел со сложением и умножением, которая может формализоваться без использования кванторов.

Давайте для начала посмотрим, как бы всякий нормальный студент, не связанный всякими там ограничениями аксиоматик, мог попытаться доказать, что рекурсия, вычисляющая значение функции Аккермана, обязательно закончится. Во-первых, он должен сразу заметить, что каждый шаг рекурсии либо уменьшает значение второго аргумента при том же значении первого, либо уменьшает значение первого аргумента (хотя значение второго аргумента при этом может увеличиться, причём иногда очень сильно). Во-вторых, он обязательно должен догадаться расположить пары аргументов в лексикографическом порядке. Это когда пара $(x+1,0)$ расположена дальше (правее) любой пары $(x,y)$, как и пара $(x,y+1)$ расположена дальше (правее) любой пары $(x,y)$.

Осталась самая малость: доказать, что любая последовательность пар аргументов, каждый следующий член которой лексикографически левее предыдущего, конечна. Тут бы нам в помощь трансфинитную индукцию, но студент таких слов не знает, поэтому пытается использовать обыкновенную математическую индукцию. Итак, ему сразу становится очевидным, что конечна любая такая последовательность, начинающаяся с $(0,y)$, ибо она не длиннее $y$. Далее студент замечает, что любая такая последовательность, начинающаяся с $(1,y^1)$, не позднее, чем через $y^1$ шагов дойдёт до члена вида $(0,y)$, а он уже знает, что оставшаяся часть последовательности окажется не длиннее $y$. Далее студент, наконец, применяет математическую индукцию и заключает, что раз из конечности любой последовательности, начинающейся с $(x,\cdot)$, следует конечность любой последовательности, начинающейся с $(x+1,\cdot)$, то и любая такая последовательность конечна. QED.

А теперь вопрос на засыпку: Что же может помешать формализовать эти несложные рассуждения в PRA? Ведь математическая индукция в ней отнюдь не запрещена.