Хайдук wrote: Насчет "эмерджентности" хороший вопрос - есть ли в целом что-нибудь принципиально большее, чем в части. Ответ далеко не очевиден...

Vladimirovich wrote:
а почему следует этому удивляться? ведь знаем же, что ОТО пока не увязана с квантовой микроструктурой микромасштабов, не вижу ничего крамольного, даже интересно и должно было ожидать

Alexander wrote:
я думаю, что есть, хотя в принципе должно можно вывезти поведение целой кучи путём большущего объёма вычислений на базе частей/элементов; дело в том, что коллективных структур (if any) с их динамикой никак нельзя предсказать на базе динамики отдельных частей, это почти магия висящая порою на волоске и значит подверженная случайным разрушительным збоям об (неожиданных) источниках которых нелегко прикинуть

Vladimirovich wrote: ... а Веейрштрасса оные это кто такие?

напротив, тут будет чем замутить воду: можно ли утверждать с чистым сердцем, что даже понятие о натуральных числах не подвергалось как-бы реинтерпретациям? вспомним сперва аксиоматику Пеано, потом трактовку 0, 1, 2, 3, ... в теории множеств как 0, {0}, {0, {0}}, {0, {0}, {0, {0}}}, ...

Хайдук wrote: Vladimirovich wrote:
с той разницей только, что математики в своей работе никогда не пользуются формальной нотацией матлогики, даже когда ищут (и находят, см. например первое "доказательство" Эндрю Уйлзом великой теоремы Ферма) ошибки в работах своих коллег

Хайдук wrote: Потому что математика на порядок сложнее

ну, и какой пользы в такой экстрим-формализации тогда?

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

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


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

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

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

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

Видите ли, ув.Хайдук, я совершенно потерял ход Вашей мысли.

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

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

В этом разница

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

Ну вот и Вы теперь видите разницу

Хайдук wrote: Сколько гигабайт займет формализация этого доказательства? И кто это все потом будет проверять?

вообще говоря формализация не предназначена для проверки челом, а для выполнения компом, поскольку тот не ошибётся вследствие усталости, внезапного затмения сознания и пр.; тем не менее чем громозже формализация, тем острее встаёт вопрос ЧТО на самом деле та выполняет, решает ли проблему или бьёт мимо?

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

в конце концов вышло, что и знаки не помогут, поскольку от принципиальной невыводимости (в том числе и самой непротиворечивости) не увильнуть; однако самым странным и шокирующим оказалось то, что вполне очевидные утверждения порядка 2+2=4 подвернулись недоказуемыми, что сразу делает их отрицания, которых даже не можем себе представить (!) вполне легитимными и допустимыми логически...

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

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

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

Alexander wrote:
в этом и состояло (по Гильберту со товарищи, а также Бурбакам) предназначение формальных систем - гарантировать "абсолютно правильный алгоритм" рассуждения/вывода из посылок/аксиом, что подразумевает и построение абсолютно правильных алгоритмов/программ для компов с учётом точных/строгих спецификаций задач, что поручаем компам решать. Самое главное, логический ВЫВОД должен был быть гарантированно безошибочным благодаря физической манипуляции физическими символами представляющими логику и аксиомы, что в принципе можно реализовать, хотя оно и не обязательно - логика с аксиомами вполне были ДО и остаются ПОСЛЕ символов. Символы (в руках компа) обеспечивают безошибочность, но когда их много это усугубляет интерпретацию; когда самих аксиом становится много (вкупе с ихней уже доказуемо недоказуемой непротиворечивостью!), тоже с трудом начинаем обозревать/просекать, тем более их формализацию символами

потому формализация практически годится только для компьютерной проверки уже объявленного не(до_конца)формального рассуждения/доказательства, как и было с 4-красками и 3-шарами; АТО чем поможет замещение аксиомы выбора симпатичным знаком, когда "выбор" из идеи бесконечного множества имеет мало общего со здоровенным выбором из конечного числа/количества, поскольку бесконечное это уже НЕ количество, а качество/сущность вместе со своим понятием мощности, которое только внешне похоже на (конечное) число/количество ; стало быть, недаром аксиома выбора оказалась именно аксиомой, независимой логически и концептуально, как бедным знакам донести это до башки?

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

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

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

Хайдук wrote: Формализация не догма, а руководство к действию

Даже если и руководство, то все равно нельзя, чтобы толерантность была общезначима
Вики wrote:

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

1=1

ну да, знали уже об этом

самоед-3 wrote: аксиоматизировать эти расплывчатые понятия не имеет смысла, не будет практического толку из-за бесплодного упрощения сложных людских ситуаций

Vladimirovich wrote:
безусловно, хотя интересно можно ли было додуматься (специалисту по теории чисел, скажем) до очевидного (как 2+2=4) арифметического выражения кодирующего/формализующего у Гёделя предложение "я недоказуемо"? можно ли было миновать такую вычурную кодировку, ведь в дальнейшем набрели на вполне приличную обобщённую теорему Рамсея, что оказалась невыводимой в арифметике Пеано? даже отсутствия решений у диофантовых уравнений нельзя получить у Пеано

Хайдук wrote: Невозможно, ибо 2+2=4 - слишком фундаментальный результат с многочисленными выводами, чтобы им разбрасываться Трудно представить себе ценность аксиоматики с его отрицанием