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

[Виктор Викторов]

nikov в сообщении #232669 писал(а):

Виктор Викторов в сообщении #232668 писал(а):

nikov в сообщении #232660 писал(а):

С моей точки зрения аксиомы геометрии вообще не являются интуитивно истинными.

Дайте, пожалуйста, определение (критерий) интуитивной истинности аксиомы.

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

Тот факт, что множество чётных чисел эквивалентно множеству натуральных чисел противоречит интуиции. Прежде чем на век умолкнуть я хочу задать два вопроса: какая из аксиом Лобачевского или Евклида соответствует действительности? Откровенно говоря, хотелось бы знать соответствует ли действительности аксиома выбора?

[AGu]

nikov в сообщении #232678 писал(а):

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

nikov писал(а):

Для ясности я еще предлагаю рассмотреть формальную теорию, обладающей теми же символами, что и арифметика Пеано, но единственной аксиомой $2 + 2 = 5$. Эта теория будет непротиворечивой, и в ней будет тривиально доказуемо утверждение $2 + 2 = 5$. Однако, это не сделает данное утверждение истинным. Не говоря уже о применениях в повседневной жизни, можно рассмотреть метаматическое применение: к формуле формального языка, состоящей из двух символов, приписали справа другую формулу, состоящую из двух символов. Сколько символов содержит результат этой операции?

Ответ: $5$. Потому что символ $5$ «по определению» равен $2+2$.

Заметьте, что $+$ - это всего лишь значок предложенной формальной теории. С чего Вы решили, что он имеет отношение к тому, что происходит с количеством знаков при приписывании одной формулы к другой?

Действительно, с чего это я так решил? Вы правы, для этого у меня не было никаких оснований. Я чисто по инерции подумал, что речь идет о стандартной интерпретации символа $+$ в арифметике длин строк. Теперь вижу, что ошибался.

[nikov]

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

[AGu]

nikov в сообщении #232686 писал(а):

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

Безусловно! Интуитивную истину глаголете. Несомненную справедливость констатируете.

[nikov]

Виктор Викторов в сообщении #232681 писал(а):

Тот факт, что множество чётных чисел эквивалентно множеству натуральных чисел противоречит интуиции. Прежде чем на век умолкнуть я хочу задать два вопроса: какая из аксиом Лобачевского или Евклида соответствует действительности? Откровенно говоря, хотелось бы знать соответствует ли действительности аксиома выбора?

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

-- Пн авг 03, 2009 16:19:10 --

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

Действительно, с чего это я так решил? Вы правы, для этого у меня не было никаких оснований. Я чисто по инерции подумал, что речь идет о стандартной интерпретации символа $+$ в арифметике длин строк. Теперь вижу, что ошибался.

А как же тогда нам узнать, какую теорию использовать, и какой смысл приписать ее значкам, если мы хотим подсчитать количество символов в конкатенации двух формул?

[Someone]

nikov в сообщении #232648 писал(а):

Виктор Викторов в сообщении #232581 писал(а):

А как с очевидностью и интуитивной истинностью аксиомы выбора?

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

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

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

nikov в сообщении #232660 писал(а):

С моей точки зрения аксиомы геометрии вообще не являются интуитивно истинными.

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

nikov в сообщении #232669 писал(а):

Истинное утверждение - утверждение, соответствующее действительности.

Какой действительности соответствует упомянутая выше аксиома арифметики?

nikov в сообщении #232669 писал(а):

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

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

nikov в сообщении #232669 писал(а):

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

Адекватности чему?

nikov в сообщении #232669 писал(а):

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

Что такое "ложные аксиомы"? Что значит, что "выводы не будут безусловно справедливы"?

nikov в сообщении #232660 писал(а):

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

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

nikov в сообщении #232688 писал(а):

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

Вы недооцениваете финитизм. В нём, например, определимы ординалы, меньшие первого эпсилонового, которые определяются уравнением $\omega^{\varepsilon}=\varepsilon$.

nikov в сообщении #232688 писал(а):

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

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

nikov в сообщении #232660 писал(а):

аксиомы Пеано являются интуитивно истинными, для них не требуется экспериментальная проверка

Но всё-таки... У Вас тут некоторое расхождение с eprosом. Он как раз утверждает, что аксиомы Пеано являются проверяемыми. В отличие, например, от аксиомы бесконечности. Но, несмотря на мои просьбы, обещанную проверку он так и не представил. Особо меня интересует, конечно, проверка следующих аксиом:
1) $0\in\mathscr H\wedge\forall n(n\in \mathscr H\to n|\in\mathscr H)$;
2) $\exists a(\varnothing\in a\wedge\forall b(b\in a\to b\cup\{b\}\in a))$.
Первое - это конъюнкция двух аксиом Пеано, записанная в обозначениях, взятых из учебника по конструктивному анализу ($\mathscr H$ - это натуральный ряд), второе - аксиома бесконечности. Первое, по утверждению eprosа, непосредственно проверяемо за конечное время, а второе - нет. Поскольку Вы с ним единомышленники, может быть, Вы представите требуемую проверку?

nikov в сообщении #232688 писал(а):

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

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

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

In recent years (after ca. 1985) the number of contributions to CRM has considerably decreased. Many researchers in CRM have turned to more computer-science oriented topics.

[AGu]

nikov в сообщении #232688 писал(а):

А как же тогда нам узнать, какую теорию использовать, и какой смысл приписать ее значкам, если мы хотим подсчитать количество символов в конкатенации двух формул?

«Узнать» -- никак, а вот договориться -- можно, причем массой способов (например, по ICQ ).

[nikov]

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

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

Где я говорил, что считаю ее недопустимой?

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

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

Не чушь. Не путаю. Мне есть дело. Можно аксиоматизировать.

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

Математика не имеет непосредственного отношения к реальному миру и занимается исключительно логическими конструкциями.

Имеет самое непосредственное отношение. Она возникла как результат взаимодействия с реальным миром, и мозг математика функционирует в реальном мире и по его законам.

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

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

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

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

nikov в сообщении #232660 писал(а):

С моей точки зрения аксиомы геометрии вообще не являются интуитивно истинными.

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

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

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

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

Да, люди разные, кто с этим спорит?

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

nikov в сообщении #232669 писал(а):

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

Адекватности чему?

Смотрите определение адекватности у Верещагина и Шеня, "Вычислимые функции", стр. 149.

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

nikov в сообщении #232669 писал(а):

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

Что такое "ложные аксиомы"? Что значит, что "выводы не будут безусловно справедливы"?

Ложные - это значит: не истинные, ошибочные. Например, $2 + 2 = 5$.
Не поверю, что Вы не знаете, чем отличается истина от лжи.

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

nikov в сообщении #232660 писал(а):

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

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

Да очень просто: представил себе два предмета, рядом с ними еще два предмета, и подсчитал, сколько всего будет предметов. Можно то же самое проделать с камешками, или палочками, нарисованными на листе бумаги.

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

nikov в сообщении #232688 писал(а):

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

Вы недооцениваете финитизм. В нём, например, определимы ординалы, меньшие первого эпсилонового, которые определяются уравнением $\omega^{\varepsilon}=\varepsilon$.

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

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

nikov в сообщении #232688 писал(а):

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

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

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

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

Поскольку Вы с ним единомышленники, может быть, Вы представите требуемую проверку?

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

[nikov]

Для иллюстрации моей мысли о интуитивно истинных аксиомах предлагаю ознакомиться с отрывком из книги Коэна (того самого, который доказал независимость континуум-гипотезы от аксиом ZFC в предположении ее непротиворечивости) "Теория множеств и континуум-гипотеза", стр. 153:

Цитата:

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

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

Цитата:

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

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

[Someone]

Виктор Викторов в сообщении #232581 писал(а):

А как с очевидностью и интуитивной истинностью аксиомы выбора?

А.С.Трулстра. Аспекты конструктивной математики. В сборнике "Справочная книга по математической логике. Часть IV. Теория доказательств и конструктивная математика." Москва, "Наука", 1983. Стр 160 - 240.

§ 4 писал(а):

Указанная интерпретация логических констант подсказывает, что следующая аксиома выбора должна быть верна ($AC_{00}=$):

$$\forall x\exists yA(x,y)\to\exists a\forall xA(x,ax)\text{,}\leqno{AC-NN}$$

так как доказательство посылки должно содержать метод, который даёт по каждому $x$ некоторый $y$ такой, что $A(x,y)$, а этот метод - не что иное, как функция, заданная законом.

То есть, интуиционизм считает аксиому выбора интуитивно верной.

nikov в сообщении #232780 писал(а):

Где я говорил, что считаю ее недопустимой?

Значит, я неправильно понял Ваш пассаж про самолёт в ответ на вопрос об аксиоме выбора.

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

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

nikov в сообщении #232780 писал(а):

Можно аксиоматизировать.

До самого конца? Давайте попробуем.

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

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

Математика не имеет непосредственного отношения к реальному миру и занимается исключительно логическими конструкциями.

nikov в сообщении #232780 писал(а):

Имеет самое непосредственное отношение. Она возникла как результат взаимодействия с реальным миром, и мозг математика функционирует в реальном мире и по его законам.

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

nikov в сообщении #232780 писал(а):

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

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

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

nikov в сообщении #232780 писал(а):

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

nikov в сообщении #232669 писал(а):

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

Адекватности чему?

Смотрите определение адекватности у Верещагина и Шеня, "Вычислимые функции", стр. 149.

Посмотрел. На странице 140 (возможно, это другое издание) читаем:

10.4 писал(а):

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

Вы считаете свой ответ адекватным моему вопросу?

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

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

nikov в сообщении #232780 писал(а):

Да очень просто: представил себе два предмета, рядом с ними еще два предмета, и подсчитал, сколько всего будет предметов. Можно то же самое проделать с камешками, или палочками, нарисованными на листе бумаги.

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

nikov в сообщении #232780 писал(а):

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

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

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

Что такое "ложные аксиомы"? Что значит, что "выводы не будут безусловно справедливы"?

nikov в сообщении #232780 писал(а):

Ложные - это значит: не истинные, ошибочные. Например, $2 + 2 = 5$.
Не поверю, что Вы не знаете, чем отличается истина от лжи.

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

[epros]

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

У Вас тут некоторое расхождение с eprosом. Он как раз утверждает, что аксиомы Пеано являются проверяемыми. В отличие, например, от аксиомы бесконечности. Но, несмотря на мои просьбы, обещанную проверку он так и не представил. Особо меня интересует, конечно, проверка следующих аксиом:
1) $0\in\mathscr H\wedge\forall n(n\in \mathscr H\to n|\in\mathscr H)$;
2) $\exists a(\varnothing\in a\wedge\forall b(b\in a\to b\cup\{b\}\in a))$.
Первое - это конъюнкция двух аксиом Пеано, записанная в обозначениях, взятых из учебника по конструктивному анализу ($\mathscr H$ - это натуральный ряд), второе - аксиома бесконечности. Первое, по утверждению eprosа, непосредственно проверяемо за конечное время, а второе - нет.

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

[Someone]

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

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

Это "известное свойство" - такая же аксиома, как сформулированная в процитированном Вами отрывке, и так же нуждается в проверке. А проверять её "не для всех" строк бессмысленно: вдруг для непроверенных строк она не выполняется?

Успокойтесь. Аксиомы конструктивного рекурсивного анализа "проверяемы" нисколько не более, чем аксиомы теории множеств. Тем более, что самих этих аксиом - бесконечное множество (как бы ни интерпретировать это множество).

[epros]

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

Это "известное свойство" - такая же аксиома, как сформулированная в процитированном Вами отрывке

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

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

и так же нуждается в проверке. А проверять её "не для всех" строк бессмысленно: вдруг для непроверенных строк она не выполняется?

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

[Someone]

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

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

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

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

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

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

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

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

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

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