Someone писал(а):
Между прочим, утверждение: "Множество называется бесконечным, если его мощность
", есть и в указанной статье википедии.
Начхать на Википедию. Есть два существенно разных определения бесконечных множеств.
1) Множество
бесконечно, если оно не равномощно никакому натуральному числу (требуется предварительно определить натуральные числа в теории множеств).
2) Множество
бесконечно по Дедекинду, если оно содержит собственное подмножество
, равномощное самому
.
Если справедлива аксиома выбора, то оба определения равносильны. Без аксиомы выбора они, однако, не равносильны.
Существование множества, бесконечного по Дедекинду, насколько я знаю, равносильно обычной аксиоме бесконечности (П.Дж.Коэн. Теория множеств и континуум-гипотеза. "Мир", Москва, 1969. Это упоминается в примечании 2 к странице 117).
А моё определение, которое удивительным образом совпало с формулировкой из википедии, чем Вас не устраивает? Я так полагаю, что оно равносильно Вашему 1-ому, хотя это, конечно, нужно доказать (на что я, признаться, никакой мотивации не имею).
Someone писал(а):
Открыв книгу Кушнера, легко убедиться, что в конструктивном анализе они существуют. Что дальше?
Из приведённой Вами цитаты я в этом "убедиться" не могу. Это всего лишь некоторые общие слова, призванные объяснить, с каким объектами мы далее собираемся иметь дело (и обозначить их как-то).
Someone писал(а):
Я могу говорить о каких-то совокупностях натуральных чисел, даже называть их "множествами" и обозначать специальными буквами. Но это не значит, что я утверждаю, что существует множество, включающее их все.
"Их" - это кого? Множества или натуральные числа?
Совокупности натуральных чисел.
Someone писал(а):
В каком смысле множество натуральных чисел
, определённое Кушнером, содержит
не все натуральные числа?
В том смысле, что прямо об этом никто не заявил. Вот аксиома бесконечности в теории множеств
прямо заявляет, что множество включает
всех последователей. Есть такое же прямое утверждение где-то, например, у того же Кушнера?
Someone писал(а):
Но мы не знаем, что утверждение неразрешимо. Вы же сами писали, что это невозможно доказать средствами нашей теории (даже и вопрос-то такой нельзя сформулировать).
Мы рассматривали не такой случай, когда очередной шаг перебирающего алгоритма может оказаться неразрешимым. Эту возможность Вы сами домыслили.
Someone писал(а):
Речь шла о гипотетическом доказательстве конечности множества совершенных чисел, которое только сообщает нам, что таких чисел не может быть бесконечно много
Речь шла о гипотетическом конструктивном доказательстве, которое сообщает нам, что таких чисел конечное количество. Не "не может быть бесконечно", а именно "конечно", ибо это не одно и то же. В последнем случае мы можем быть уверены в том, что доказавший располагает способом
вычислить конкретное значение, которым ограничено количество объектов.
Someone писал(а):
Тот, кто это утверждает, доказал, что нужных нам чисел не более 100 штук. Он, однако, не смог определить точного количества. Может быть, их всего 99. Или даже меньше.
Я не пойму, Вы действительно этого не понимаете или придуриваетесь?
Вы исходите из того, что перебирающий "будет ждать" пока не наберётся ровно 100 штук, а поэтому если их меньше, то не дождётся. Но очевидно, что разумные условия перебора не могут быть таковыми. Когда перебор закончится и в ящике не останется больше предметов, алгоритм остановится и об этом нам станет известно.
Я понимаю, что Вы думаете, что с поиском совершенных чисел ситуация может быть иной, т.е. мы будем ждать 100-того числа. Так могло бы случится, если бы предъявленное нам доказательство того, что чисел не более 100, было неконструктивным. Но если оно конструктивно, то значит, что в алгоритм перебора будет заложен какой-то способ определения того, что числа закончились.
Добавлено спустя 1 час 4 минуты 19 секунд:Nxx писал(а):
Я прекрасно понимаю, какие варианты есть в интуицинистской логике (невозможно доказать, что невозможно доказать... и т.д.). Но при этом число m есть только в первых двух вариантах, когда его можно вычислить.
Варианты не совсем такие. "Невозможно доказать" может быть доказуемо в самой теории (без привлечения мета-теоретических средств) и в таком случае является просто опровержением. Вот "неразрешимость" в теории доказана быть не может, а поэтому, если она имеет место, то это - новый "случай".
Nxx писал(а):
С чего вы решили, что случаев только два?
Я этого не говорил.
Nxx писал(а):
С чего вы решили, что случай (с) противоречив?
Я Вам уже объяснял. Это связано с тем, что стоящий перед нами вопрос - о существовании. Поэтому в какой бы теории мы ни рассуждали, доказательство того, что существование объекта с помощью легальных средств недоказуемо, является доказательством его несуществования. Таким образом, в данной теории вопрос сущестования объекта разрешён, т.е. утверждение в той же теории о его неразрешимости было бы неверным.
Кстати, именно так Гёделевское
понимает мета-теория. Это высказывание имеет вид:
или
, где
- некий арифметический предикат.
Мета-теория
понимает предикат
так: "
является Гёделевским номером доказательства
в теории
". В самой теории
высказывание
неразрешимо. А раз
недоказуемо в теории
, значит с точки зрения мета-теории
утверждение
верно. Т.е. вопрос существования такого
разрешён в мета-теории
, однако неразрешим в теории
.
Теперь подумайте: Может ли какая-то из теорий утверждать неразрешимось этого вопроса
в ней самой? Нет. В теории
вопрос неразрешим, но она об этом "не знает". А в теории
вопрос разрешён.
Nxx писал(а):
потому что число х, якобы, рациональное по условию задачи.
Я не говорил, что "число
рациональное по условию задачи". Я говорил, что в обоих из двух случаев (a) или (b) оно рациональное. Но в конструктивной логике на двух этих вариантах всё не заканчивается.
Я же Вам продемонстрировал, как предположение о нерациональности
сводится к противоречию. В конструктивной логике, как и в классической, это означает опровержение предположения. Таким образом, имеем доказанным двойное отрицание: невозможность нерациональности
. Закона же снятия двойного отрицания в конструктивной логике нет, и не нужно притягивать его за уши, пытаясь перебрать какие-то "случаи" (занятие заведомо бессмысленное, ибо "случаев" этих бесконечно много).
Добавлено спустя 24 минуты 19 секунд:Xaositect писал(а):
Вот мы тут про геделевское утверждение говорим.
Оно имеет вид
, где предикат
рекурсивен и означает, что доказательство за номером
является доказательством утверждения
.
При этом для каждого конкретного
доказуемо, что
, то есть если мы возьмем алгоритм, который выдает число, в
-м разряде которого стоит 1, если
и 0, если
, то он задает конструктивное число 0, но мы не можем этого доказать.
Nxx, что вы все-таки думаете насчет этого примера конструктивного числа, которое не может не быть равным нулю, потому что доказать равенство мы не можем, а неравенство в
-м разряде ведет к противоречию с
?
Доказательство рекурсивности
и связанные вопросы можно прояснить в
Мендельсоне, гл. 3.
Кстати,
Xaositect, это в качестве примера "неснимаемого" двойного отрицания не подходит. В теории мы не можем привести
к противоречию (можем только привести к противоречию
для любого предварительно выбранного
, но общего механизма опровержения для всех
в теории нет). Поэтому теория не может доказать, что это число не может не быть равным нулю. А мета-теория может доказать не только это, но и то, что число равно нулю.