что следует из теоремы Геделя

[epros]

Alexey Romanov в сообщении #223247 писал(а):

Это доказано, но не в Вашей теории. (И это доказательство как раз использует то, чего Вы не хотите допускать в свою теорию.)

Ошибаетесь, как раз это доказано в этой теории - в теории, которая знает, что такое стандартные натуральные числа, но не факт, что ей известно что-либо про "нестандартные".

Всё на самом-то деле очень просто: В синтаксисе арифметики есть константа $0$ и через функцию инкремента мы можем записать выражения вида $S(0)$, $S(S(0))$ и т.п. Это всё - правильные выражения в синтаксисе арифметики, и через такие выражения можно записать любое стандартное натуральное число. Для любого $n$ из таких чисел существует доказательство $G(n)$.

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

Alexey Romanov в сообщении #223247 писал(а):

Вместо этого я предложил бы Вам рассмотреть арифметику с $\omega$-правилом. ("Из $p(0), p(1), p(2), \ldots$ выводится $$\forall n ~ p(n)$.")

Давайте попробуем для начала это утверждение формализовать. Синтаксис $p(0), p(1), p(2), \ldots$ я не понимаю, а на неформальном уровне рассматривать мета-теорию неинтересно: Эдак можно начать делать какие угодно "содержательные выводы" (в терминологии Инта), которые не ограничены ничем, кроме фантазий автора.

[Xaositect]

Alexey Romanov в сообщении #223169 писал(а):

Это, очевидно, неверно. Если бы оно было истинно в любой модели арифметики, то оно было бы доказуемо в ней по теореме Гёделя о полноте.

My bad.
А как, кстати, выглядит модель, в которой это утверждение ложно? Я себе плохо ее представляю.

-- Пт июн 19, 2009 12:42:27 --

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

Давайте попробуем для начала это утверждение формализовать. Синтаксис $p(0), p(1), p(2), \ldots$ я не понимаю, а на неформальном уровне рассматривать мета-теорию неинтересно: Эдак можно начать делать какие угодно "содержательные выводы" (в терминологии Инта), которые не ограничены ничем, кроме фантазий автора.

Как я понимаю.
Оно означает, что $\forall n\ p(n)$ является теоремой, если теоремами являются все формулы $p(i)$, полученные подстановкой нумералов в $p(n)$ вместо $n$.
Если ввести это правило, множество теорем может стать рекурсивно неперечислимым (Но, если я не ошибаюсь, будет $\Sigma_2$).

[Alexey Romanov]

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

Alexey Romanov в сообщении #223247 писал(а):

Это доказано, но не в Вашей теории. (И это доказательство как раз использует то, чего Вы не хотите допускать в свою теорию.)

Для любого $n$ из таких чисел существует доказательство $G(n)$.

Да, существует. Но доказать существование этого доказательства без использования ординалов и прочего инструментария теории множеств нельзя. А их в Вашей теории нет...

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

Alexey Romanov в сообщении #223247 писал(а):

Вместо этого я предложил бы Вам рассмотреть арифметику с $\omega$-правилом. ("Из $p(0), p(1), p(2), \ldots$ выводится $$\forall n ~ p(n)$.")

Давайте попробуем для начала это утверждение формализовать. Синтаксис $p(0), p(1), p(2), \ldots$ я не понимаю, а на неформальном уровне рассматривать мета-теорию неинтересно: Эдак можно начать делать какие угодно "содержательные выводы" (в терминологии Инта), которые не ограничены ничем, кроме фантазий автора.

Если для любого стандартного натурального $n$ выводится $p(n)$, то выводится $\forall n ~ p(n)$. Разумеется, в логике первого порядка это формализовать нельзя, так же как и ваши рассуждения; нужна инфинитарная логика.

Xaositect в сообщении #223259 писал(а):

А как, кстати, выглядит модель, в которой это утверждение ложно? Я себе плохо ее представляю.

А какие-нибудь нестандартные модели арифметики Вы представляете хорошо? Я, например, нет.

Но дело в том, что предикаты $Ax(x) \equiv$ "$x$ есть Гёделевский номер аксиомы арифметики", $Pr(x, y) \equiv$ "$x$ есть Гёделевский номер доказательства формулы с Гёделевским номером $y$", и т.д. нормально работают на стандартных числах. Но легко доказать, что в любой нестандартной модели арифметики есть нестандартное число $N$ такое, что истинно $Ax(N)$. Естественно, на самом деле номера всех аксиом стандартны. Так что в нестандартных моделях эти предикаты просто выражают нечто другое...

[Xaositect]

Alexey Romanov в сообщении #223265 писал(а):

А какие-нибудь нестандартные модели арифметики Вы представляете хорошо? Я, например, нет.

Ну, есть конструкции, которые по крайней мере кажутся понятными.

[epros]

Xaositect в сообщении #223259 писал(а):

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

Давайте попробуем для начала это утверждение формализовать. Синтаксис $p(0), p(1), p(2), \ldots$ я не понимаю

Как я понимаю.
Оно означает, что $\forall n\ p(n)$ является теоремой, если теоремами являются все формулы $p(i)$, полученные подстановкой нумералов в $p(n)$ вместо $n$.
Если ввести это правило, множество теорем может стать рекурсивно неперечислимым (Но, если я не ошибаюсь, будет $\Sigma_2$).

Давайте запишем формально. Что-нибудь вроде этого:
$(\forall i \in \mathbb{N}) (A \vdash p(i)) \rightarrow (A \vdash (\forall i \in \mathbb{N})~ p(i))$?

А нафига оно нам нужно? Если теория истинная, т.е. $(A \vdash p) \rightarrow p$, то из левой части импликации выводимо более интересное: $(\forall i \in \mathbb{N})~ p(i)$. А если нет, то какая нам разница, что в ней невыводимо $(\forall i \in \mathbb{N})~ p(i)$?

Alexey Romanov в сообщении #223265 писал(а):

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

Для любого $n$ из таких чисел существует доказательство $G(n)$.

Да, существует. Но доказать существование этого доказательства без использования ординалов и прочего инструментария теории множеств нельзя. А их в Вашей теории нет...

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

Alexey Romanov в сообщении #223265 писал(а):

Разумеется, в логике первого порядка это формализовать нельзя, так же как и ваши рассуждения; нужна инфинитарная логика.

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

[Alexey Romanov]

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

А нафига оно нам нужно?

Чтобы позволить доказать теорему Гудстейна.

Ещё раз. Арифметика не позволяет доказать, что все числа стандартные (и даже определить предикат $n \in \mathbb{N}$). Так что символ $\mathbb{N}$ Вы, очевидно, добавляете в метатеории. Но мне непонятно, какие аксиомы и/или правила вывода Вы для него вводите, если Вас не устраивает $\omega$-правило.

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

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

И формализуемое в арифметике? Именно $(\forall i \in \mathbb{N}) (A \vdash p(i))$? Если так, очень интересно. Особенно потому, что арифметика не знает ничего про стандартные числа, и это было бы доказательством в арифметике $\forall i ~ (A \vdash p(i))$.

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

Оставляю без комментария слова про "... как и ваши рассуждения ..."

А зря. Потому что отличить $\forall n \in \mathbb{N}$ и арифметическое $\forall n$ без $\omega$-правила или какого-то его аналога у Вас не получится.

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

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

А вот доказательство

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

$(\forall n \in \mathbb{N})(A \vdash G(n))$,

в Вашей теории, как мне кажется, будет бесконечно длинным. Жду обещанного куска статьи.

[epros]

Alexey Romanov в сообщении #223312 писал(а):

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

А нафига оно нам нужно?

Чтобы позволить доказать теорему Гудстейна.

В арифметике?
А нафига нам "позволять" её доказывать в арифметике, если известно, что в арифметике она недоказуема?

Это очень странный подход: Вводить дополнительное правило вывода, согласно которому "доказуемым" должно считаться всякое такое, что недоказуемо стандартными средствами, но не противоречит теории... Эдак действительно можно прийти к рекурсивно неперечислимому множеству теорем (и это при рекурсивной перечислимости высказываний теории ), к "инфинитарной логике" и к прочей ерунде.

Alexey Romanov в сообщении #223312 писал(а):

Ещё раз. Арифметика не позволяет доказать, что все числа стандартные (и даже определить предикат $n \in \mathbb{N}$). Так что символ $\mathbb{N}$ Вы, очевидно, добавляете в метатеории. Но мне непонятно, какие аксиомы и/или правила вывода Вы для него вводите, если Вас не устраивает $\omega$-правило.

Не добавляю никаких аксиом. Для доказательства $(\forall n \in \mathbb{N})(A \vdash G(n))$ нужно стандартное исчисление предикатов первого порядка + индукция по натуральным числам.

Естественно, индукция начинается с числа $0$, т.е. с той самой константы, которая определена самой арифметикой. Это гарантирует, что речь идёт именно о "стандартных" натуральных числах.

Alexey Romanov в сообщении #223312 писал(а):

И формализуемое в арифметике? Именно $(\forall i \in \mathbb{N}) (A \vdash p(i))$? Если так, очень интересно. Особенно потому, что арифметика не знает ничего про стандартные числа, и это было бы доказательством в арифметике $\forall i ~ (A \vdash p(i))$.

Само утверждение $(\forall i \in \mathbb{N}) (A \vdash p(i))$ конечно же не является формализуемым в арифметике. Оно - метатеоретическое.

Относительно того, что "арифметика не знает ничего про стандартные числа", думаю, Вы не совсем точны: Арифметика "знает", что константа $0$ является "стандартным" числом, и $S(0)$ тоже, и т. д. А вот про "нестандартные" числа она действительно ничего не знает. Хотя, можно, конечно, сказать, что это "знает" не арифметика (ибо она - просто набор значков), а мы. Но суть, по-моему, от этого не изменится.

Alexey Romanov в сообщении #223312 писал(а):

А зря. Потому что отличить $\forall n \in \mathbb{N}$ и арифметическое $\forall n$ без $\omega$-правила или какого-то его аналога у Вас не получится.

По-моему, мы в состоянии отличить символ $0$ (определённый в языке стандартной арифметики Пеано) от символа $\omega$, который там не определён.

Alexey Romanov в сообщении #223312 писал(а):

А вот доказательство

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

$(\forall n \in \mathbb{N})(A \vdash G(n))$,

в Вашей теории, как мне кажется, будет бесконечно длинным.

Поверьте, вполне конечное.
Но, конечно же, оно существенно мета-теоретическое (ибо привлекает индукцию по утверждениям о существовании доказательств $G(n)$).

Alexey Romanov в сообщении #223312 писал(а):

Жду обещанного куска статьи.

Увы, до понедельника. Ибо статья дома, куда я сегодня - завтра уже не попаду.

[Alexey Romanov]

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

Не добавляю никаких аксиом. Для доказательства $(\forall n \in \mathbb{N})(A \vdash G(n))$ нужно стандартное исчисление предикатов первого порядка + индукция по натуральным числам.

Для начала давайте договоримся о языке. Насколько я понимаю, мы рассматриваем язык арифметики первого порядка, с дополнительными предикатами $x \in \mathbb{N}$ ($x$ -- стандартное число) и $A \vdash p$ (арифметика доказывает $p$). Больше ничего нет.

Соответственно, я полагаю, что формулы вида $(\forall n \in \mathbb{N})(P(n))$ следует читать как сокращение $\forall n (n \in \mathbb{N} \rightarrow P(n))$.

Пока всё верно?

[epros]

Alexey Romanov в сообщении #223312 писал(а):

Жду обещанного куска статьи.

Вот здесь. Части статьи, не относящиеся к делу, я удалил.

Alexey Romanov в сообщении #223344 писал(а):

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

Не добавляю никаких аксиом. Для доказательства $(\forall n \in \mathbb{N})(A \vdash G(n))$ нужно стандартное исчисление предикатов первого порядка + индукция по натуральным числам.

Для начала давайте договоримся о языке. Насколько я понимаю, мы рассматриваем язык арифметики первого порядка, с дополнительными предикатами $x \in \mathbb{N}$ ($x$ -- стандартное число) и $A \vdash p$ (арифметика доказывает $p$). Больше ничего нет.

Соответственно, я полагаю, что формулы вида $(\forall n \in \mathbb{N})(P(n))$ следует читать как сокращение $\forall n (n \in \mathbb{N} \rightarrow P(n))$.

Пока всё верно?

Метатеория может использовать любой формальный язык, в котором в качестве предметных констант и переменных могут выступать формулы арифметики. Плюс к этому, она сама должна содержать арифметику (иначе невозможно использовать индукцию по натуральным числам). Т.е. натуральные числа - это тоже предметные переменые метатеории. Стало быть выражение $n \in \mathbb{N}$ означает, что рассматривается не любая предметная переменная, а именно натуральное число. Совершенно верно: "формулы вида $(\forall n \in \mathbb{N})(P(n))$ следует читать как сокращение $\forall n (n \in \mathbb{N} \rightarrow P(n))$".

[Alexey Romanov]

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

Стало быть выражение $n \in \mathbb{N}$ означает, что рассматривается не любая предметная переменная, а именно натуральное число.

То есть оно просто означает, что $n$ -- предметная переменная арифметики, а не тех областей, которые появляются в метатеории? А не что $n$ стандартное?

Даже если и нет, то мы имеем ($n$ -- предметная переменная арифметики):

1) $0 \in \mathbb{N}$
2) $\forall n ~ (n \in \mathbb{N} \to n+1 \in \mathbb{N})$
3) По аксиоме индукции из 1 и 2 выводится $\forall n ~ n \in \mathbb{N}$.

Так что $n \in \mathbb{N}$ не может означать "$n$ стандартно" без привлечения ресурсов существенно за пределами логики первого порядка (либо $\omega$-правила, либо логики второго порядка, либо чего-то ещё) и обязано быть равносильным "$n$ -- предметная переменная арифметики".

Согласны?

Есть, конечно, ещё вариант Робинсона: сказать
3') аксиома индукции распространяется только на формулы, не упоминающие предикат стандартности. Но это не поможет , потому что тогда индукции по стандартным числам нет.

-- Вс июн 21, 2009 23:55:19 --

Ага. Можно объяснить это намного проще.

Обозначим принцип рефлексии для $p$ ($(A \vdash p) \rightarrow p$) через $PR(p)$. Соответственно, метатеория, о которой идёт речь, будет $MA = A + \{ PR(p) ~|~ p$ -- предложение на языке $MA \}$.

Лемма 1: пусть $\mathcal M$ -- модель $A$. Чтобы расширить $\mathcal M$ на язык метатеории, положим $\mathcal M \vDash (A \vdash p) \iff A \vdash p$ (т.е. $A \vdash p$ истинно в модели $\mathcal M$ тогда и только тогда, когда $p$ действительно доказуемо в $A$). Эта расширенная $\mathcal M$ есть модель $MA$.

Доказательство: достаточно показать, что $\mathcal M \vDash PR(p)$ для всех $p$.

Предположим, что $\mathcal M \vDash (A \vdash p)$. Тогда действительно $A \vdash p$ и $\mathcal M \vDash p$. Q.E.D.


Теорема 2: $MA$ -- консервативное расширение $A$.

Доказательство: Возьмём любое предложение $p$ на языке $A$, такое что $A \nvdash p$. Тогда есть модель $A$ $\mathcal M$ такая, что $\mathcal M \nvDash p$. Но мы можем рассматривать $\mathcal M$ как модель $MA$ по лемме 1. Таким образом, невозможно $MA \vdash p$.


Следствие: Теорема Гудстейна недоказуема в $MA$.

Доказательство: возьмём теорему Гудстейна в качестве $p$ из теоремы 2.

-- Пн июн 22, 2009 00:01:38 --

Насчёт статьи -- в $MA$ нельзя формализовать уже первый шаг: "It's obvious, that for any given natural $k$ there is a formula of standard
first-order Peano arithmetic, that defines such a function."

[epros]

Alexey Romanov в сообщении #223844 писал(а):

Насчёт статьи -- в $MA$ нельзя формализовать уже первый шаг: "It's obvious, that for any given natural $k$ there is a formula of standard
first-order Peano arithmetic, that defines such a function."

Ваше замечание более чем удивительно, ибо речь идёт действительно об очевидных вещах. Упоминаемая функция $\Lambda$ - это всего лишь выражение типа $a^{b^c + d^e + \ldots} + \ldots$, где имеется в виду конечное количество слагаемых на каждом конечном "этаже" возведения в степень, и количество этих "этажей" $k$ тоже конечно. Там приведено рекурсивное определение для любого $k$ ("этажности"), начиная в единицы, так что при желании можно выписать формулу для $k=3$, $k=4$ и т.п. (если не лень).

Только не говорите мне, что возведение в степень неформализуемо в ПА. Этим фактом ещё Гёдель пользовался.

Alexey Romanov в сообщении #223844 писал(а):

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

Стало быть выражение $n \in \mathbb{N}$ означает, что рассматривается не любая предметная переменная, а именно натуральное число.

То есть оно просто означает, что $n$ -- предметная переменная арифметики, а не тех областей, которые появляются в метатеории? А не что $n$ стандартное?

Даже если и нет, то мы имеем ($n$ -- предметная переменная арифметики):

1) $0 \in \mathbb{N}$
2) $\forall n ~ (n \in \mathbb{N} \to n+1 \in \mathbb{N})$
3) По аксиоме индукции из 1 и 2 выводится $\forall n ~ n \in \mathbb{N}$.

Так что $n \in \mathbb{N}$ не может означать "$n$ стандартно" без привлечения ресурсов существенно за пределами логики первого порядка (либо $\omega$-правила, либо логики второго порядка, либо чего-то ещё) и обязано быть равносильным "$n$ -- предметная переменная арифметики".

Согласны?

Есть, конечно, ещё вариант Робинсона: сказать
3') аксиома индукции распространяется только на формулы, не упоминающие предикат стандартности. Но это не поможет , потому что тогда индукции по стандартным числам нет.

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

Как я уже говорил, на самом деле всё просто: Строка $0$ интерпретируется метатеорией как натуральное число, строка $S(0)$ - как натуральное число и т.д. Когда мы говорим о выражениях типа $(\forall n \in \mathbb{N})(A \vdash p(n))$, то имеется в виду, что в формулу арифметики $p(n)$ можно подставить вместо $n$ любое выражение вида $S(\ldots S(0)\ldots)$ и доказать то, что получилось.

По-моему, здесь по определению всё "стандартно".

[Alexey Romanov]

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

Как я уже говорил, на самом деле всё просто: Строка $0$ интерпретируется метатеорией как натуральное число, строка $S(0)$ - как натуральное число и т.д. Когда мы говорим о выражениях типа $(\forall n \in \mathbb{N})(A \vdash p(n))$, то имеется в виду, что в формулу арифметики $p(n)$ можно подставить вместо $n$ любое выражение вида $S(\ldots S(0)\ldots)$ и доказать то, что получилось.

Блин. Это и есть $\omega$-правило.

Xaositect в сообщении #223259 писал(а):

Как я понимаю.
Оно означает, что $\forall n\ p(n)$ является теоремой, если теоремами являются все формулы $p(i)$, полученные подстановкой нумералов в $p(n)$ вместо $n$.

В логике первого порядка это невозможно, потому что

Цитата:

любое выражение вида $S(\ldots S(0)\ldots)$

выразить нельзя.

[epros]

Alexey Romanov в сообщении #223913 писал(а):

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

Как я уже говорил, на самом деле всё просто: Строка $0$ интерпретируется метатеорией как натуральное число, строка $S(0)$ - как натуральное число и т.д. Когда мы говорим о выражениях типа $(\forall n \in \mathbb{N})(A \vdash p(n))$, то имеется в виду, что в формулу арифметики $p(n)$ можно подставить вместо $n$ любое выражение вида $S(\ldots S(0)\ldots)$ и доказать то, что получилось.

Блин. Это и есть $\omega$-правило.

Ох уж мне эти теоретико-множественные прибабахи... Оказывается, чтобы сказать, что натуральное число - это не фиг знает что такое, а именно определённая арифметикой константа (т.е. выражение вида $S(\ldots S(0)\ldots)$) нам нужно специальное правило...

Alexey Romanov в сообщении #223913 писал(а):

В логике первого порядка это невозможно, потому что

Цитата:

любое выражение вида $S(\ldots S(0)\ldots)$

выразить нельзя.

Ну и ну.

А Вы, часом, не забыли, что речь идёт о метатеории, одно из назначений которой (я бы сказал - главное) заключается в том, чтобы определять алфавит и синтаксис предметной теории? Поэтому утверждение: "Рассматриваемая строка символов является выражением вида $S(\ldots S(0)\ldots)$)", является формализуемым в этой метатеории с помощью примитивно-рекурсивной функции - части аналитической грамматики предметного языка?

Или Вы хотели сказать, что примитивно-рекурсивные функции, которыми определяется грамматика предметного языка, нельзя определить в классическом исчислении предикатов первого порядка?

[Alexey Romanov]

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

Ох уж мне эти теоретико-множественные прибабахи... Оказывается, чтобы сказать, что натуральное число - это не фиг знает что такое, а именно определённая арифметикой константа (т.е. выражение вида $S(\ldots S(0)\ldots)$) нам нужно специальное правило...

Это не "теоретико-множественные прибабахи". Это просто недостаточная выразительность логики первого порядка, о чём ясно сказано в той самой статье. Чтобы сказать, что кроме этих констант никаких других чисел нет, нам нужно сделать одно из следующего
1) перечислить все эти константы в одной формуле $\forall n ~ n = 0 \vee n = S(0) \vee n = S(S(0)) \vee ... . Для этого нужна инфинитарная логика.
2) сказать, что достаточно формулу доказать для всех этих констант. Это $\omega$-правило.
3) сказать, что мы рассматриваем наименьшую модель арифметики. Это либо теория множеств, либо логика второго порядка.

Если бы мы могли сказать "натуральное число - это не фиг знает что такое, а именно определённая арифметикой константа" в $MA$, то она имела бы единственную модель и (поскольку она рекурсивно аксиоматизируема) была бы полна.

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

А Вы, часом, не забыли, что речь идёт о метатеории, одно из назначений которой (я бы сказал - главное) заключается в том, чтобы определять алфавит и синтаксис предметной теории? Поэтому утверждение: "Рассматриваемая строка символов является выражением вида $S(\ldots S(0)\ldots)$)", является формализуемым в этой метатеории с помощью примитивно-рекурсивной функции - части аналитической грамматики предметного языка?

Будем использовать $n$ для переменной по числам, $\sigma$ для переменной по строкам, ++ -- операция приписывания. Разумеется, мы можем определить формулу метатеории $Repr(n, \sigma)$ такую, что

$Repr(0, \sigma) \leftrightarrow \sigma = ``0``$

$Repr(n+1, ``S(`` + \! + \sigma + \! + ``)``) \leftrightarrow Repr(n, \sigma)$

Беда в том, что мы теперь легко можем доказать $\forall n ~ \exists ! \sigma ~ Repr(n, \sigma)$. То есть в тех моделях, где есть нестандартные числа, они вполне будут представляться выражением вида $S(\ldots S(0)\ldots)$) -- вот только с нестандартным количеством $S$.

[epros]

Alexey Romanov в сообщении #223934 писал(а):

Это не "теоретико-множественные прибабахи". Это просто недостаточная выразительность логики первого порядка, о чём ясно сказано в той самой статье.

Я не знаю что Вы хотите сказать, утверждая, что логика первого порядка "недостаточно выразительна". Я говорю о метатеории, которая определяет алфавит и синтаксис арифметики Пеано. Она достаточно выразительна для этого и может быть записана вся целиком в исчислении предикатов первого порядка.

Alexey Romanov в сообщении #223934 писал(а):

Чтобы сказать, что кроме этих констант никаких других чисел нет, нам нужно сделать одно из следующего
1) перечислить все эти константы в одной формуле $\forall n ~ n = 0 \vee n = S(0) \vee n = S(S(0)) \vee ...$ . Для этого нужна инфинитарная логика.

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

Нам нужно всего лишь рекурсивно определить предикат "является натуральным числом":
1. $(\forall x)(x \in \mathbb{N} \rightarrow
2. $

Здесь я специально поставил кавычки, чтобы было видно, что речь идёт о строковых константах. Точка - это операция конкатенации. Соответственно $x$ - строковая переменная. Хотите я Вам данную аналитическую грамматику напишу в виде исполнимой процедуры в Си? Впрочем, не буду: при желании сами напишете.

Alexey Romanov в сообщении #223934 писал(а):

Если бы мы могли сказать "натуральное число - это не фиг знает что такое, а именно определённая арифметикой константа" в $MA$, то она имела бы единственную модель и (поскольку она рекурсивно аксиоматизируема) была бы полна.

Я не совсем понял, что именно Вы понимаете под $MA$. Судя по всему, ту же арифметику, но расширенную схемой аксиом "принципа рефлексии", т.е. алфавит и синтаксис языка Вы не трогаете. А зря. Я говорю о метатеории, которая определяет алфавит и синтаксис языка арифметики. Естественно, у неё самой язык богаче.

О "моделях" же я вообще не желаю слышать как о сугубо теоретико-множественном прибабахе.

Alexey Romanov в сообщении #223934 писал(а):

вот только с нестандартным количеством $S$.

Ну и ну, совсем Вы заморочены этими "моделями"... Впору мне изобразить:

Не бывает строк символов, в которых находилось бы "нестандартное количество" $S$.

Может быть у Вас в каких-то фантастических теориях бывают бесконечные строки. А в Вашей "инфинитарной логике" может быть даже доказывается, что такие фантастические теории "существуют". Но никто таковой теории пока что реально на бумаге не видел. Поэтому я исхожу из стандартного исчисления предикатов, согласно которому любая константа, переменная или формула представляет собой конечную строку. Так что и метатеория формулирует утверждения исключительно относительно конечных строк.