Существует ли биекция между вычислимыми числами и нат.?

[epros]

Someone писал(а):

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

Хочу попутно заметить, что конструктивный анализ также "не предполагает использования заранее сочинённого алгоритма". Т.е. когда говорится о том, что неизвестно, существует ли нечётное совершенное число, то речь идёт не только о том, что алгоритм прямого перебора, который был выполнен не помню уж то ли до $10^{300}$, то ли до $10^{400}$, пока такого числа не нашёл. Речь идёт о том, что эта проблема пока не решена всеми доступными средствами.

Так что когда я говорю, что "не исключено, что проблема неразрешима", я имею в виду "всеми средствами, которые доступны, когда либо будут доступны или даже в принципе могли бы быть доступными". А когда я говорю о "существующем решении проблемы", то я не обязательно готов его записать в форме конкретной строки и даже не обязательно речь идёт о конкретном алгоритме, который построит решение, если не столкнётся с ограничениями ресурсов. Речь может, например, идти об (n)-алгоритме, который построит (n-1)-алгоритм, который ... и т.д., и т.п. ... и в итоге построит (1)-алгоритм, который построит решение. Или о любом другом конструктивном методе.

Someone писал(а):

Я хотел сказать, что закон исключённого третьего не имеет отношения к тому, будет задача решена или не будет.

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

Someone писал(а):

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

Обращаю также Ваше внимание, что речь была не об утверждении о том, что "решение либо есть, либо нет", а о том, что решение является положительным или отрицательным.

Перевираете.

Мы говорили о законе исключенного третьего, т.е. об утверждении, что решением является либо ответ "да", либо ответ "нет". То, что "решение либо есть, либо нет" - это уже совсем другое утверждение.

Someone писал(а):

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

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

Someone писал(а):

но мои высказывания являются отражением Вашего экстремизма.

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

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

Someone писал(а):

И что-то всё-таки было об обоснованности CRA по сравнению с теорией множеств. И именно на основе интуитивно самоочевидных, но совершенно неопределённых свойств строк символов.

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

Someone писал(а):

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

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

Someone писал(а):

Если не аксиоматизировать нужные свойства строк, то ничего из них не выведется, ни арифметика Пеано, ни CRA.

Ну так мы их и аксиоматизируем. По-моему, тут все мнения сходятся?

Someone писал(а):

Возможно, Ваше мнение об общеочевидности свойство строк связано с отсутствием у Вас достаточного опыта в этой области, поскольку никаких других строк Вы не встречали. А я, например, в период учёбы (да и долгое время потом) пользовался двумя системами стенографии (фоностенографией О.С.Александровой и вариантом ГЕСС А.Г.Гильдебранда). Фоностенографией я пользовался недолго, всего год, поэтому буду говорить о стенографии А.Г.Гильдебранда. В этой системе очередной символ приписывается к имеющейся строке пятью разными способами. А это нарушает свойства строк, необходимые для обоснования аксиом Пеано и для работы алгоритмов. В частности,
1) неверно утверждение о единственности последователя;
2) посимвольно совпадающие строки могут быть различными.
Поэтому хотите Вы или не хотите, но свойства строк нужно формализовывать явным образом.

Я понимаю, что придумать можно что угодно. Можно придумать даже такое понимание "строки", которое не будет соответствовать обычному. Например, когда "посимвольно совпадающие строки могут быть различными" (промежутки между символами что-ли разные?). Но речь-то идёт именно о стандартном понимании, которое ещё и предварительно оговаривается (на неформальном уровне). А потом, да, - мы "явным образом" формализуем некоторые их общеочевидные свойства.

Someone писал(а):

О принципе Маркова я говорил. Он, конечно, вполне нормально смотрится с точки зрения классической математики, но почему Вы считаете его "общеочевидным", для меня загадка.

Тут я пока не готов ответить. Я знаю, о чем речь, но...

Добавлено спустя 1 час 44 минуты 57 секунд:

ewert писал(а):

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

Интересно, и как долго Вы собираетесь искать, скажем, пример конструктивно определённой на $\mathbb{R}$ нелинейной аддитивной функции?

ewert писал(а):

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

С чего Вы это взяли, что какие-то реальные задачи бывает невозможно конструктивно поставить?

Добавлено спустя 34 минуты 31 секунду:

маткиб писал(а):

Да и прикладникам будет проще пользоваться тем, что попроще, с учётом того, что и то, и другое принципиально не врёт.

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

маткиб писал(а):

Какое отношение имеет существование решателя к его описываемости каким-то там "высказыванием"?

Очень простое: Если наш мир познаваем, то это означает, что всё в нём существующее описываемо неким высказыванием. А до "существования" решателя где-то за рамками нашего мира (и по-моему кавычки здесь очень уместны), как мне кажется, нам не должно быть никакого дела.

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

маткиб писал(а):

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

Чтобы не было соблазна пытаться обосновать закон исключённого третьего соображениями типа: "вообразим себе универсальный решатель..."

Но в чём Вы противоречие углядели с существованием этого решателя?

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

маткиб писал(а):

Я вот, например, тоже не понимаю, чем счётное множество хуже конечного, но Вам же не очевидно?

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

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

[маткиб]

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

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

А пример про численное интегрирование Вы проигнорировали?

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

Очень простое: Если наш мир познаваем, то это означает, что всё в нём существующее описываемо неким высказыванием.

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

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

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

Ещё раз посмотреть пример про численное интегрирование.

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

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

Если специально не отворачиваться, то для конечных множеств из, например, $2^{2^{10000000}}$ элементов примеры из жизни настолько же "известны", как и для счётных множеств.

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

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

Уровень "критичности" отношений к своим знаниям всё равно придётся выбрать (отличный от абсолютного максимума и минимума). Чем больше критичность, тем слабее результаты, но тем они более надёжны. И выбирать придётся из различных соображений. Мне кажется, что "уровень критичности" соответствующий конструктивизму, чрезмерен и только тормозит развитие науки.

[epros]

маткиб писал(а):

А пример про численное интегрирование Вы проигнорировали?
...
Ещё раз посмотреть пример про численное интегрирование.

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

маткиб писал(а):

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

Очень простое: Если наш мир познаваем, то это означает, что всё в нём существующее описываемо неким высказыванием.

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

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

маткиб писал(а):

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

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

маткиб писал(а):

Если специально не отворачиваться, то для конечных множеств из, например, $2^{2^{10000000}}$ элементов примеры из жизни настолько же "известны", как и для счётных множеств.

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

маткиб писал(а):

Уровень "критичности" отношений к своим знаниям всё равно придётся выбрать (отличный от абсолютного максимума и минимума). Чем больше критичность, тем слабее результаты, но тем они более надёжны. И выбирать придётся из различных соображений. Мне кажется, что "уровень критичности" соответствующий конструктивизму, чрезмерен и только тормозит развитие науки.

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

[маткиб]

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

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

Поверхностный действительно не нужен.

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

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

Было бы интересно, если бы Вы привели подобное доказательство.

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

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

Вот не совсем прикладная, но интересная теорема, утверждающая об останавливаемости конкретного достаточно простого алгоритма, не доказуемая без аксиомы бесконечности:
http://en.wikipedia.org/wiki/Goodstein%27s_theorem

[ewert]

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

С чего Вы это взяли, что какие-то реальные задачи бывает невозможно конструктивно поставить?

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

[Nxx]

ewert писал(а):

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

С чего Вы это взяли, что какие-то реальные задачи бывает невозможно конструктивно поставить?

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

Вообще-то, вероятность всегда вводится аксиоматически.

[ewert]

и, значить, конструктивность как абсолютный прынцып --- вовсе не абсолютна, не так ли?

[Someone]

Nxx в сообщении #185832 писал(а):

Более того, согласно теореме Геделя, существуют алгоритмы, которые никогда не остановятся, но доказать это невозможно.

Nxx писал(а):

Цитата:

Странное утверждение. Откуда же тогда известно, что они не остановятся? В свете сказанного выше.

Из теоремы.

Ещё более странно. Если есть доказанная теорема, утверждающая, что алгоритмы не остановятся, то почему это невозможно доказать?

Nxx писал(а):

Цитата:

Не понял, причём тут теория сложности. Она что, отменяет физические ограничения на возможности физических устройств?

Она дает возможность определить, что можно решить эффективно.

Какое это имеет отношение к вопросу о существовании физической модели машины Тьюринга? Вы понимаете, что устройство, обладающее ограниченными ресурсами, не способно решать задачи, решаемые машиной Тьюринга?

epros писал(а):

маткиб писал(а):

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

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

Простенький пример, демонстрирующий полезность неконструктивной теоремы существования. Рассмотрим последовательность действительных чисел, определяемую рекуррентно формулами $x_1=1$, $x_{n+1}=\sqrt{1+x_n}$ при $n\in\mathbb N$. Найдём $\lim\limits_{n\to\infty}x_n$.
1) Легко видеть, что $x_2=\sqrt{2}>x_1$. Далее, поскольку при $n>1$ из неравенства $x_n>x_{n-1}$ следует, что $x_{n+1}=\sqrt{1+x_n}>\sqrt{1+x_{n-1}}=x_n$, отсюда следует, что наша последовательность возрастающая.
2) Заметим, что $x_1<2$. Если уже доказано, что $x_n<2$, то $x_{n+1}=\sqrt{1+x_n}<\sqrt{3}<2$, откуда следует, что наша последовательность ограничена.
3) По теореме о монотонной ограниченной последовательности, существует конечный предел $\lim\limits_{n\to\infty}x_n=x$.
4) Переходя к пределу при $n\to\infty$ в равенстве $x_{n+1}=\sqrt{1+x_n}$, получим уравнение $x=\sqrt{1+x}$, имеющее единственный корень $x=\frac{1+\sqrt{5}}2$.
5) Полезно оценить скорость сходимости. Заметим, что, так как наша последовательность возрастающая, то $1=x_1\leqslant x_n<x\leqslant 2$, поэтому $x-x_1\leqslant 1$ и

$$0<x-x_{n+1}=\sqrt{1+x}-\sqrt{1+x_n}=\frac{x-x_n}{\sqrt{1+x}+\sqrt{1+x_n}}<\frac{x-x_n}{2\sqrt{2}}\leqslant\frac{x-x_1}{\left(2\sqrt{2}\right)^n}\leqslant\frac 1{\left(2\sqrt{2}\right)^n}\text{,}$$

откуда $0<x-x_n\leqslant\frac 1{\left(2\sqrt{2}\right)^{n-1}}$ (заметим, что для получения этой оценки не требуется знать $x$; вполне достаточно знать, что $x$ существует, а также свойства предела).

Теорема о монотонной ограниченной последовательности является "чистой" теоремой существования, не дающей никакого конкретного действительного числа. В CRA эта теорема неверна: существует монотонная ограниченная последовательность рациональных чисел, которая в конструктивном смысле не имеет предела. Это не означает, конечно, что рассмотренная задача неразрешима конструктивными методами. В данном случае при конструктивном решении нужно вместо указанных выше пунктов 1) и 2) предъявить так называемый регулятор фундаментальности последовательности: алгоритм, вычисляющий такую последовательность натуральных чисел $\beta_n$, что для всех $k,l\geqslant\beta_n$ выполняется неравенство $|x_k-x_l|<2^{-n}$, после чего в пункте 3) используется соответствующая теорема CRA о сходимости фундаментальной последовательности.

ewert в сообщении #186226 писал(а):

"Вот и верь после этого людям!" Что ж это за непрерывность-то такая, если она допускает неограниченность?!...

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

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

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

Я чего-то не понял юмора. Вы предполагаете запустить алгоритм на выполнение раньше, чем его напишете?

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

Речь идёт о том, что эта проблема пока не решена всеми доступными средствами.

Ну, здесь ключевым словом является "пока". Со временем количество "доступных средств" увеличивается. Например, Большая теорема Ферма, поставленная в рамках элементарной теории чисел, была решена средствами, далеко выходящими за пределы этой теории. Известны теоремы, относящиеся к арифметике Пеано, которые недоказуемы в арифметике, но благополучно доказуемы в теории множеств. Заметим, что арифметика эквивалентна теории, которая получается, если в теории множеств ZFC аксиому бесконечности заменить её отрицанием.

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

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

даже не обязательно речь идёт о конкретном алгоритме, который построит решение, если не столкнётся с ограничениями ресурсов. Речь может, например, идти об (n)-алгоритме, который построит (n-1)-алгоритм, который ... и т.д., и т.п. ... и в итоге построит (1)-алгоритм, который построит решение

Это не обобщение. Фактически Ваш "(n)-алгоритм" и есть алгоритм, решающий задачу. Что он там делает, прежде чем выдать ответ - это его проблема.

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

Или о любом другом конструктивном методе.

Этого я не понял. У Б.А.Кушнера во введении (на странице 27 в имеющемся у меня издании "Лекций по конструктивному математическому анализу") написано: "Интуитивные понятия «эффективности», «вычислимости» и т.п. связываются с точным понятием алгорифма." Вы намерены произвольно расширять принятое в CRA понятие конструктивности?

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

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

??? Закон исключённого третьего означает, что высказывание $A\vee\neg A$ истинно независимо от истинности высказывания $A$. Это так при общепринятой двузначной интерпретации классической математической логики. В интуиционистской логике это не так.

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

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

Чёрт, я вообще перестал понимать, о чём Вы говорите. Разве классическая математика каким-то образом отрицает возможность ситуаций, когда задача неразрешима? К тому же, "задача неразрешима" - это не логическое значение. Это утверждение.

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

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

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

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

Ну так мы их и аксиоматизируем. По-моему, тут все мнения сходятся?

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

Я понимаю, что придумать можно что угодно. Можно придумать даже такое понимание "строки", которое не будет соответствовать обычному. Например, когда "посимвольно совпадающие строки могут быть различными" (промежутки между символами что-ли разные?). Но речь-то идёт именно о стандартном понимании, которое ещё и предварительно оговаривается (на неформальном уровне). А потом, да, - мы "явным образом" формализуем некоторые их общеочевидные свойства.

Я не пойму, начались какие-то подвижки, или нет?

Я не знаю, что такое "обычная" строка, пока это формально не определено. "Необычные" с Вашей точки зрения строки в стенографии придуманы не для того, чтобы осложнить Вам обоснование CRA. Они разрабатывались с целью достичь наибольшей скорости записи устной речи. В 1928 году проходил конкурс на лучшего съездовского стенографа. Некоторые стенографы писали со скоростью 140 слов в минуту. Более поздние данные мне неизвестны. Если бы Вы с детства пользовались стенографией, ничего "необычного" в таких строках для Вас не было бы. В них, кстати, не только промежутки между символами могут быть разными. Разным может быть положение символа относительно предыдущего символа или относительно линии строки. Может использоваться нажим (впрочем, с распространением шариковых ручек использование нажима стало затруднительным).

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

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

Если классическая теорема о существовании "заставляет искать решение", то вряд ли от этого жизнь "ищущего" станет легче (с учётом того, что он вряд ли что-либо найдёт).

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

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

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

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

В действительности абстракция актуальной бесконечности, которую Вы так не любите, ничем не хуже. Вдобавок, обе абстракции к математике как логической конструкции отношения не имеют. Все математики, независимо от направления, манипулируют конечными последовательностями символов. Эти абстракции вообще никак не используются в математических рассуждениях. В частности, абстракция актуальной бесконечности совершенно необязательна, о чём я Вам уже говорил. Мы можем интерпретировать множества не как совокупности одновременно существующих объектов, что предполагается данной абстракцией, а как свойства объектов. Это никак не влияет на математические рассуждения. Именно о такой интерпретации множеств в CRA говорит и Кушнер.

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

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

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

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

[epros]

маткиб писал(а):

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

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

Вот не совсем прикладная, но интересная теорема, утверждающая об останавливаемости конкретного достаточно простого алгоритма, не доказуемая без аксиомы бесконечности:
http://en.wikipedia.org/wiki/Goodstein%27s_theorem

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

Кстати, сама по себе арифметика ординалов (включая определение константы $\omega$, а также операций сложения, умножения и возведения в степень) не факт что требует для своего определения аксиомы бесконечности, ибо это тоже всего лишь арифметика. Но этот так, попутное замечание.

Как я понимаю, доказательство может быть построено на понятии "максимального количества степеней в n-ричном разложении числа". Например, в двоичном разложении числа 35, т.е. в $2^{2^2+1}+2+1$ двойка возводится в степень самой себя не более 2 раз. И очевидно, что при построении следующего элемента последовательности это "количество степеней" не увеличится. К тому же, можно конструктивно доказать, что через конечное количество шагов оно непременно уменьшится.

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

ewert писал(а):

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

С чего Вы это взяли, что какие-то реальные задачи бывает невозможно конструктивно поставить?

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

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

[маткиб]

epros писал(а):

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

Вообще-то, здесь используется ординал

$$ e_0=\omega+\omega^{\omega}+\omega^{\omega^{\omega}}+\ldots $$

Тут уж Вам не обойтись без актуальной бесконечности.

epros писал(а):

Кстати, сама по себе арифметика ординалов (включая определение константы $\omega$, а также операций сложения, умножения и возведения в степень) не факт что требует для своего определения аксиомы бесконечности, ибо это тоже всего лишь арифметика. Но этот так, попутное замечание.

Ну кроме этих операций там ещё есть рекурсия, супремум, бесконечные суммы и произведения всякие и т.п., без них не определить $e_0$.

epros писал(а):

Как я понимаю, доказательство может быть построено на понятии "максимального количества степеней в n-ричном разложении числа". Например, в двоичном разложении числа 35, т.е. в $2^{2^2+1}+2+1$ двойка возводится в степень самой себя не более 2 раз. И очевидно, что при построении следующего элемента последовательности это "количество степеней" не увеличится.

"Максимальное количество степеней" - это высота формулы - 1 что ли? Если да, то это верно и доказывается вполне себе конструктивно (в арифметике Пеано без проблем).

epros писал(а):

К тому же, можно конструктивно доказать, что через конечное количество шагов оно непременно уменьшится.

А вот это докажите!

epros писал(а):

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

Вы очень плохо думаете об арифметике Пеано (хотя с чего бы?). Синтаксических средств тут хватит и с большим запасом. В арифметике Пеано и гораздо более хитрые построения можно формализовывать.

epros писал(а):

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

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

[epros]

Someone писал(а):

Простенький пример, демонстрирующий полезность неконструктивной теоремы существования. Рассмотрим последовательность действительных чисел, определяемую рекуррентно формулами $x_1=1$, $x_{n+1}=\sqrt{1+x_n}$ при $n\in\mathbb N$. Найдём $\lim\limits_{n\to\infty}x_n$.
1) Легко видеть, что $x_2=\sqrt{2}>x_1$. Далее, поскольку при $n>1$ из неравенства $x_n>x_{n-1}$ следует, что $x_{n+1}=\sqrt{1+x_n}>\sqrt{1+x_{n-1}}=x_n$, отсюда следует, что наша последовательность возрастающая.
2) Заметим, что $x_1<2$. Если уже доказано, что $x_n<2$, то $x_{n+1}=\sqrt{1+x_n}<\sqrt{3}<2$, откуда следует, что наша последовательность ограничена.
3) По теореме о монотонной ограниченной последовательности, существует конечный предел $\lim\limits_{n\to\infty}x_n=x$.
4) Переходя к пределу при $n\to\infty$ в равенстве $x_{n+1}=\sqrt{1+x_n}$, получим уравнение $x=\sqrt{1+x}$, имеющее единственный корень $x=\frac{1+\sqrt{5}}2$.
5) Полезно оценить скорость сходимости. Заметим, что, так как наша последовательность возрастающая, то $1=x_1\leqslant x_n<x\leqslant 2$, поэтому $x-x_1\leqslant 1$ и

$$0<x-x_{n+1}=\sqrt{1+x}-\sqrt{1+x_n}=\frac{x-x_n}{\sqrt{1+x}+\sqrt{1+x_n}}<\frac{x-x_n}{2\sqrt{2}}\leqslant\frac{x-x_1}{\left(2\sqrt{2}\right)^n}\leqslant\frac 1{\left(2\sqrt{2}\right)^n}\text{,}$$

откуда $0<x-x_n\leqslant\frac 1{\left(2\sqrt{2}\right)^{n-1}}$ (заметим, что для получения этой оценки не требуется знать $x$; вполне достаточно знать, что $x$ существует, а также свойства предела).

Теорема о монотонной ограниченной последовательности является "чистой" теоремой существования, не дающей никакого конкретного действительного числа. В CRA эта теорема неверна: существует монотонная ограниченная последовательность рациональных чисел, которая в конструктивном смысле не имеет предела. Это не означает, конечно, что рассмотренная задача неразрешима конструктивными методами. В данном случае при конструктивном решении нужно вместо указанных выше пунктов 1) и 2) предъявить так называемый регулятор фундаментальности последовательности: алгоритм, вычисляющий такую последовательность натуральных чисел $\beta_n$, что для всех $k,l\geqslant\beta_n$ выполняется неравенство $|x_k-x_l|<2^{-n}$, после чего в пункте 3) используется соответствующая теорема CRA о сходимости фундаментальной последовательности.

Здесь мне не очевидно только одно: Как этот пример демонстрирует "полезность" неконструктивной теоремы существования? Не мудрствуя лукаво, я бы на практике начал решение этой задачи с Вашего п. 4, т.е. с решения соответствующего квадратного уравнения. Если мне вдруг потребуется доказать, что получившаяся величина является пределом данной последовательности, то не составит большого труда сделать это напрямую, без помощи теоремы существования предела для монотонных ограниченных последовательностей. Кстати, все остальные пункты Вашего рассуждения, кроме собственно п. 3, прекрасно работают и в конструктивном анализе.

Someone писал(а):

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

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

Я чего-то не понял юмора. Вы предполагаете запустить алгоритм на выполнение раньше, чем его напишете?

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

Someone писал(а):

Ну, здесь ключевым словом является "пока". Со временем количество "доступных средств" увеличивается.

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

Someone писал(а):

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

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

Someone писал(а):

Заметим, что арифметика эквивалентна теории, которая получается, если в теории множеств ZFC аксиому бесконечности заменить её отрицанием.

Я не уверен в том, что это вполне корректная интерпретация. Дело в том, что отрицание аксиомы бесконечности судя по всему невыводимо из аксиом арифметики.

Someone писал(а):

Существование решения может зависеть от обстоятельств, которые в данной теории не фиксированы.

Когда мы говорим о "решении", то речь обычно идёт о решении в рамках фиксированной теории. А судим мы об этом с помощью средств, которые фиксированы в рамках другой теории (мета-теории).

Someone писал(а):

Всё это имеет смысл только при условии, когда теория фиксирована. Как только мы разрешаем произвольно менять теорию (расширять, добавляя новые объекты и новые аксиомы, или заменять другой теорией, например, рассматривая метатеории), сама постановка вопроса теряет смысл. Обсуждается же именно такая ситуация, когда средства решения не фиксированы.

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

Someone писал(а):

Это не обобщение. Фактически Ваш "(n)-алгоритм" и есть алгоритм, решающий задачу. Что он там делает, прежде чем выдать ответ - это его проблема.

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

Someone писал(а):

Этого я не понял. У Б.А.Кушнера во введении (на странице 27 в имеющемся у меня издании "Лекций по конструктивному математическому анализу") написано: "Интуитивные понятия «эффективности», «вычислимости» и т.п. связываются с точным понятием алгорифма." Вы намерены произвольно расширять принятое в CRA понятие конструктивности?

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

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

Someone писал(а):

??? Закон исключённого третьего означает, что высказывание $A\vee\neg A$ истинно независимо от истинности высказывания $A$. Это так при общепринятой двузначной интерпретации классической математической логики. В интуиционистской логике это не так.

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

Someone писал(а):

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

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

Чёрт, я вообще перестал понимать, о чём Вы говорите. Разве классическая математика каким-то образом отрицает возможность ситуаций, когда задача неразрешима? К тому же, "задача неразрешима" - это не логическое значение. Это утверждение.

Вот я и говорю не просто о том, что "возможны ситуации, когда задача неразрешима", а о том, имею ли я право рассматривать такие ситуации как соответствующее логическое значение высказывания, составляющего формулировку задачи?

Someone писал(а):

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

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

Someone писал(а):

"Необычные" с Вашей точки зрения строки в стенографии придуманы не для того, чтобы осложнить Вам обоснование CRA. Они разрабатывались с целью достичь наибольшей скорости записи устной речи. В 1928 году проходил конкурс на лучшего съездовского стенографа. Некоторые стенографы писали со скоростью 140 слов в минуту. Более поздние данные мне неизвестны. Если бы Вы с детства пользовались стенографией, ничего "необычного" в таких строках для Вас не было бы. В них, кстати, не только промежутки между символами могут быть разными. Разным может быть положение символа относительно предыдущего символа или относительно линии строки. Может использоваться нажим (впрочем, с распространением шариковых ручек использование нажима стало затруднительным).

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

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

Someone писал(а):

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

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

Someone писал(а):

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

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

Someone писал(а):

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

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

Someone писал(а):

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

На это я уже ответил маткибу. Судя по Вашим дальнейшим комментариям, Вы мой ответ не восприняли. Никто на самом деле не говорит, что некую строку длиной $10^{10^{10}}$ символов мы сможем "реально" продолжить (не исключено, что мы у неё и конца-то не найдём). Речь в абстракции потенциальной осуществимости идёт только о том, что когда мы будем иметь дело с конкретной задачей, то это ограничение всегда можно будет считать выходящим за её рамки.

Someone писал(а):

Вдобавок, обе абстракции к математике как логической конструкции отношения не имеют. Все математики, независимо от направления, манипулируют конечными последовательностями символов. Эти абстракции вообще никак не используются в математических рассуждениях. В частности, абстракция актуальной бесконечности совершенно необязательна, о чём я Вам уже говорил. Мы можем интерпретировать множества не как совокупности одновременно существующих объектов, что предполагается данной абстракцией, а как свойства объектов. Это никак не влияет на математические рассуждения. Именно о такой интерпретации множеств в CRA говорит и Кушнер.

Вот этого уже я не понял. Аксиома бесконечности (а ведь это, как я понимаю, и есть утверждение о существовании актуальной бесконечности) "необязательна"? А о чём мы тогда с Вами спорили до сих пор? Конечно же я знаю, что в конструктивном анализе понятие "бесконечного множества" можно "интерпретировать" как перечислимый (или неперечислимый) тип. Например, "натуральное число" и "рациональное число" - это перечислимые типы. Для них даже есть доказуемое (тривиальным образом) утверждение, соответствующее "потенциальной бесконечности": Что не существует конечной совокупности объектов данного типа, содержащей все объекты. Однако с актуальной бесконечностью всё же есть разница.

Someone писал(а):

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

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

Someone писал(а):

Ваш "забор из палочек" - это и есть аксиома бесконечности.

Нет, это не так. Если интерпретировать аксиому бесконечности как утверждение о строках (из символов "{", "," и "}"), то она утверждает существование бесконечной строки. А это отнюдь не то же самое, что утверждение о существовании любой конечной строки.

[epros]

маткиб писал(а):

Вообще-то, здесь используется ординал

$$ e_0=\omega+\omega^{\omega}+\omega^{\omega^{\omega}}+\ldots $$

Покажите пальцем где используется. Я вижу, что в разложении числа (элемента последовательности) основание разложения (число $n$) заменяется на $\omega$. Поскольку число $n$ встречается в разложении элемента последовательности конечное количество раз, то и омег в результате в записи будет конечное количество. Ни о каких бесконечных возведениях в степень, вроде бы, речи нет.

маткиб писал(а):

Ну кроме этих операций там ещё есть рекурсия, супремум, бесконечные суммы и произведения всякие и т.п., без них не определить $e_0$.

Если не нужно $e_0$, то без бесконечных возведений в степень, очевидно, можно обойтись.

Кстати, по этому доказательству есть пара вопросов (возможно, довольно глупых, но чтобы уж расставить все точки над ё):
1) Чем доказано, что декремент числа приводит к тому, что парный к нему ординал становится строго меньше?
2) Чем доказано, что "не существует строго убывающей последовательности ординалов"? Как я понимаю, последовательность с точки зрения теории множеств - это множество пар из номера и элемента последовательности. А вполне упорядоченное множество, имеющее максимальный элемент, само по себе не обязано быть конечным.

маткиб писал(а):

epros писал(а):

К тому же, можно конструктивно доказать, что через конечное количество шагов оно непременно уменьшится.

А вот это докажите!

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

маткиб писал(а):

Вы очень плохо думаете об арифметике Пеано (хотя с чего бы?). Синтаксических средств тут хватит и с большим запасом. В арифметике Пеано и гораздо более хитрые построения можно формализовывать.

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

маткиб писал(а):

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

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

[маткиб]

epros писал(а):

Покажите пальцем где используется. Я вижу, что в разложении числа (элемента последовательности) основание разложения (число $n$) заменяется на $\omega$. Поскольку число $n$ встречается в разложении элемента последовательности конечное количество раз, то и омег в результате в записи будет конечное количество. Ни о каких бесконечных возведениях в степень, вроде бы, речи нет.

Ну всё правильно Вы говорите. Просто $e_0$ - это наименьший ординал, которого с гарантии хватит на все такие случаи. Иными словами, нам нужны все ординалы, которые строго меньше $e_0$.

epros писал(а):

Если не нужно $e_0$, то без бесконечных возведений в степень, очевидно, можно обойтись.

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

epros писал(а):

Кстати, по этому доказательству есть пара вопросов (возможно, довольно глупых, но чтобы уж расставить все точки над ё):
1) Чем доказано, что декремент числа приводит к тому, что парный к нему ординал становится строго меньше?
2) Чем доказано, что "не существует строго убывающей последовательности ординалов"? Как я понимаю, последовательность с точки зрения теории множеств - это множество пар из номера и элемента последовательности. А вполне упорядоченное множество, имеющее максимальный элемент, само по себе не обязано быть конечным.

Это вам, конструктивистам, не понять, ибо ТЕОРИЯ МНОЖЕСТВ

epros писал(а):

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

Никто не запрещает расширять синтаксис (например, для удобства). Но с точки зрения принципиальной доказуемости/недоказуемости такие расширения как правило не дают ничего нового (всё можно кодировать в исходном синтаксисе). Лучше это понимать во избежание заблуждений по поводу того, что, например, арифметика Пеано слаба из-за её убогого синтаксиса.

P.S. Остался в подвешенном состоянии вопрос о конструктивности аксиомы индукции. Например, с чего бы

$$ P(0)\&(\forall n)(P(n)\rightarrow P(n+1))\rightarrow(\forall n)P(n) $$

верна для неразрешимого $P(n)$?

Добавлено спустя 42 секунды:

Если уж собираемся мета-теоретические средства использовать, то надо хотя бы с индукцией разобраться.

Добавлено спустя 5 минут 32 секунды:

Подробнее про точки над "ё".

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

1) Чем доказано, что декремент числа приводит к тому, что парный к нему ординал становится строго меньше?

Это проще всего понять, если рассматривать вычитание единицы из числа как уменьшение его $k$-ичной записи в лексикографическом порядке. К слову сказать, операция возведения в степень для ординалов как раз определяется на основе лексикографического порядка.

epros писал(а):

2) Чем доказано, что "не существует строго убывающей последовательности ординалов"? Как я понимаю, последовательность с точки зрения теории множеств - это множество пар из номера и элемента последовательности. А вполне упорядоченное множество, имеющее максимальный элемент, само по себе не обязано быть конечным.

Это один из пунктов в определении вполне упорядоченного множества. Всё есть в Верещагине и Шене "Начала теории множеств".

[Nxx]

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

[epros]

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

Договоримся об обозначениях. Основание разложения числа (соответсвующее шагу последовательности) будем обозначать $n$, а "этажность" формулы его разложения - $m$ (т.е. минимальное число этажности $m+1$ - это $n^{[m]2}$, где под $n^{[m]1}$ понимается возведение числа $n$ в степень самого себя $m$ раз, а под $n^{[m]k}$ - то же самое, но вместо $n$ в самой верхней позиции подставлено $n^k$). Под переменными $m1$, $m2$ ... будем понимать любые неотрицательные целые числа.

Запишем такую цепочку из формул арифметики:

(1) Если любое число меньше $n^{[m]2}$ обнулится за конечное количество шагов, то любое число меньше $n^{[m+1]2}$ обнулится за конечное количество шагов.
(2) Если любое число меньше $n^{[m] m1}$ обнулится за конечное количество шагов, то любое число меньше $n^{[m] (m1+1)}$ обнулится за конечное количество шагов.
(3) Если любое число меньше $n^{[m-1]n^{m1}+m2}$ обнулится за конечное количество шагов, то любое число меньше $n^{[m-1]n^{m1}+m2+1}$ обнулится за конечное количество шагов.
...

Очевидно, что для заданного $m$ этих формул конечное количество (а именно, $m+3$). Последняя формула выглядит примерно так:

(m+3) Если любое число меньше $x+mk$ обнулится за конечное количество шагов, то любое число меньше $x+mk+1$ обнулится за конечное количество шагов.

где в качестве $x$ нужно подставить $m$ этажное выражение, которое я не могу сейчас выписать, а в качестве $k$ - число, равное $m+2$.

Последняя формула очевидно истинная (ибо первый же шаг по числу $x+mk+1$ превращает его в число вида $x+mk$). По индукции из неё следует предпоследняя, по индукции из неё следует пред-предпоследняя и т.д. до первой формулы. Из первой формулы по индукции следует, что обнулится любое число (что и является доказательством теоремы).

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