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

[georg38]

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

[man]

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

Зато эта аксиома прекрасным образом формализуется в метатеории:
$\forall n ~ (n=0 \vee (\exists m ~ \mathfrak{N}(m) \wedge m+1=n)) \leftrightarrow \mathfrak{N}(n)$
Здесь $\mathfrak{N}$ - предикатный символ, определённый в языке метатеории, который призван обозначать "принадлежность к натуральным числам". Как видите, это - формула стандартного исчисления предикатов первого порядка.

Если бы это была формула теории, то есть подозрение, что в $ скрывается предикатная переменная неэлементарного языка, т.е. свойство индивидных переменных, а не она сама, в частности свойство интервалов между натуральными числами быть равными. Если заменить $ на $S(m)$ можно предъявить неизоморфную $\mathbb {N}$ структуру линейного порядка с непостоянными интервалами. В этом смысле расширение алфавита было бы не консервативным, но т.к. это метатеория, объектами которой являются строки (термы), это ограничение заложено в синтаксисе. Я Вас правильно понял ?

[Someone]

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

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

Раз уж Вам физические ограничения непонятны, давайте проверим на опыте. Архимед в своё время придумал систему записи очень больших чисел и показал, как с её помощью записывается число $10^{8\cdot 10^{16}}$. Предлагаю Вам изобразить его чёрточками на бумаге. Когда закончите, приходите с этой бумагой ко мне.

И что мы таким образом "проверим на опыте"? Я заранее знаю в какое ограничение мы упрёмся - в ограниченность моей мотивации. И что это доказывает? Это "ограничение" не имеет принципиального характера и может быть преодолено.

Вот и преодолейте. Тем более, что это не физическое препятствие, а психологическое. И посмотрим, что из этого выйдет.

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

И что мы таким образом "проверим на опыте"?

Как что? Что каждую строку чёрточек на листе бумаги, содержащую менее $10^{80000000000000000}$ чёрточек, можно продолжить, приписав ещё одну чёрточку. Это даст нам "непосредственную" проверку одной из аксиом Пеано до этого же числа. Вы же утверждали, что такая проверка возможна. Правда, Вы уже один раз, как будто, согласились со мной, что практическая проверка аксиом Пеано за конечное время невозможна, поэтому их нужно принимать или не принимать без проверки. Теперь Вы хотите взять свои слова назад?

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

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

Если все препятствия преодолимы, то преодолейте их и продемонстрируйте мне $10^{80000000000000000}$ чёрточек, нарисованных на бумаге.

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

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

По моим понятиям - изображали ранее и продолжаете изображать. И не только в этом вопросе.

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

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

Ранее Вы заявляли, что это не теория множеств, но против арифметики не возражали:

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

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

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

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

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

Теперь же заявляете, что это и не арифметика. В таком случае предъявите полный список аксиом своей MT. Доказательство неизвестно в какой теории никого не устроит. О теореме Гудстейна чётко утверждается, что она недоказуема в арифметике Пеано и доказуема в ZF (или другой аналогичной теории множеств), а также в арифметике второго порядка. Но арифметика второго порядка содержит достаточно большой фрагмент теории множеств (например, совокупность всех подмножеств натурального ряда).

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

А мне такой факт неизвестен.

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

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

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

Ну, у меня мотивация поиска ошибок в Вашем доказательстве не больше, чем у Вас - мотивация рисования $10^{80000000000000000}$ чёрточек.

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

Боже мой, какой ужас!

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

Кто это Вам сказал, что такого предиката нет? Есть, и очень простой: $n=n$. Именно потому, что всё, о чём говорит арифметика Пеано, не только "обычно", но и всегда по определению является натуральным числом. Не предусмотрены там совсем другие средства. А именно, средства для выражения понятия "любое множество натуральных чисел".

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

Зато эта аксиома прекрасным образом формализуется в метатеории:
$\forall n ~ (n=0 \vee (\exists m ~ \mathfrak{N}(m) \wedge m+1=n)) \leftrightarrow \mathfrak{N}(n)$
Здесь $\mathfrak{N}$ - предикатный символ, определённый в языке метатеории, который призван обозначать "принадлежность к натуральным числам". Как видите, это - формула стандартного исчисления предикатов первого порядка.

Идиотствуете? Какое это имеет отношение к аксиоме АП?

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

АП. Каждое множество натуральных чисел, которое
1) содержит число $1$ (или $0$, если мы хотим начинать натуральный ряд с $0$) и
2) вместе с каждым натуральным числом $n$ содержит и число $n+1$,
содержит все натуральные числа.

Ваша "формализация" сформулирована для одного множества, а именно - для множества всех натуральных чисел. Потому что и $n=0 \vee (\exists m ~ \mathfrak{N}(m) \wedge m+1=n)$, и $\mathfrak{N}(n)$ выполняются для всех натуральных чисел - как стандартных, так и нестандартных.

[epros]

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

Вот и преодолейте. Тем более, что это не физическое препятствие, а психологическое. И посмотрим, что из этого выйдет.

Не имею достаточной мотивации.

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

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

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

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

Ранее Вы заявляли, что это не теория множеств, но против арифметики не возражали:
...
Теперь же заявляете, что это и не арифметика.

Я не говорил, что MT является арифметикой!! Я сказал, что она содержит арифметику, поскольку использует индукцию по натуральным числам. Но никакого "достаточно большого фрагмента теории множеств" она не содержит, в чём легко может убедиться любой вменяемый субъект, прочитавший доказательство.

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

В таком случае предъявите полный список аксиом своей MT. Доказательство неизвестно в какой теории никого не устроит.

Не говорите ерунды. Ни одно математическое доказательство не выполняется абсолютно формально, ибо это непосильный мартышкин труд. Если доказательство окажется неформализуемым, любому критику не составит труда указать в каком месте. По этой же причине нет необходимости полностью формально описывать язык и аксиоматику используемой теории - ибо вменяемому читателю это и так очевидно. Даже для тех, кто не желает читать (вроде Вас), я уже сказал всё, что нужно: что доказательство может быть формализовано в стандартном исчислении предикатов плюс индукция по натуральным числам. Для особо сомневающихся я также объяснил, что в MT понимается под "натуральным числом": это терм вида $0+1+ \dots +1$ (очевидно, раз MT определяет язык арифметики Пеано, она определяет и что такое "терм").

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

О теореме Гудстейна чётко утверждается, что она недоказуема в арифметике Пеано и доказуема в ZF

Я не собираюсь оспаривать ни того, ни другого.

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

Я уже объяснял Вам, что Ваше нежелание признавать известные факты никакой роли не играет.

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

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

Ну, у меня мотивация поиска ошибок в Вашем доказательстве не больше, чем у Вас - мотивация рисования $10^{80000000000000000}$ чёрточек.

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

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

Кто это Вам сказал, что такого предиката нет? Есть, и очень простой: $n=n$.

Смеётесь? Покажите здесь предикатный символ, интерпретируемый как "является натуральным числом".

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

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

Зато эта аксиома прекрасным образом формализуется в метатеории:
$\forall n ~ (n=0 \vee (\exists m ~ \mathfrak{N}(m) \wedge m+1=n)) \leftrightarrow \mathfrak{N}(n)$
Здесь $\mathfrak{N}$ - предикатный символ, определённый в языке метатеории, который призван обозначать "принадлежность к натуральным числам". Как видите, это - формула стандартного исчисления предикатов первого порядка.

Идиотствуете? Какое это имеет отношение к аксиоме АП?

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

Для прикидывающихся непонятливыми разберём по буквам:
Вы употребили понятие "множество натуральных чисел". Допустим, это такая вот штука:
$\mathbb{N} := \{n ~ : ~ \mathfrak{N}(n) \}$
Здесь предикатный символ $\mathfrak{N}$ выражает принадлежность соответствующего объекта к натуральным числам (очевидно, теория может допускать существование и другого рода объектов).
Согласно Вашему пункту 1) $\mathbb{N}$ должно содержать $0$: $\mathfrak{N}(0)$.
Согласно Вашему пункту 2) $\forall m~ \mathfrak{N}(m) \rightarrow \mathfrak{N}(m+1)$.
Согласно последней строчке Вашей формулировки условия 1) и 2) являются необходимыми и достаточными для определения принадлежности объекта ($n$) к натуральным числам ($\mathfrak{N}(n)$). Осталось только записать всё это одной формулой...

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

Ваша "формализация" сформулирована для одного множества, а именно - для множества всех натуральных чисел. Потому что и $n=0 \vee (\exists m ~ \mathfrak{N}(m) \wedge m+1=n)$, и $\mathfrak{N}(n)$ выполняются для всех натуральных чисел - как стандартных, так и нестандартных.

Неужели? И что же моя формализация допускает такого, что исключено Вашей словесной формулировкой?

Хочу обратить Ваше внимание, что моя формула является всего лишь рекурсивным определением предиката $\mathfrak{N}(n)$. В частности, если понимать выражение $m+1$ как: "К строке $m$ добавить в конце строку $+1$", то мы получим рекурсивное определение предиката: "Строка $n$ является термом вида $0+1+ \dots +1$".

[Someone]

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

Не имею достаточной мотивации.

То есть, Вы сами прекрасно понимаете, что данное предприятие неосуществимо. Но не хотите этого признавать.

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

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

С точки зрения математика, "проверка" в Вашем смысле вообще проверкой не является. И эту "проверку" Вы всё время пытаетесь выдавать за "железное обоснование" конструктивизма.

Ситуация с "обоснованностью", например, у интуиционистской арифметики (а с ней и у CRA, который, по утверждению Трулстры, есть интуиционистская арифметика с двумя дополнительными схемами аксиом; А.С.Трулстра, Аспекты конструктивной математики, Справочная книга по математической логике, Часть IV, Теория доказательств и конструктивная математика, "Наука", Москва, 1983, пункт 4.13) нисколько не лучше, чем у классической. Дело в том, что существует перевод формул классической арифметики на язык интуиционистской, при котором, если исходное утверждение доказуемо в классической арифметике, то переведённое утверждение доказуемо в интуиционистской арифметике (кроме того, переведённое утверждение при классической интерпретации равносильно исходному; Стефен К.Клини, Введение в метаматематику, "Иностранная литература", Москва, 1957, Часть IV, Гдава V, § 81), в то время как перевод в обратном направлении невозможен. Поэтому из непротиворечивости интуиционистской арифметики следует непротиворечивость классической, но обратного утверждения нет.

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

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

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

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

Даже для тех, кто не желает читать (вроде Вас), я уже сказал всё, что нужно: что доказательство может быть формализовано в стандартном исчислении предикатов плюс индукция по натуральным числам.

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

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

Для особо сомневающихся я также объяснил, что в MT понимается под "натуральным числом": это терм вида $0+1+ \dots +1$ (очевидно, раз MT определяет язык арифметики Пеано, она определяет и что такое "терм").

Я помню. Я ещё объяснял Вам, что эти термы образуют модель теории T, изоморфную натуральному ряду теории MT.

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

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

Ну почему "невесть что"? Это опубликовано 27 лет назад (Laurie Kirby and Jeff Paris, Accessible independence results for Peano arithmetic, Bull. London Math. Soc, 14 (1982), 285-293), и с тех пор никто не заявлял, что в работе есть ошибки. Если Вы не желаете признавать факты, то боюсь, что Вы останетесь в гордом одиночестве. Обратите внимание, что уже все Ваши собеседники, кроме меня, Вас покинули. Я тоже Вас покину.

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

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

Кто это Вам сказал, что такого предиката нет? Есть, и очень простой: $n=n$.

Смеётесь? Покажите здесь предикатный символ, интерпретируемый как "является натуральным числом".

Дался Вам этот "символ"... Ну давайте обозначим его $\mathfrak K$.

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

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

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

Зато эта аксиома прекрасным образом формализуется в метатеории:
$\forall n ~ (n=0 \vee (\exists m ~ \mathfrak{N}(m) \wedge m+1=n)) \leftrightarrow \mathfrak{N}(n)$
Здесь $\mathfrak{N}$ - предикатный символ, определённый в языке метатеории, который призван обозначать "принадлежность к натуральным числам". Как видите, это - формула стандартного исчисления предикатов первого порядка.

Идиотствуете? Какое это имеет отношение к аксиоме АП?

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

Позволяю. Но не прикидываюсь. Это моё естественное состояние.

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

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

Совершенно не то же самое.

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

Для прикидывающихся непонятливыми разберём по буквам:
Вы употребили понятие "множество натуральных чисел". Допустим, это такая вот штука:
$\mathbb{N} := \{n ~ : ~ \mathfrak{N}(n) \}$
Здесь предикатный символ $\mathfrak{N}$ выражает принадлежность соответствующего объекта к натуральным числам (очевидно, теория может допускать существование и другого рода объектов).

Не "допустим". У меня сказано: "каждое множество натуральных чисел". Что, по Вашему мнению, здесь делает слово "каждое"? Здесь речь идёт не о $\mathbb N$, а о произвольном множестве $X$, удовлетворяющем условию $\forall n(n\in X\to \mathfrak N(n))$.
Стандартно аксиома АП "формализуется" так:
$\forall X(X\subseteq\mathbb N\to(0\in X\wedge\forall n(n\in X\to n+1\in X)\to X=\mathbb N))$.

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

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

Ваша "формализация" сформулирована для одного множества, а именно - для множества всех натуральных чисел. Потому что и $n=0 \vee (\exists m ~ \mathfrak{N}(m) \wedge m+1=n)$, и $\mathfrak{N}(n)$ выполняются для всех натуральных чисел - как стандартных, так и нестандартных.

Неужели? И что же моя формализация допускает такого, что исключено Вашей словесной формулировкой?

Ваша "формализация" допускает существование такого множества $X\subseteq\mathbb N$, которое удовлетворяет условию $0\in X\wedge\forall n(n\in X\to n+1\in X)$, но не совпадает с $\mathbb N$. Из-за того, что это множество $X$ нельзя определить формулой языка арифметики Пеано, аксиомы индукции для него не работают. Собственно говоря, из-за этого и появляются нестандартные модели.

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

Хочу обратить Ваше внимание, что моя формула является всего лишь рекурсивным определением предиката $\mathfrak{N}(n)$.

Вот именно.

Ладно, перейдём к Вашему "доказательству".
Прежде всего, мне непонятны основания для Ваших индуктивных переходов. Я понимаю, что Вам они кажутся очевидными, но для меня это не так. В частности, странно вот это:

epros писал(а):

Let's consider the number $x+1=\Lambda_{m+2}(n,m_1,\ldots,m_{m+2}+1)$. If $x+1=g_{n-1}(y)$, then for the next step of Goodstein's sequence we will have:

$$g_n(y)=\mathop{\mathrm{Subs}}\nolimits^{n+1}_n (x)=\Lambda_{m+2}(n+1,m_1,\ldots,m_{m+2})\text{.}$$

Определяя функции $\Lambda_k$, Вы писали, что $0\leqslant m_k\leqslant(n-1)n^{\Lambda_{k-1}(n,m1,\ldots,m_{k-1})}$. Но тогда преобразование $\mathop{\mathrm{Subs}}\nolimits^{n+1}_n$ должно применяться и к $m_k$, чего у Вас нет. А если это преобразование применять, то $m_k$ растёт, и индуктивного перехода не получается.

Вы считаете, что импликация

epros писал(а):

$\forall nZ_n(\Lambda_{m+2}(n,2,0,\ldots,0))\to\forall nZ_n(\Lambda_{m+3}(n,2,0,\ldots,0))$

верна? Как я понимаю,

$$\Lambda_{m+2}(n,2,0,\ldots,0)=2^{2^{.^{.^{.^2}}}}\text{,}$$

где количество "двоек" равно $m+2$. В указанной выше статье Kirby и Paris'а число именно такого вида (с нестандартным числом "двоек") служит контрпримером к теореме Гудстейна.

epros писал(а):

And because for any natural $x$ there is such an $r$, that $x<\Lambda_{r+2}(2,2,0\ldots,0)$, we can assert for any given natural $x$ that proposition $\exists k(g_k(x)=0)$ is provable in atrithmetic. Or in single common meta-theoretical assertion:

$$\forall x\in\mathbb N(A\vdash\exists k(g_k(x)=0))\text{.}$$

But it doesn't mean, that Goodstein's theorem is proven in arithmetic. Such an assertion:

$$A\vdash\forall x\exists k(g_k(x)=0)\text{,}$$

that was proven in [4], doesn't contradict this result. That's because quantification "for any $x$" claims induction over collections of arithmetic formulas, that is possible only in meta-theory.

Противоречит, причём, противоречие получается несколькими способами.
1) Как я уже говорил, модель теории T, составленная из указанных Вами термов, изоморфна натуральному ряду метатеории MT, поэтому, доказывая теорему Гудстейна для T, метатеория MT доказывает её и для себя.
2) Мы можем поручить роль метатеории арифметике T, формализовав в ней арифметику Пеано T' и доказав теорему Гудстейна для T'. Как отмечено в пункте 1), тем самым мы докажем теорему и для T.
3) Ваше утверждение о "коллекции арифметических формул" поверхностно. Вся проблема сводится к тому, что функции $\Lambda_k$ имеют разное число аргументов. Эту проблему очень легко обойти, используя (обще)рекурсивную нумерацию конечных последовательностей натуральных чисел, для которой существуют (обще)рекурсивные функции, восстанавливающие эту последовательность по её коду. Такие нумерации известны, пример Вы можете найти в литературе (например: Б.А.Кушнер, Лекции по конструктивному математическому анализу, "Наука", Москва, 1973, глава 1, § 3, пункт 1). Пользуясь этими алгоритмами, легко упаковать $k,n,m_1,m_2,\ldots,m_k$ в одно натуральное число и превратить Ваши функции $\Lambda_k$ в одну функцию одной переменной.

[epros]

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

То есть, Вы сами прекрасно понимаете, что данное предприятие неосуществимо. Но не хотите этого признавать.

На самом деле не имеет значения, считаю ли я это предприятие осуществимым. В любом случае отстутствие мотивации - конкретное препятствие для его осуществления. Но если бы мне, например, платили по доллару за каждую чёрточку, то, возможно, я бы им занялся не смотря ни на какие соображения об "осуществимости".

Точно таже и с любыми другими конкретными препятствиями, которые могут возникнуть: Не исключено, что мы придумаем способы их преодолеть.

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

С точки зрения математика, "проверка" в Вашем смысле вообще проверкой не является. И эту "проверку" Вы всё время пытаетесь выдавать за "железное обоснование" конструктивизма.

Если быть точным, за "обоснование" я пытаюсь выдать не "проверку" (конкретный результат конкретных действий), а "проверяемость". Т.е. с моей точки зрения "обоснованием" является существование способов проверки.

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

Видите ли, что бы я ни говорил, я всё-таки читал Ваше сочинение. И не заметил там никаких дополнительных аксиом, которые бы Вы использовали. Если Вы их использовали, Вы обязаны были это явно указать.

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

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

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

Во-первых, касательно использования знаков сложения и умножения: MT рассматривает знак сложения только как часть терма арифметики $0+1+ \dots +1$, самой ей такая операция не нужна. Я бы сказал, что ей нужна операция конкатенации строк (а как же без неё в теории, определяющей формальный язык?). Например, аксиому индукции по некой формуле $PA \vdash \varphi(n)$ в ней можно записать так:
$(PA \vdash \varphi(
$\forall n ~ n \in \mathbb{N} \rightarrow PA \vdash \varphi(n)$
Здесь точка обозначает конкатенацию строк, а выражение $n \in \mathbb{N}$ означает утверждение, что $n$ является строкой вида $0+1+ \dots +1$.
Так что использование индукции я не отрицаю. Но полный объём арифметики со всеми её операциями тут вряд ли нужен.

Во-вторых, мне не очевидно, что такая теория "это и есть арифметика Пеано".

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

Ну почему "невесть что"? Это опубликовано 27 лет назад (Laurie Kirby and Jeff Paris, Accessible independence results for Peano arithmetic, Bull. London Math. Soc, 14 (1982), 285-293), и с тех пор никто не заявлял, что в работе есть ошибки.

Я не оспариваю результаты Laurie Kirby and Jeff Paris, я сомневаюсь в Вашем утверждении, что MT - это арифметика, а поэтому всё доказанное в ней автоматически оказывается доказанным в арифметике.

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

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

Позвольте не обращать внимание на эту сентенцию. У собеседников могут быть разные мотивы, чтобы не участвовать в обсуждении. Кого-то вопрос может быть просто не интересует, кому-то просто лень разбираться. Я никому не собираюсь навязываться.

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

Дался Вам этот "символ"... Ну давайте обозначим его $\mathfrak K$.

Можно, конечно, доопределить. Только:
А) Это будет уже не арифметика Пеано.
Б) Это не имеет отношения к формуле арифметики Пеано $n=n$.

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

Совершенно не то же самое.
...
У меня сказано: "каждое множество натуральных чисел". Что, по Вашему мнению, здесь делает слово "каждое"? Здесь речь идёт не о $\mathbb N$, а о произвольном множестве $X$, удовлетворяющем условию $\forall n(n\in X\to \mathfrak N(n))$.
Стандартно аксиома АП "формализуется" так:
$\forall X(X\subseteq\mathbb N\to(0\in X\wedge\forall n(n\in X\to n+1\in X)\to X=\mathbb N))$.

Ладно, принимаю Вашу формализацию.
Разумеется она не записывается в арифметике первого порядка. Причины две:
1) Использованы обозначения теории множеств, которых нет в арифметике. Это легко обходится заменой $n\in X$ на $\mathfrak{X}(n)$.
2) Множество $X$ стоит под квантором. Когда мы заменяем $X$ на предикатный символ $\mathfrak{X}$, мы лишаемся возможности ставить его под квантор (по правилам логики первого порядка). Это можно обойти за счёт того, что формула записывается не в предметной теории, а в метатеории: Мы можем сказать: "Для любой формулы $\varphi$ предметной теории является теоремой, что ...".

Так что всё это прекрасно формализуется в метатеории в языке исчисления предикатов первого порядка.

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

Ваша "формализация" допускает существование такого множества $X\subseteq\mathbb N$, которое удовлетворяет условию $0\in X\wedge\forall n(n\in X\to n+1\in X)$, но не совпадает с $\mathbb N$. Из-за того, что это множество $X$ нельзя определить формулой языка арифметики Пеано, аксиомы индукции для него не работают. Собственно говоря, из-за этого и появляются нестандартные модели.

Указанное мной рекурсивное определение предиката $\mathfrak{N}$ тоже нельзя определить формулой языка арифметики Пеано, поскольку оно использует не определённый в языке предикатный символ.

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

Определяя функции $\Lambda_k$, Вы писали, что $0\leqslant m_k\leqslant(n-1)n^{\Lambda_{k-1}(n,m1,\ldots,m_{k-1})}$. Но тогда преобразование $\mathop{\mathrm{Subs}}\nolimits^{n+1}_n$ должно применяться и к $m_k$, чего у Вас нет. А если это преобразование применять, то $m_k$ растёт, и индуктивного перехода не получается.

Ура! Наконец-то Вы решили снизойти до конкретных замечаний к доказательству. Отвечаю:

Область определения для переменной $m_k$ действительно растёт с увеличением $n$, но это совершенно не означает, что что-либо происходит с конкретным значением этой переменной. Поясняю на конкретном примере. Допустим, на 5-ом шаге элемент последовательности имеет вид:
$x=4+5^{3+5^{2}+5^{1+5}}$
Здесь $m_1=1$, $m_2=1$, $m_3=3+5^{2}$, $m_4=4$.
Рассмотрим число, на единицу большее:
$x+1=5+5^{3+5^{2}+5^{1+5}}$
На следующем щаге последовательности Гудстейна произойдёт следующее:
1) Из числа $x+1$ вычтется единица.
2) Все пятёрки заменятся на шестёрки.
Получим:
$4+6^{3+6^{2}+6^{1+6}}$
Итак, получили число того же вида, что и $x$, но только с основанием разложения на единицу больше (6 вместо 5), что и утверждается в процитированном Вами отрывке.

Обратите внимание, что граница области определения $m_4$ (последней переменной функции $\Lambda_{m+2}$) не имеет никакого значения. Пример специально подобран таким образом, чтобы Вы видели, что даже если то единственное слагаемое в разложении $x$, которое меньше $n$, при увеличении его на единицу оказывается равным $n$, всё равно утверждение оказывается верным.

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

Вы считаете, что импликация

epros писал(а):

$\forall nZ_n(\Lambda_{m+2}(n,2,0,\ldots,0))\to\forall nZ_n(\Lambda_{m+3}(n,2,0,\ldots,0))$

верна? Как я понимаю,

$$\Lambda_{m+2}(n,2,0,\ldots,0)=2^{2^{.^{.^{.^2}}}}\text{,}$$

где количество "двоек" равно $m+2$. В указанной выше статье Kirby и Paris'а число именно такого вида (с нестандартным числом "двоек") служит контрпримером к теореме Гудстейна.

Да, только Вы забыли подставить $n=2$:

$$\Lambda_{m+2}(2,2,0,\ldots,0)=2^{2^{.^{.^{.^2}}}}\text{,}$$

Импликацию я считаю верной потому, что к этому ведёт цепочка рассуждений по индукции.

Про "нестандартное число двоек" даже и не знаю что сказать... Очевидно, что последний шаг моего доказательства применим только для "стандартного числа двоек". Как Вы наверное уже поняли логику моего доказательства, я попытался просто "в лоб" продемонстрировать, что "этажность" представления числа за конечное количество шагов уменьшается (что она не увеличивается - очевидно). Собственно, указанная Вами импликация примерно это и утверждает: что если число такой-то "этажности" обнулится за конечное количество шагов, то и число на единицу большей "этажности" обнулится за конечное количество шагов.

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

[Someone]

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

Но если бы мне, например, платили по доллару за каждую чёрточку, то, возможно, я бы им занялся не смотря ни на какие соображения об "осуществимости".

Даже если бы Вам сказали, что заплатят только всю сумму сразу после окончания работы?

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

Если быть точным, за "обоснование" я пытаюсь выдать не "проверку" (конкретный результат конкретных действий), а "проверяемость". Т.е. с моей точки зрения "обоснованием" является существование способов проверки.

То есть, потенциально, затратив бесконечное количество материальных и временных ресурсов? В таком смысле "проверить" можно и аксиому бесконечности.

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

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

Видите ли, Вы заявляли:

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

Я не говорил, что MT является арифметикой!! Я сказал, что она содержит арифметику

Собственно говоря, поэтому у меня возник вопрос, какие дополнительные аксиомы Вы используете. Как я уже говорил, в такой ситуации Вы обязаны формулировать все дополнительные предположения явно.

Теперь Вы уже заявляете, что MT не содержит арифметику. Может, на чём-то определённом остановимся? На самом деле этот наш спор не имеет абсолютно никакого значения. Пусть Вы используете в качестве MT Бог знает что. Но я же вижу, что Вы делаете. Я возьму в качестве MT арифметику Пеано, кодируя символы и строки натуральными числами, продублирую в ней Ваши построения и, если в них всё в порядке, докажу теорему Гудстейна для MT, делая при этом вид, что доказываю её для T. Какие препятствия у меня возникнут?

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

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

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

Кто это Вам сказал, что такого предиката нет? Есть, и очень простой: $n=n$.

Смеётесь? Покажите здесь предикатный символ, интерпретируемый как "является натуральным числом".

Дался Вам этот "символ"... Ну давайте обозначим его $\mathfrak K$.

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

Можно, конечно, доопределить. Только:
А) Это будет уже не арифметика Пеано.
Б) Это не имеет отношения к формуле арифметики Пеано $n=n$.

Ну, очевидно, Вы не знаете, что такое предикат. Читаем (Стефен К.Клини, Введение в метаматематику, "Иностранная литература", Москва, 1957, Часть II, Глава VII, § 31):

Цитата:

Аналогично любая формула арифметической системы может интерпретироваться как выражающая некоторый предикат при обычном арифметическом значении символов. Например, $\exists c(a=0''\cdot c)$ выражает $E(a)$, или $a$ четно, $a=b$ выражает $a=b$, а $\exists b(c'+a=b)$ (сокращенно $a<b$, см. § 17) выражает $a<b$.

Так вот, предикат $\mathfrak K(n)$ выражается арифметической формулой $n=n$. Совершенно очевидно, что добавление символа $\mathfrak K$ в язык арифметики ничего нового в арифметику не вносит, даже если забыть, что этот предикат тривиален.

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

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

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

мне не очевидно, что такая теория "это и есть арифметика Пеано".

А откуда возьмутся натуральные числа, если не будет арифметики?
И что я могу сделать, если Вы не знаете, что такое арифметика Пеано? Только сказать, что арифметика Пеано - это исчисление предикатов с равенством плюс аксиомы Пеано (с операциями сложения и умножения и аксиомами для них). А теория множеств ZFC - это исчисление предикатов с равенством плюс аксиомы ZFC. И так далее. Разумеется, я не хочу сказать, что всякая формальная теория должна включать исчисление предикатов.

Кстати, если у Вас MT - более слабая теория, чем арифметика Пеано, то у неё нестандартных моделей ещё больше, и не факт, что Вы сможете средствами MT построить модель арифметики, чтобы доказать в этой модели теорему Гудстейна. И, наконец, мне трудно понять, что делает в Вашем рассуждении метатеория, и почему это рассуждение не проходит в самой теории T.

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

Ладно, принимаю Вашу формализацию.

Это не моя формализация. Это стандартное понимание данной аксиомы.

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

Разумеется она не записывается в арифметике первого порядка. Причины две:
1) Использованы обозначения теории множеств, которых нет в арифметике. Это легко обходится заменой $n\in X$ на $\mathfrak{X}(n)$.
2) Множество $X$ стоит под квантором. Когда мы заменяем $X$ на предикатный символ $\mathfrak{X}$, мы лишаемся возможности ставить его под квантор (по правилам логики первого порядка). Это можно обойти за счёт того, что формула записывается не в предметной теории, а в метатеории: Мы можем сказать: "Для любой формулы $\varphi$ предметной теории является теоремой, что ...".

Так что всё это прекрасно формализуется в метатеории в языке исчисления предикатов первого порядка.

Нет. Мы, конечно, можем вместо "множество" говорить "свойство", "предикат" или ещё что-нибудь, но обойти квантор $\forall X$ не удастся. Как только Вы замените этот квантор каким-то списком аксиом, категоричность сразу пропадёт, и появятся нестандартные модели. Это следует из теоремы компактности.

А причём тут метатеория - совсем непонятно. Аксиомы теории T должны быть сформулированы в её языке, а не в языке метатеории MT.

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

Указанное мной рекурсивное определение предиката $\mathfrak{N}$ тоже нельзя определить формулой языка арифметики Пеано, поскольку оно использует не определённый в языке предикатный символ.

Тем не менее, этот предикат должен быть определён в языке MT, иначе Вы не сможете определить, какие объекты MT принадлежат модели теории T. А для теории T этот предикат вообще не нужен.

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

Область определения для переменной $m_k$ действительно растёт с увеличением $n$, но это совершенно не означает, что что-либо происходит с конкретным значением этой переменной. Поясняю на конкретном примере. Допустим, на 5-ом шаге элемент последовательности имеет вид:
$x=4+5^{3+5^{2}+5^{1+5}}$
Здесь $m_1=1$, $m_2=1$, $m_3=3+5^{2}$, $m_4=4$.
Рассмотрим число, на единицу большее:
$x+1=5+5^{3+5^{2}+5^{1+5}}$
На следующем щаге последовательности Гудстейна произойдёт следующее:
1) Из числа $x+1$ вычтется единица.
2) Все пятёрки заменятся на шестёрки.
Получим:
$4+6^{3+6^{2}+6^{1+6}}$
Итак, получили число того же вида, что и $x$, но только с основанием разложения на единицу больше (6 вместо 5), что и утверждается в процитированном Вами отрывке.

В Вашей записи $g_4(y)=x+1=\Lambda_4(5,1,1,3+5^2,4+1)=\Lambda_4(5,1,1,28,5)$,
тогда $g_5(y)=\mathop{\mathrm{Subs}}\nolimits^6_5(x)=\Lambda_4(6,1,1,3+6^2,4)=\Lambda_4(6,1,1,39,4)$,
а не $\Lambda_4(6,1,1,28,4)$, как у Вас написано:

epros писал(а):

Let's consider the number $x+1=\Lambda_{m+2}(n,m_1,\ldots,m_{m+2}+1)$. If $x+1=g_{n-1}(y)$, then for the next step of Goodstein's sequence we will have:

$$g_n(y)=\mathop{\mathrm{Subs}}\nolimits^{n+1}_n (x)=\Lambda_{m+2}(n+1,m_1,\ldots,m_{m+2})\text{.}$$

Можно взять $g_4(y)=x+1=\Lambda_4(5,1,1,3+5^2,5^{5^5}+1)=\Lambda_4(5,1,1,28,5^{3125}+1)$,
тогда $g_5(y)=\mathop{\mathrm{Subs}}\nolimits^6_5(x)=\Lambda_4(6,1,1,3+6^2,6^{6^6})=\Lambda_4(6,1,1,39,6^{46656})$,
а не $\Lambda_4(6,1,1,28,5^{3125})$. Как я и говорил, числа $m_k$ растут, а не остаются постоянными. Вы же имеете в виду, что последнее число с каждым шагом уменьшается на единицу (у Вас так написано).

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

Да, только Вы забыли подставить $n=2$:

$$\Lambda_{m+2}(2,2,0,\ldots,0)=2^{2^{.^{.^{.^2}}}}\text{,}$$

Импликацию я считаю верной потому, что к этому ведёт цепочка рассуждений по индукции.

Я уже говорил, что я не понимаю, на основании чего Вы делаете индуктивные переходы. Они были бы правильными, если бы числа $m_k$ не возрастали на каждом шаге, а последнее из них убывало так, как это у Вас написано. Фактически же они возрастают на протяжении очень большого числа шагов, и совсем не очевидно, что когда-нибудь начнут убывать.

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

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

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

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

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

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

И как Вы хотите узнать, стандартное число "этажей" или нестандартное?
Есть доказательства недоказуемости теоремы Гудстейна в арифметике Пеано, по-видимому, не использующие никаких нестандартных моделей. Например: Andrés Eduardo Caicedo, Goodstein's function, Revista Colombiana de Matemáticas, Volumen 41(2007)2, páginas 381-391.

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

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

[Basil Peace]

По теме топика:
Про совершенную "неочевидность" равенства множеств есть в Николай Вавилов. Не совсем наивная теория множеств:

Цитата:

равенство, как и всё остальное, является результатом соглашения...

И далее приводится пример другого определения равенства множеств.

По поводу очевидности того или иного утверждения оттуда же:

Цитата:

Из Принстонского фольклора:
"In the fifties, it was said in Princeton that there were four definitions of the word "obvious".
If something was obvious in the sense of Beckenbach, then it is true and you can see it immediately.
If something is obvious in the sense of Chevalley, then it is true and it will take you several weeks to see it.
If something is obvious in the sense of Bochner, then it is false and it will take you several weeks to see it.
If something is obvious in the sense of Lefschetz, then it is false and you can see it immediately."