очевидность понятия "равно".

[Someone]

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

У меня есть доказательство "метатеоремы" Гудстейна (ссылку на кусок своей статьи я здесь где-то уже приводил, если интересно, можете относительно его содержания поводить меня мордой по столу ).

Хотел напомнить Вам, что доказать такую теорему нельзя, поскольку можно найти нестандартные модели арифметики Пеано, в которых существуют контрпримеры к теореме Гудстейна, о чём я Вам однажды уже говорил. Однако обнаружил, что Alexey Romanov потратил массу усилий, чтобы втолковать Вам это (в теме "что следует из теоремы Геделя"), и, как я вижу, совершенно не преуспел в этом.

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

От собственно теоремы Гудстейна она отличается тем, что первая утверждает конечность любой последовательности Гудстейна, а вторая утверждает, что для каждой конкретной последовательности Гудстейна в арифметике Пеано есть доказательство её конечности (чувствуете разницу?).

Разницу мы, конечно, чувствуем, но дело в том, что упомянутый контрпример является "конкретным".

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

Следующий вопрос, который возникает, заключается в том, что мешает выполнить доказательство этой метатеоремы в самой арифметике Пеано. Собственно, у меня есть некие идеи относительно того, как этого добиться посредством некоего расширения синтаксиса: нужно добавить средства для записи примитивно-рекурсивных функций. Правда я пока не уверен, что это возможно без выхода за пределы стандартного исчисления предикатов.

Насколько я знаю, арифметика Пеано без символов для сложения и умножения является достаточно бедной теорией. Если добавить символ для сложения, то получается арифметика Пресбургера, которая также существенно беднее арифметики Пеано с символами сложения и умножения. Добавление обозначений для всех примитивно рекурсивных функций и соответствующих аксиом для них уже ни к какому расширению арифметики Пеано не приводит, то есть, является консервативным расширением её языка.

[Профессор Снэйп]

Someone в сообщении #232557 писал(а):

Добавление обозначений для всех примитивно рекурсивных функций и соответствующих аксиом для них уже ни к какому расширению арифметики Пеано не приводит, то есть, является консервативным расширением её языка.

А почему именно примитивно рекурсивных? Тогда уж рекурсивных, частично рекурсивных, или даже арифметических...

Впрочем, последнее приведёт к модельно полной теории. В то время как примитивно рекурсивные, рекурсивные, частично рекурсивные функции всего лишь будут снижать количество перемен кванторов в формулах максимум на единичку.

P. S. Тема выеденного яйца не стоит. Развели тут флуд, понимаешь!

[AGu]

Профессор Снэйп в сообщении #232761 писал(а):

P. S. Тема выеденного яйца не стоит. Развели тут флуд, понимаешь!

«Тут» -- это где? В этой теме? Тогда все законно: тема такая. Что же до выеденных яиц, то у кого-то, может, хобби такое -- на досуге запихивать в них желтки.

[epros]

AGu в сообщении #232529 писал(а):

epros писал(а):

Что особенного в требовании, чтобы каждый объект теории можно было назвать именем собственным?

То, что это требование по сути дела исключает возможность говорить об абстрактных объектах. Какие же это «абстрактные объекты», если они все -- «чиста конкретные» -- не то что поименованные, а фактически являющиеся именами?

Мне странно такое представление об абстрактности объектов, согласно которому объект абстрактен, если не существует его конкретных экземпляров (имеющих уникальные имена). По моим понятиям является абстрактным, например, объект "натуральное число". Но у него есть конкретные экземпляры: скажем, число 1 или число 2.

AGu в сообщении #232529 писал(а):

Рассмотрим теорию $\mathcal O_2$ с равенством, имеющую единственную специальную аксиому

$(\exists\,x)(\exists\,y)\bigl(x\ne y\ \&\ (\forall\,z)(z=x\ \lor\ z=y)\bigr)$.

Думаю, многие согласятся с тем, что $\mathcal O_2$ -- это «теория двух объектов». Тем не менее, теория $\mathcal O_2$ не имеет ни одного объекта во 2-м смысле. Вас это не смущает?

Интересно, откуда взято соображение о том, что это - "теория двух объектов"? Вы можете их указать?

-- Пн авг 24, 2009 14:26:40 --

Someone в сообщении #232557 писал(а):

Хотел напомнить Вам, что доказать такую теорему нельзя, поскольку можно найти нестандартные модели арифметики Пеано, в которых существуют контрпримеры к теореме Гудстейна, о чём я Вам однажды уже говорил.

Хотелось бы услышать возражения по приведённому тексту доказательства: в чём ошибка. Соображения о том, что его "не может быть", звучат слишком абстрактно.

Хочу также заметить, что я уже однажды отвечал (и Вам, и Alexey Romanov), что утверждение "метатеоремы Гудстейна" касается только стандартных натуральных чисел, а именно таких, которые выражаются строками вида $S( \dots S(0) \dots )$, так что Ваше возражение не в тему.

Someone в сообщении #232557 писал(а):

Насколько я знаю, арифметика Пеано без символов для сложения и умножения является достаточно бедной теорией. Если добавить символ для сложения, то получается арифметика Пресбургера, которая также существенно беднее арифметики Пеано с символами сложения и умножения.

Я это знаю. Для арифметики Пресбургера доказана полнота, так что расширить её язык таким образом (чтобы стали доказываться ранее недоказуемые утверждения), очевидно, не получится.

Someone в сообщении #232557 писал(а):

Добавление обозначений для всех примитивно рекурсивных функций и соответствующих аксиом для них уже ни к какому расширению арифметики Пеано не приводит, то есть, является консервативным расширением её языка.

Интересно, на чём основано это утверждение? Хотелось бы посмотреть, каким образом переводятся на язык арифметики Пеано формулы с участием функции $\Lambda_m$, которая рекурсивно определена в том куске статьи, который я приводил выше.

[man]

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

Как Вы можете заметить, объектам первого рода (замкнутым термам, примеры: $0, S(0), S(S(0)), \dots$) соответствуют объекты второго рода (формулы теории, примеры: $x=0, x=S(0), x=S(S(0)), \dots$). Так что второе определение в некотором смысле расширяет первое: я учёл Вашу претензию (которая показалась мне обоснованной), что теории без констант не следует лишать прав "определять объекты".

Какого рода объектом будет: $x=S(x)$ ? Как в данном случае понимать равенство ? Вообще, что такое $S$, по сути, помимо того, что это имя процедуры взятия в скобки (фигурные или нет, неважно) ?

[epros]

man в сообщении #238316 писал(а):

Какого рода объектом будет: $x=S(x)$?

Никакого. У нас нет доказательства $\exists! x (x=S(x))$, поэтому мы не можем утверждать в соответствии с определением, что это - объект.

[AGu]

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

AGu в сообщении #232529 писал(а):

Рассмотрим теорию $\mathcal O_2$ с равенством, имеющую единственную специальную аксиому

$(\exists\,x)(\exists\,y)\bigl(x\ne y\ \&\ (\forall\,z)(z=x\ \lor\ z=y)\bigr)$.

Думаю, многие согласятся с тем, что $\mathcal O_2$ -- это «теория двух объектов». Тем не менее, теория $\mathcal O_2$ не имеет ни одного объекта во 2-м смысле. Вас это не смущает?

Интересно, откуда взято соображение о том, что это - "теория двух объектов"? Вы можете их указать?

Если бы мне было позволено произнести слово «модель» , я бы сказал, что всякая модель теории $\mathcal O_2$ состоит из двух объектов, но в данном случае я буду вынужден сказать, что это соображение родом из интуиции, как и «абстрактные объекты». Поэтому я и написал «Думаю, многие согласятся с тем, что...», а не «Очевидно, что...» или «В определенном смысле...». На мой взгляд, аксиому $(\exists\,x)(\exists\,y)\bigl(x\ne y\ \&\ (\forall\,z)(z=x\ \lor\ z=y)\bigr)$ можно неформально прочитать так: «существуют два различных объекта $x$ и $y$ такие, что всякий объект равен одному из них». Если Ваша интуиция сопротивляется такому прочтению и не подсказывает, что «абстрактный мир» теории $\mathcal O_2$ «состоит из двух объектов», то у нас с Вами очень разные интуиции, и дальнейшую дискуссию ожидает очередной тупик.

[epros]

AGu в сообщении #238437 писал(а):

Если бы мне было позволено произнести слово «модель» , я бы сказал, что всякая модель теории $\mathcal O_2$ состоит из двух объектов

Произнести слово «модель» можно, только нужно не забыть, что это понятие основано на весьма нетривиальной аксиоматике, куда более навороченной, чем аксиоматика рассматриваемой теории. А это наводит на мысль, что рассуждения о «количестве» объектов теории характерны скорее для этой аксиоматики, а не для рассматриваемой теории «самой по себе».

AGu в сообщении #238437 писал(а):

На мой взгляд, аксиому $(\exists\,x)(\exists\,y)\bigl(x\ne y\ \&\ (\forall\,z)(z=x\ \lor\ z=y)\bigr)$ можно неформально прочитать так: «существуют два различных объекта $x$ и $y$ такие, что всякий объект равен одному из них».

В плане буквоедства я бы уточнил: «существуют различные объекты $x$ и $y$ такие, что всякий объект равен какому-то из них». Чтобы применить слово «два», как это сделали Вы, нужно, как минимум, уметь считать, т.е. иметь понятие об арифметике. Конечно же, метатеория, имеющая понятие об арифметике, сможет подсчитать количество переменных, стоящих под кванторами в формуле Даже более того: она сможет сформулировать утверждение о том, что объектов теории согласно её собственному заявлению не более двух. Для этого даже не потребуются те сильные допущения, на которых основана теория моделей, хотя и понятие об арифметике - это тоже кое-что.

Если Мы с Вами согласимся с тем, что за метатеорией можно по умолчанию признать право иметь какие-то понятия об арифметике (а я против этого не возражаю), то в интерпретации такой метатеории Ваша теория определяет «пару объектов». Но отсюда ещё очень далеко до того, чтобы утверждать, что эта теория определяет каждый объект из этой пары.

[AGu]

Опуская несущественные (для меня) детали, цитирую главное:

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

В плане буквоедства я бы уточнил: «существуют различные объекты [...]

Итак, Вы признали, что (интуитивно) в «мире» теории $\mathcal O_2$ «существуют различные объекты». С другой стороны, по Вашему (второму) определению теория $\mathcal O_2$ не имеет объектов. Если это — не противоречие с интуицией, то что это?

[man]

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

man в сообщении #238316 писал(а):

Какого рода объектом будет: $x=S(x)$?

Никакого. У нас нет доказательства $\exists! x (x=S(x))$, поэтому мы не можем утверждать в соответствии с определением, что это - объект.

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

Как Вы можете заметить, объектам первого рода (замкнутым термам, примеры: $0, S(0), S(S(0)), \dots$) соответствуют объекты второго рода (формулы теории, примеры: $x=0, x=S(0), x=S(S(0)), \dots$). Так что второе определение в некотором смысле расширяет первое: я учёл Вашу претензию (которая показалась мне обоснованной), что теории без констант не следует лишать прав "определять объекты".

Разве это не объект второго рода (формула теории) ?
По поводу сути оператора "свертки" (заключения в скобки) $S$ и равенства. Когда имеется "объект" $x$ для определения которого, как объекта первого рода, требуется бесконечно много скобок $x=((...))$, то применение к нему свертки $S(x)$ пораждает не "такой же", а "тот же самый" объект $(((...)))$.
Формула $x=S(x)$ судя по всему такая же независимая аксиома, как и $x \neq S(x)$, (Вы это имели в виду, когда говорили о недоказуемости $\exists! x (x=S(x))$ ?) но, как теория содержащая вторую аксиому, сможет различить объкты $((...))$ и $(((...)))$ непонятно, т.к. "изнутри" строк не видно, видны лишь "множества" ?

[Someone]

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

По моим понятиям является абстрактным, например, объект "натуральное число". Но у него есть конкретные экземпляры: скажем, число 1 или число 2.

А нету такого объекта - "натуральное число". Или Вы имели в виду натуральный ряд? Когда мы говорим "пусть $n$ - натуральное число", то символ (переменная) "n" является (временным) именем некоторого объекта, являющегося натуральным числом. Поскольку он конкретно здесь никак не задан, его, видимо, следует считать абстрактным. AGu, поправьте меня, пожалуйста, если я неправильно понимаю термин "абстрактный объект".

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

Someone в сообщении #232557 писал(а):

Хотел напомнить Вам, что доказать такую теорему нельзя, поскольку можно найти нестандартные модели арифметики Пеано, в которых существуют контрпримеры к теореме Гудстейна, о чём я Вам однажды уже говорил.

Хотелось бы услышать возражения по приведённому тексту доказательства: в чём ошибка. Соображения о том, что его "не может быть", звучат слишком абстрактно.

Вы понимаете, что такое контрпример и какова его роль?
А поиск ошибок - это обязанность автора "доказательства", а не автора контрпримера.

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

Хочу также заметить, что я уже однажды отвечал (и Вам, и Alexey Romanov), что утверждение "метатеоремы Гудстейна" касается только стандартных натуральных чисел, а именно таких, которые выражаются строками вида $S( \dots S(0) \dots )$, так что Ваше возражение не в тему.

А что есть Ваша метатеория? Если это теория множеств, и в ней натуральные числа изображаются конечными ординалами, так что аксиомы арифметики являются теоремами теории множеств, то вопросов нет, и доказательство известно.

Если же в качестве метатеории Вы используете арифметику, то в ней "стандартные" и "нестандартные" натуральные числа различить нельзя, поскольку все они одинаково удовлетворяют всем аксиомам. В частности, схема индукции определяет последовательность $0,S(0),S(S(0)),S(S(S(0))),\ldots$ для всех натуральных чисел, как для стандартных, так и для нестандартных. Конечно, Вы можете не определять эту последовательность схемой индукции, но тогда я бы очень хотел посмотреть, как Вы её определяете и доказываете выполнение аксиом арифметики, а также отличаете стандартные натуральные числа от нестандартных.
Ещё одно соображение состоит в том, что утверждение, не выполняющееся хотя бы в одной модели, является недоказуемым (разумеется, мы предполагаем непротиворечивость Вашей метатеории).
Поскольку одной из моделей Вашей метатеории является та, в которой теорема Гудстейна ложна, то сразу получаем контрпример к Вашему доказательству.

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

Someone в сообщении #232557 писал(а):

Добавление обозначений для всех примитивно рекурсивных функций и соответствующих аксиом для них уже ни к какому расширению арифметики Пеано не приводит, то есть, является консервативным расширением её языка.

Интересно, на чём основано это утверждение? Хотелось бы посмотреть, каким образом переводятся на язык арифметики Пеано формулы с участием функции $\Lambda_m$, которая рекурсивно определена в том куске статьи, который я приводил выше.

Вам на этот вопрос ответили уже в другой теме.

Профессор Снэйп в сообщении #232761 писал(а):

А почему именно примитивно рекурсивных?

Потому что об этом спросил epros.

[epros]

AGu в сообщении #238491 писал(а):

Опуская несущественные (для меня) детали, цитирую главное:

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

В плане буквоедства я бы уточнил: «существуют различные объекты [...]

Итак, Вы признали, что (интуитивно) в «мире» теории $\mathcal O_2$ «существуют различные объекты». С другой стороны, по Вашему (второму) определению теория $\mathcal O_2$ не имеет объектов. Если это — не противоречие с интуицией, то что это?

Нет, не так. Теория $\mathcal O_2$ утверждает, что существуют различные объекты. Но при этом теория $\mathcal O_2$ не определяет ни одного объекта. Не вижу противоречия.

Другой аналогичный пример: Теория ZFC утверждает, что существуют нелинейные аддитивные функции $\mathbb{R} \to \mathbb{R}$, но она не определяет ни одной такой функции.

-- Пт авг 28, 2009 10:37:19 --

man в сообщении #238512 писал(а):

Разве это не объект второго рода (формула теории) ?

В определении № 2 было сказано: Формула теории, такая что ...
В данном случае условие "такая что ..." не выполнено.

man в сообщении #238512 писал(а):

Когда имеется "объект" $x$ для определения которого, как объекта первого рода, требуется бесконечно много скобок $x=((...))$

Не существует термов с бесконечным количеством скобок. (Напоминаю, что в определении № 1 под объектами, определёнными теорией, понимались именно замкнутые термы).

man в сообщении #238512 писал(а):

Формула $x=S(x)$ судя по всему такая же независимая аксиома, как и $x \neq S(x)$, (Вы это имели в виду, когда говорили о недоказуемости $\exists! x (x=S(x))$ ?)

Недоказуемое - значит либо противоречащее аксиоматике (непротиворечивой теории), либо независимое от неё. Какой из вариантов имеет место, в данный момент сказать не берусь.

-- Пт авг 28, 2009 11:01:49 --

Someone в сообщении #238559 писал(а):

А нету такого объекта - "натуральное число". Или Вы имели в виду натуральный ряд? Когда мы говорим "пусть $n$ - натуральное число", то символ (переменная) "n" является (временным) именем некоторого объекта, являющегося натуральным числом. Поскольку он конкретно здесь никак не задан, его, видимо, следует считать абстрактным.

Это вопрос терминологии. Иногда, говоря "объект", подразумевают конкретный объект. Но я исхожу из терминологии, допускающей абстрактные объекты, такие как "стул" (без конкретизации какой именно). Так что я имел в виду не "натуральный ряд", а именно "натуральное число" (отдельно взятое, но без конкретизации какое именно).

Someone в сообщении #238559 писал(а):

Вы понимаете, что такое контрпример и какова его роль?
А поиск ошибок - это обязанность автора "доказательства", а не автора контрпримера.

Я Вам указал на некорректность Вашего контрпримера (утверждение метатеоремы касается стандартных чисел, а Ваш пример - с нестандартным числом). На этом "обязанность автора" считаю исполненной.

Someone в сообщении #238559 писал(а):

А что есть Ваша метатеория? Если это теория множеств, и в ней натуральные числа изображаются конечными ординалами, так что аксиомы арифметики являются теоремами теории множеств, то вопросов нет, и доказательство известно.

Нет, выше я уже говорил, что мои метатеоретические рассуждения формализуемы в стандартном исчислении предикатов первого порядка плюс индукция по натуральным числам. Без всякой теории множеств.

Someone в сообщении #238559 писал(а):

Если же в качестве метатеории Вы используете арифметику, то в ней "стандартные" и "нестандартные" натуральные числа различить нельзя, поскольку все они одинаково удовлетворяют всем аксиомам. В частности, схема индукции определяет последовательность $0,S(0),S(S(0)),S(S(S(0))),\ldots$ для всех натуральных чисел, как для стандартных, так и для нестандартных.

Речь идёт об индукции, выполняемой начиная со стандартного числа 0 (есть такая константа в языке арифметики Пеано).

Someone в сообщении #238559 писал(а):

Конечно, Вы можете не определять эту последовательность схемой индукции

Используется стандартная схема индукции из арифметики Пеано.

Someone в сообщении #238559 писал(а):

Цитата:

Интересно, на чём основано это утверждение? Хотелось бы посмотреть, каким образом переводятся на язык арифметики Пеано формулы с участием функции $\Lambda_m$, которая рекурсивно определена в том куске статьи, который я приводил выше.

Вам на этот вопрос ответили уже в другой теме

На какой из вопросов?

Если на первый (на чём основано утверждение, что получим консервативное расширение теории), то я такого ответа не вижу: Где вообще продемонстрирован способ "добавления обозначений для всех примитивно рекурсивных функций и соответствующих аксиом для них"?

Если на второй, то указанный по ссылке способ перевода формул не применим для формул с участием функции $\Lambda_m$, он был предназначен только для перевода формул с новой константой.

[anik]

Уважаемый conviso! Может быть вы удовлетворитесь моим мнением по поводу равенства?
Прежде всего аксиома: в природе не существуют два одинаковых объекта. Даже кристаллы одного и того же вещества - различны. Если два, то различные. Мы же не говорим: в классе находились двадцать различных учеников (понимая, что ученики не могут быть одинаковы).
Обрисую ситуацию похожую на ситуацию с зайцами: один отдел в магазине обслуживают два продавца, к ним стоят две очереди, по 10 человек в каждой. Эти две череди можно рассматривать как два множества А и В с упорядоченными элементами и эти элементы есть возможность попарно сравнить. По количеству человек эти две очереди равны. Но, равны ли множества А и В? "Если каждый элемент множества А равен соответствующему элементу множества В то такие множества равны". Но в очереди А последний стоит мужчина, а в очереди В последняя стоит женщина. Равна ли женщина мужчине? Если же в действительности каждый человек в очереди А равен человеку в очереди В, то это означает, что очередь одна, а продавцов, обслуживающих эту очередь двое.
Равными могут быть объекты по наличию в них одного и того же свойства. Так две очереди равны по количеству человек стоящих в них. Два шарика равны по диаметру. Здесь равенство уже приближённое, поскольку диаметру сопоставлено действительное число, а количеству человек - натуральное.

[Someone]

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

Теория $\mathcal O_2$ утверждает, что существуют различные объекты. Но при этом теория $\mathcal O_2$ не определяет ни одного объекта.

Что это значит? А арифметика Пеано определяет какие-нибудь объекты?

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

Someone в сообщении #238559 писал(а):

Вы понимаете, что такое контрпример и какова его роль?
А поиск ошибок - это обязанность автора "доказательства", а не автора контрпримера.

Я Вам указал на некорректность Вашего контрпримера (утверждение метатеоремы касается стандартных чисел, а Ваш пример - с нестандартным числом). На этом "обязанность автора" считаю исполненной.

Не пройдёт. Потрудитесь объяснить, как Вы с помощью аксиом арифметики Пеано отличаете стандартные натуральные числа от нестандартных.

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

Someone в сообщении #238559 писал(а):

Если же в качестве метатеории Вы используете арифметику, то в ней "стандартные" и "нестандартные" натуральные числа различить нельзя, поскольку все они одинаково удовлетворяют всем аксиомам. В частности, схема индукции определяет последовательность $0,S(0),S(S(0)),S(S(S(0))),\ldots$ для всех натуральных чисел, как для стандартных, так и для нестандартных.

Речь идёт об индукции, выполняемой начиная со стандартного числа 0 (есть такая константа в языке арифметики Пеано).

Ну и что? Она по определению начинается со стандартного числа $0$. В аксиоме так написано. И включает все натуральные числа, какие есть. Как стандартные, так и нестандартные. Это тоже написано в той же аксиоме.

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

Someone в сообщении #238559 писал(а):

Вам на этот вопрос ответили уже в другой теме

На какой из вопросов?

Если на первый (на чём основано утверждение, что получим консервативное расширение теории), то я такого ответа не вижу: Где вообще продемонстрирован способ "добавления обозначений для всех примитивно рекурсивных функций и соответствующих аксиом для них"?

Господи... Все примитивно рекурсивные функции (и даже все частично рекурсивные) определяются в языке арифметики Пеано системами уравнений (деталей не знаю, никогда не интересовался). Предположим, у нас есть некоторая формула, содержащая символ $f(x)$ для значения такой функции. Перед формулой пишем $\exists a(\text{определение }f(x))$ (в определении, естественно, заменяем $f(x)$ на $a$), затем в формуле заменяем $f(x)$ на $a$. Именно это имел в виду Профессор Снэйп, когда говорил, что введение в язык арифметики нового символа для такой функции всего лишь приводит к уменьшению числа кванторов в формуле на единицу.

[epros]

Someone в сообщении #238646 писал(а):

А арифметика Пеано определяет какие-нибудь объекты?

Ранее это обсуждалось: Определяет в любом из двух указанных определений. В смысле первого определения - это термы вида $S( \dots S(0) \dots)$. В смысле второго определения - это формулы вида $x = S( \dots S(0) \dots)$.

Someone в сообщении #238646 писал(а):

Потрудитесь объяснить, как Вы с помощью аксиом арифметики Пеано отличаете стандартные натуральные числа от нестандартных.

Если бы Вы потрудились хотя бы взглянуть на доказательство, то у Вас не возникали бы такие вопросы. Доказательство построено таким образом, что сначала доказывается $(PA \vdash G(n)) \rightarrow (PA \vdash G(n+1))$ для любого $n$ (строки) и $PA \vdash G(0)$, а потом вывод $\forall n \in \mathbb{N} ~ (PA \vdash G(n))$ получается индукцией (по термам $0, 0+1, 0+1+1, \dots$).

Так что для меня "стандартные" числа - это такие, которые можно получить индукцией из 0:
- имеем $0 \in \mathbb{N}$ (1)
- имеем $\forall n ~ (n \in \mathbb{N} \rightarrow n+1 \in \mathbb{N})$ (2)
- по индукции из (1) и (2) получаем: $\forall n ~ (n \in \mathbb{N})$

Никаких "нестандартных" чисел моя метатеория вообще не знает.

Someone в сообщении #238646 писал(а):

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

Речь идёт об индукции, выполняемой начиная со стандартного числа 0 (есть такая константа в языке арифметики Пеано).

Ну и что? Она по определению начинается со стандартного числа $0$. В аксиоме так написано. И включает все натуральные числа, какие есть. Как стандартные, так и нестандартные. Это тоже написано в той же аксиоме.

Я не знаю о чём Вы говорите. В моей метатеории, которая содержит арифметику, но ничего не знает про "множества", все числа, которые можно получить индукцией начиная с нуля, являются "стандартными". Про "нестандартные" она вообще ничего не знает. В этой метатеории можно определить предикат $n \in \mathbb{N}$ (пусть Вас не смущает форма записи, намекающая на теоретико-множественное отношение принадлежности множеству - можно это записать и предикатным символом). И для этой предикатной формулы можно записать соответствующую аксиому индукции.

Someone в сообщении #238646 писал(а):

Все примитивно рекурсивные функции (и даже все частично рекурсивные) определяются в языке арифметики Пеано системами уравнений (деталей не знаю, никогда не интересовался).

А давайте поинтересуемся. У меня функция $\Lambda_k$ рекурсивно определяется так:
$\Lambda_1(n,m_1) = m_1$
$\Lambda_k(n,m_1, \dots , m_k) = m_k + n^{\Lambda_{k-1}(n,m_1, \dots , m_{k-1})}$

Someone в сообщении #238646 писал(а):

Предположим, у нас есть некоторая формула, содержащая символ $f(x)$ для значения такой функции.

Это не наш случай. Если бы была общая формула для функции $\Lambda_k$, то никаких проблем с доказуемостью в арифметике не было бы. Утверждения метатеории состоят в другом: Для любого натурального $k$ существует формула арифметики, такая что ....