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

Но ведь при этом будет доказано (!), что такая последовательность таки является разрешённой! Что ж Вы так от доказанной вещи отпираетесь?

Ещё раз, одно из двух:

1) Или формальные доказательства применимы всегда и везде — и тогда извольте признать корректность "доказанного доказательства" «потому что гладиолус».

2) Или формальные доказательства в применении к метаматематике теряют своё значение — но тогда и ZF потеряет автоматическую применимость к метаматематическим множествам (вроде множества всех формул, выводимых в самой ZF).

Tertium non datur, тут надо выбирать (ну, или закрыть глаза на проблему, если так проще).

> Квантор добавили Вы. У Вас, кстати, не было требования с любым текстом справиться.

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

> подходящий алгоритм где-то на треть должен суметь сжать.

Шутку понял. Смешно. Результат первого сжатия сжимаем ещё на треть, потом ещё на треть, и в итоге любой текст дожимается до одного байта — а потом ещё на треть :-)

> "Реальный" кирпич совершенно не исчерпывающе
> описывается в переписке.

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

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

> Толстую книгу "кирпичом" называете?

Я могу её назвать хоть Эманацией Тонкой Сущности Будды — она от этого ни существовать не перестанет, ни светиться не начнёт.

> Бананы? Вкусные и питательные?? Где???

В клетке. Но рвать нельзя — в той клетке так не принято :-)

> Например, "диагональный метод Кантора"
> не стали же называть "диагональным методом Цермело-Френкеля"?

Метод Кантора мы можем применять хоть при установлении неперечислимости множества несамоприменимых машин Тьюринга — суть его от этого не меняется. А вот суть континуум-гипотезы при переходе к Цермело-Френкелю меняется радикально. Простенькая аналогия: при доказательстве теоремы Гёделя о неполноте строится (явным образом, её программу можно на бумажке записать!) некая рекурсивная функция, которая тождественно обращается в нуль, но ни доказать, ни опровергнуть этого средствами формальной арифметики нельзя. Вы уверены, что утверждение об этой самой невозможности доказательства есть адекватный ответ на содержательный вопрос о том, является рассматриваемая функция нулевой, или нет?

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

> Это идеализм, если я правильно понимаю.

Неправильно понимаете. См. выше про гладиолус и "доказанные доказательства". А ещё лучше — откройте первую главу «Оснований математики». Всяко лучше, чем Бурбаки.

С уважением,
Гастрит

(Reply to this) (Parent) (Thread)

1) Или формальные доказательства применимы всегда и везде — и тогда извольте признать корректность "доказанного доказательства" «потому что гладиолус».

2) Или формальные доказательства в применении к метаматематике теряют своё значение — но тогда и ZF потеряет автоматическую применимость к метаматематическим множествам (вроде множества всех формул, выводимых в самой ZF).
Речь о работе вычислительной машины, вообще-то.
Ей "плевать" на противоречивость или непротиворечивость.
Она действует по каким-то алгоритмам, которые могут быть основаны на, например, арифметике. И основанность их на арифметике не означает, что они обязательно перестанут работать, если арифметика противоречива. "Потому что гладиолус" в данном случае непричём. Но достаточно сложные алгоритмы, считая через одно место, быть может, могут столкнутся с противоречиями арифметики с видимыми результатами (складывали 5 и 7 супербыстрым методом, корректность которого выведена из арифметики, и получили -3).

Tertium non datur, тут надо выбирать
А про интуиционистскую логику ещё почему-то пишут, что она лишена "закона исключённого третьего":)

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

Результат первого сжатия сжимаем ещё на треть…
Объясняю подробнее: в последней версии Юникода всего около 100000 символов, ну, ещё есть всякое, ещё куча зарезервирована, в сумме — 1114112 символов. Для записи знака в UCS-4 заведомо достаточно в среднем, таким образом, около 20.09 бит, а экономия только за счёт правильного использования этого свойства составит более 37%, более трети. Типичный текст в UCS-4 скорее всего сожмётся значительно сильнее. Проверил на "Жизни и судьбе" Василия Гроссмана: оригинал ("байтовый") — 1765564, в UCS-4 до сжатия — 6945864, а после сжатия обычными архиваторами — 621070/637473/700255/1036912, в каждом случае — меньше исходного "байтового" размера. Если в процентах, то, округляя вверх, примерно от 35.2% до 58.8%. Такова "реальность" как её можно изучать.

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

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

А вот суть континуум-гипотезы при переходе к Цермело-Френкелю меняется радикально.
И как? Она скучает по антиномиям и чахнет?

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

(Reply to this) (Parent) (Thread)

> складывали 5 и 7 супербыстрым методом,
> корректность которого выведена из арифметики,
> и получили -3

Не-не-не, давайте не устраивать путаницы. Мы ничего не складывали — мы провели некий алгорифмический процесс, который дал результат "-3". На арифметике тут была основана отнюдь не сама возможность осуществления этого процесса — на ней было основано теоретическое допущение, будто его результаты всегда совпадут с результатами другого (но тоже реального!) процесса (сложения). Оказалось, что такого совпадения нет — подумаешь, какая катастрофа! Да мало ли было в истории науки таких неверных допущений? Закон Бойля тоже выполняется лишь приближённо — и что, в момент обнаружения этой приближённости исчезли газы, к которым он ранее применялся, или из учебников физики сами собой стёрлись основанные на этом законе выкладки? Да и зачем так далеко ходить: я вот только что "сложил" стандартными средствами C два числа 40000 типа short — и знаете, оттого, что на выходе я получил -51072, мир ни разу не перевернулся.

> А про интуиционистскую логику ещё почему-то пишут,
> что она лишена "закона исключённого третьего":)

Вот именно потому, что так "пишут", Гейтинг и рвал на себе волосы :-) Потому что когда идиот со съеденным формальными системами мозгом видит исчисление и не видит в нём закона исключённого третьего — он тут же решает, что этим законом вообще запрещено пользоваться. Невдомёк идиоту, что «интуиционизм развивается независимо от формализации, которая может только идти по следам математической конструкции» (Гейтинг, «Интуиционизм», 1965, стр. 13), что «в любой момент открытие новых методов рассуждения может заставить нас расширить формальную систему» (там же) и что в разных ситуациях могут оказаться пригодными разные логические средства — идиоту вынь да положь исчерпывающий набор правил, годный на все случаи жизни.

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

> Я считаю, что слово "существовать" применимо к ним
> только как квантор в математическом контексте.

А я считаю, что четыре пальца — это четыре пальца, а не три и не пять (независимо от того, слышали мы про аксиомы Пеано, или не слышали). И 220 вольт — это именно 220 вольт (и чтобы превратить их в 12, нужен трансформатор, а не смена аксиоматики).

> И как?

А так, что непонятно:

1) Почему все свойства, аксиоматизированные в ZF, выполняются для канторовских (содержательно понимаемых!) множеств?
2) Почему в ZF аксиоматизированы все свойства, выполняющиеся для канторовских множеств?

Может, правильным является использование не ZF, а сочетания ZF+континуум-гипотеза? Или наоборот — ZF+отрицание континуум-гипотезы? Вот на этот вопрос Коэн ответил?

Что мне толку знать, что для гёделевской рекурсивной функции с формальной арифметикой совместимо как утверждение о её тождественном равенстве нулю, так и обратное? Получу ли я в действительности хоть одно отличное от нуля число, если запущу на реальной машине последовательно вычисляющую значения этой функции программу, или не получу — вот что меня единственно волнует. Hic Rhodus, hic salta.

> неточности (антиномии)

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

> На конкурсах (олимпиадах письменных, например)
> могут выше оценить работу, в которой
> больше вариантов додумывания

Что олимпиады — зло, я всегда знал :-)

С уважением,
Гастрит

(Reply to this) (Parent) (Thread)

(Reply to this) (Parent)