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

[arqady]

nikov писал(а):

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

О реальном человеческом мире.

[epros]

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

для этого требуется бесконечно много бумаги, чернил и времени.

нет

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

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

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

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

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

Кстати, Вы не находите, что построения CRA уже давно вышли за границы, в которых возможна эта самая "непосредственная" проверка?

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

[Someone]

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

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

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

для этого требуется бесконечно много бумаги, чернил и времени.

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

нет

Да. Смотрите ниже.

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

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

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

$\begin{tabular}{c|c}n&число частей\\ \hline $0$&$1=2^0$\\ $1$&$2=2^1$\\ $2$&$4=2^2$\\ $3$&$8=2^3$\end{tabular}$

Сделаем отсюда вывод, что число частей равно $2^n$ для всех целых $n\geqslant 0$? А если для $n=4$ получится $14$ вместо $16=2^4$, скажем, что это "не тот объект"?
Другой пример. Я за свою жизнь видел очень много ворон. Все они были серые с чёрными крыльями. Можно ли сделать отсюда вывод, что все вороны такие? Когда я учился в аспирантуре, у меня был приятель из Хабаровска. Как-то мы с ним прогуливались около университета, и он вдруг спрашивает: "А это что за птица?" Я посмотрел и говорю: "Ворона." Он был сильно удивлён. В Хабаровске ворóны чёрные. Потом я посмотрел в книге (какой-то зоологический справочник о птицах СССР) и узнал, что на территории СССР действительно живут две разновидности ворон: на западе - серые с чёрными крыльями, на востоке - чёрные.

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

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

Вы уверены, что Вы сможете добавить чистый лист бумаги? Или что найдёте чернила?

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

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

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

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

Имеется в виду тривиальность: временнáя сложность алгоритмов, используемых в CRA, заведомо превосходит то, что мы можем "проверить" на реальных объектах.

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

Именно потому, что я не вижу примера построения бесконечного объекта.

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

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

[epros]

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

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

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

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

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

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

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

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

Имеется в виду тривиальность: временнáя сложность алгоритмов, используемых в CRA, заведомо превосходит то, что мы можем "проверить" на реальных объектах.

Это зависит от того, как мы будем проверять. Живой пример - хотя бы проверка материализуемости того же самого числа $10^{10^{10}}$. Очевидно, что времени для его записи чёрточками нам в реальности заведомо не хватит. Поэтому проверка заключается не в выписывании всего числа, а в проверке того, что процесс выписывания числа разбивается на конечное количество шагов, каждый из которых реализуем.

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

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

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

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

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

Вам нужен не CRA, который активно работает с бесконечными множествами, а финитизм, в котором бесконечные множества категорически запрещены.

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

[Droog_Andrey]

Если я правильно уловил нить беседы, в соседней теме недавно шли подобные рассуждения:
post235092.html#p235092

[Someone]

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

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

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

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

Нет. Это утверждение в общепринятой аксиоматике арифметики является аксиомой.

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

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

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

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

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

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

Встречались. Уже во времена Архимеда, а может быть, и раньше.

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

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

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

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

Вот именно. И никаких "проверок" в реальном мире мы устроить не можем.

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

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

Имеется в виду тривиальность: временнáя сложность алгоритмов, используемых в CRA, заведомо превосходит то, что мы можем "проверить" на реальных объектах.

Это зависит от того, как мы будем проверять. Живой пример - хотя бы проверка материализуемости того же самого числа $10^{10^{10}}$. Очевидно, что времени для его записи чёрточками нам в реальности заведомо не хватит. Поэтому проверка заключается не в выписывании всего числа, а в проверке того, что процесс выписывания числа разбивается на конечное количество шагов, каждый из которых реализуем.

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

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

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

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

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

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

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

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

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

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

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

Вам нужен не CRA, который активно работает с бесконечными множествами, а финитизм, в котором бесконечные множества категорически запрещены.

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

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

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

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

Что касается CRA, который "активно работает с бесконечными множествами" в том смысле, что он принимает аксиому бесконечности, то я его точно в такой же степени не понимаю, как и классическую теорию множеств.

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

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

[epros]

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

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

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

Нет. Это утверждение в общепринятой аксиоматике арифметики является аксиомой.

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

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

Эта модель хорошо описывает процесс счёта, но далеко выходит за границы того, что можно проверить. Есть мнение (не моё), что слишком далеко.

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

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

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

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

Встречались. Уже во времена Архимеда, а может быть, и раньше.

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

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

Вот именно. И никаких "проверок" в реальном мире мы устроить не можем.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Как это? Вот теория множеств определяет, конечно множество или бесконечно (т.е. в ней можно записать формулу $fin(x)$, утверждающую конечность множества $x$). После этого мы берём, и все высказывания теории множеств переделываем в высказывания только о конечных множествах (добавив где нужно условие $fin(x)$)?

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

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

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

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

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

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

[Someone]

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

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

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

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

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

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

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

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

Какие примеры? Архимед показал, как можно определить число $10^{80000000000000000}$. Оно вполне себе "натуральное число", но очень далеко выходит за пределы того, что можно реализовать как "строку чёрточек".

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

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

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

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

Чтобы "убедиться" в осуществимости, порой бывает достаточно веры в то, что такой шаг "во всём подобен" шагу, осуществлённому ранее.

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

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

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

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

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

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

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

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

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

Как это? Вот теория множеств определяет, конечно множество или бесконечно (т.е. в ней можно записать формулу $fin(x)$, утверждающую конечность множества $x$). После этого мы берём, и все высказывания теории множеств переделываем в высказывания только о конечных множествах (добавив где нужно условие $fin(x)$)?

Финитизм не имеет отношения к теории множеств. Это некоторое ограничение арифметики.

A.S.Troelstra писал(а):

Finitism may be characterized as based on the concept of natural number (or finite,
concretely representable structure), which is taken to entail the acceptance of proof
by induction and definition by recursion.
Abstract notions, such as ‘constructive proof’, ‘arbitrary number-theoretic function’
are rejected. Statements involving quantifiers are finitistically interpreted in
terms of quantifier-free statements. Thus an existential statement $\exists xAx$ is regarded
as a partial communication, to be supplemented by providing an $x$ which satisfies
$A$. Establishing $\neg\forall xAx$ finitistically means: providing a particular $x$ such that $Ax$
is false.

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

Это не я придумал. Может быть я это несколько иными словами выразил, но требование предъявления построения примера объекта для любого утверждения о существовании было заложено в конструктивизм его основателями.

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

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

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

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

Да, была такая ссылка. Так ведь в теории множеств ни одного явно определённого множества нет, ни конечного, ни бесконечного. Обратите внимание, что в ZF (и в ZFC), кроме аксиомы бесконечности, есть ещё аксиома существования пустого множества, и она, насколько мне известно, из остальных аксиом не выводится. А аксиома бесконечности в современной формулировке явно ссылается на существование пустого множества.

Насколько я помню, эта ссылка относилась не к CRA, а к направлению, которое развивал Бишоп, но оно, вроде бы, идейно близко к CRA.

A.S.Troelstra писал(а):

In carrying out his programme, Bishop is guided by three
principles:
1. avoid concepts defined in a negative way;
2. avoid defining irrelevant concepts — that is to say, among the many possible
classically equivalent, but constructively distinct definitions of a concept,
choose the one or two which are mathematically fruitful ones, and disregard
the others;
3. avoid pseudo-generality, that is to say, do not hesitate to introduce an extra
assumption if it facilitates the theory and the examples one is interested in
satisfy the assumption.
Statements of Bishop’s constructive mathematics (BCM for short) may be read
intuitionistically without distortion; sequences are then to be regarded as given by
a law, and accordingly, no continuity axioms nor bar induction are assumed.
Statements of BCM may also be read by a Markov-constructivist without essential
distortion; the algorithms are left implicit, and no use is made of a precise
definition of algorithm.