по своему происхождению аксиоматические теории даже формальными не были, а то каков шанс неким операциям со знаками найти некое (неформальное) применение в будущем?
это да, как недостижимый (и ненужный, по большому счёту) идеал; гораздо интереснее будет как на практике добились формального доказательства компом 4-х красок и 3-упаковки ядрами? ведь компу надо было самому (во избежание ошибок) найти дорогу к неизбежным промежуточным подсказкам нами (а то самому не выбраться из джунглей) и наконец к целевому формальному утверждению теоремы
Практическая реализация может быть безумно сложна.
Но суть в том, что возможна. Это главное
Проверка формализованного текста требует лишь в некотором роде механического внимания, так как единственные возможные источники ошибок — это длина или сложность текста. Вот почему математик большей частью доверяет собрату, сообщающему результат алгебраических вычислений, если только известно, что эти вычисления не слишком длинны и выполнены тщательно.
Напротив, в неформализованном тексте всегда существует опасность ошибочных умозаключений, к которым может привести, например, злоупотребление интуицией или рассуждение по аналогии. Однако в действительности математик, желающий убедиться в полной правильности, или, как говорят, "строгости", доказательства или теории, отнюдь
не прибегает к одной из тех полных формализации, которыми мы. сейчас располагаем, и даже большей частью не пользуется частичными и неполными формализациями, доставляемыми алгебраическим и другими подобными исчислениями.
Обыкновенно он довольствуется тем, что приводит изложение к такому состоянию, когда его опыт и чутье математика говорят ему, что перевод на формализованный
язык был бы теперь лишь упражнением (быть может, очень тягостным) в терпении.
Если, как нередко бывает, возникают сомнения, то в конечном счете они относятся именно к возможности прийти без двусмысленности к такой формализации — употреблялось ли одно
и то же слово в разных смыслах в зависимости от контекста, нарушались ли правила синтаксиса бессознательным употреблением способов рассуждения, не разрешаемых явно этими правилами, была ли, наконец, совершена фактическая ошибка. Если оставить в стороне последний случай, то непременно рано или поздно сомнения преодолеваются тем, что текст редактируется, все больше и больше приближаясь к формализованному тексту, пока, по общему мнению математиков, дальнейшее продолжение этой работы не станет излишним.
Иными словами, правильность математического текста всегда проверяется более или менее явным сравнением с правилами какого-либо формализованного языка.
Если бы формализованная математика была так же проста, как игра в шахматы, то, составив описание выбранного нами формализованного языка, мы должны были бы затем лишь излагать наши доказательства на этом языке, подобно тому как автор шахматного трактата записывает в своей нотации партии, которым он хочет научить, сопровождая их в случае необходимости комментариями.
Однако вопрос решается отнюдь не столь легко, и не требуется большого опыта, чтобы убедиться в абсолютной неосуществимости подобного проекта: даже простейшее доказательство из начального раздела Теории множеств потребовало бы сотен знаков дла своей полной формализации.
Поэтому, уже начиная с Книги I настоящего Трактата, возникает настоятельная необходимость сокращать формализованный текст введением новых слов (называемых „сокращающими символами") и дополнительных правил синтаксиса (называемых „дедуктивными критериями") в довольно значительном количестве.
Поступая так, мы получаем языки, гораздо более удобные, чем формализованный язык в собственном смысле, и относительно которых любой мало-мальски опытный математик будет убежден, что их можно рассматривать как стенографические транскрипции формализованного языка.
Но мы уже не будем иметь уверенности, что переход от одного из этих языков к другому может быть сделан чисто механическим образом. Чтобы обрести эту уверенность, пришлось бы
настолько усложнить правила синтаксиса, управляющие употреблением новых слов, что польза от этих слов стала бы иллюзорной. Здесь, как и в алгебраическом исчислении и при употреблении почти любых обозначений, которыми обычно пользуются математики, удобный инструмент предпочитается другому, теоретически более совершенному,
но слишком громоздкому.
Как увидит читатель, введение этого сжатого языка сопровождается -„рассуждениями" особого типа, принадлежащими к так называемой Метаматематике.
как ни странно, НЕ согласный я с бОльшей частью написанного Бурбаками ; бьюсь об заклад, что написано хотя бы полвека тому назад и местами звучит устарело, даже нестрого
Проверка формализованного текста требует лишь в некотором роде механического внимания, так как единственные возможные источники ошибок — это длина или сложность текста. Вот почему математик большей частью доверяет собрату, сообщающему результат алгебраических вычислений, если только известно, что эти вычисления не слишком длинны и выполнены тщательно.
формализованный текст предназначен компу, бессмысленно брешущему челу проверять текст, поскольку не будет уверенности не ошибся ли элементарно; "проверять" комп также бессмысленно, зачем тогда давать ему работу? комп безошибочен по определению, проверять его незачем.
в неформализованном тексте всегда существует опасность ошибочных умозаключений, к которым может привести, например, злоупотребление интуицией или рассуждение по аналогии… желающий убедиться в полной правильности, или, как говорят, "строгости", доказательства или теории, отнюдь не прибегает к одной из тех полных формализации, которыми мы сейчас располагаем… приводит изложение к такому состоянию, когда его опыт и чутье математика говорят ему, что перевод на формализованный язык был бы теперь лишь упражнением (быть может, очень тягостным) в терпении... правильность математического текста всегда проверяется более или менее явным сравнением с правилами какого-либо формализованного языка.
в целом это неверно: полной универсальной формализацией для всей математики НЕ располагаем да и незачем, ведь никто бы не стал ею пользоваться; полная (реализуемая на компе) формализация даже отдельной задачи требует большой и очень кропотливой работы подверженной куче ошибок. На самом деле работающие математики НЕ стремятся к какой-либо формализации, стандарта такого нет, остаются только оценка и понимание их коллег; в тех редких и исключительных случаях, когда даже эксперты не могут придти к согласию (из-за громоздкости и запутанности задачи) насчёт правильности решения задачу могут полностью формализовать и отдать компу на проверку, 4-е краски и 3-упаковка шарами стали такими задачами.
для любой формализации остаётся каверзная и очень трудная проблема адекватности и релевантности задаче, которую формализация призвана решать, поскольку даже незаметные ошибки могут обернуться работой компа впустую/всуе по решению другой, а не интересующей нас задачи; знаковые конструкции это абракадабра для мозга и остаётся также проблема корректной интерпретации результатов компа, потому что только комп может гарантированно/доказуемо безошибочно оперировать знаками, а вот каким будет (если будет) их смысл это нам решать.
формализованный текст предназначен компу, бессмысленно брешущему челу проверять текст, поскольку не будет уверенности не ошибся ли элементарно; "проверять" комп также бессмысленно, зачем тогда давать ему работу? комп безошибочен по определению, проверять его незачем.
Вообще-то во времена Бурбаков компы были не такие
Но и все равно, остается проблема проверки программы, обрабатывающий этот формализованный текст. И эту рекурсию не преодолеть Хайдук wrote:
в целом это неверно: полными универсальными формализациями для всей математики НЕ располагаем да и незачем, ведь никто бы не стал ими пользоваться;
Мысль Бурбаков ортогональна.
в неформализованном тексте всегда существует опасность ошибочных умозаключений,
И это мысль правильная. Что мы ясно видим на примере нашего друга Впитера. Хайдук wrote:
На самом деле работающие математики НЕ стремятся к какой-либо формализации, стандарта такого нет, остаются только оценка и понимание их коллег; в тех редких и исключительных случаях, когда даже эксперты не могут придти к согласию (из-за громоздкости и запутанности задачи) насчёт правильности решения задачу могут полностью формализовать и отдать компу на проверку, 4-е краски и 3-упаковка шарами стали такими задачами.
Именно поэтому Бурбаки и говорят о Метаматематике Хайдук wrote:
для любой формализации остаётся каверзная и очень трудная проблема адекватности и релевантности задаче
Да. Я вверху отметил это же самое.
Но в целом ничего, что противоречило бы Бурбакам Вы не сказали, ув. Хайдук
все равно, остается проблема проверки программы, обрабатывающий этот формализованный текст.
безусловно, и в этом заключена проблема стриктной формализации: она гаубица, стрелять из которой по воробям не стоит, поскольку затраты по обеспечению логической безошибочности, полноты и смысловой/семантической адекватности перевешивают конечную реальную пользу.
в неформализованном тексте всегда существует опасность ошибочных умозаключений
... но, к счастью, консенсуса экспертов как правило хватает
Vladimirovich wrote:
поэтому Бурбаки и говорят о Метаматематике
они вроде говорили о замещении некоторых участков строгого кода чем-то покоротче, но я не думаю, что компромиссы тут желательны: ошибиться на таком скользком пути проще простого, всегда может померещиться некий миф; в действительности я не знаю какими точно путями добились уверенности в том, что комп реально решил эти две пресловутые задачи, о 4-х красках и об упаковки 3-пространства ядрами. Представляю себе это так: комп начинает с некоторой обозримой для нас и не вызывающей сомнения аксиоматической базы, его операции заведомо правильны и можно доказать, что не могут сплоховать в принципе; в дальнейшем мы его направляем (чтоб не утонул в джунгли потенциально возможных вариантов) предлагая ему некоторые полностью формальные (чтобы не ущучить его изначальную корректность) цели, до которых он будет стремиться достучаться; если не успеет, выбираем цели полргче и поближе к текущему состоянию его или даже он может показать нам, что цель была недостижимой поскольку поставленной нами ... ошибочно . Таким образом комп может (или не) доползти до лелеянного (нами) формального выражения теоремы и тогда останется, конечно, чтобы и мы были довольны этим выражением как адекватным нашей первоначальной, сугубо неформальной задаче; в этом последнем даже Бог не может помочь ни нам, ни компу, ни формализации по Бурбакам
ни вроде говорили о замещении некоторых участков строгого кода чем-то покоротче, но я не думаю, что компромиссы тут желательны: ошибиться на таком скользком пути проще простого
Правильно. Главное, иметь возможность проверить формально в случае неконсенсуса
А при консенсусе сойдет и так
думаю, что если хотим подлинного формального доказательства, то должны до конца строго соблюдать правила компа и не допущать никаких "консенсусних коротких замыканий", во избежание
Хайдук, нарисуйте графики этих функций, для последней достаточно одного периода.
Это напомнило мне, как сын в 9-м классе, рассказывая однокласснику о графике функции с косинусом, сказал, что в соответствии с конспектом если некоторое выражение(функция) умножается на положительное число, например у=9(косинус(х)), то период графика будет ДЕФОРМИРОВАН по оси Х, сжат в ДЕВЯТЬ раз!
Услышав моё возмущение, сказал, подожди, посмотрел школьный конспект и сказал, что так им продиктовали...
После моего возражения, что если что=то умножается на положительное число, большее единицы, то график "растягивается" по оси У, сказал ему подожди, пошёл разбираться...
Все это написал только потому, что страшно за формализацию и КОНСЕНСУС (агресивное большинство). С учетом: Vladimirovich wrote:
Alexander wrote:
Когда говорят о "бурбакизме" всегда вспоминается Арнольд с его остроумной критикой аксиоматического преподавания математики в школе.
А преподавание в школе и не должно быть бурбакистическим.
Условно говоря, преподавая детям информатику в школе, совсем не нужно заставлять их писать программы на ассемблере.
добавлю, со времен работы на КУВТ "Корвет", с ОЗУ аж на 48 Кб, говорил школьникам: не должен ученик думать, что если он решает задачку не карандашом, а гелиевой шариковой ручкой, то ему ДУMАТЬ необязательно...
И третье: ну может же ошибочка быть и в учебнике (как в тесте с олимпиады для первоклашек), или в утверждении преподавателя... Как и в моих рассуждениях! З павагай, к читателям и почитателям формализма
Дан шар и точка А на его поверхности. Построить систему окружностей, все точки которых принадлежат шару так, чтобы шар кроме точки А расслаивался на эти окружности - т е чтобы окружности не имели общих точек и любaя точка шара кроме А принадлежала одной из окружностей.
Мои конструктивные спoсобности крайне слабы и я за жизнь так и не научился делать такое. Но какие мои годы Научусь.
Решение. -
Warning: Spoiler![ Click to expand ][ Click to hide ]
Пусть В - точка, диаметрально противоположная А, МN - прямая, касающаяся шара в В. Рассмотрим круги, получающиеся в пересечении поверхности шара с плоскостями, проходящими через МN. Их центры лежат на окружности С, кaсающиеся шара в B(это легко, опускаю).
Искомая система соcтоит из:
1. Этой окружности.
2. Все окружности внутри шара на упомянутых плоскостях с центрами в центрах сечений.
3. Все параллели - т е сечения поверхности шара плоскостями, перпендикулярными АВ
параллелей не ли хватает плюс любая окружность через В (но не А)?
кажется, что окружность С не расслаивает шар, так как находится внутри его с диаметром равным радиусу шара, притом в центре шара у этой окружности "дыра", поскольку центр не может быть частью её.
кроме того у окружностей системы 1-3 много общих точек (моя любая через В тоже пересекает параллели )
Я слегка отредактировал описание решения(вставил слово "поверхности" в описание окружности С) Было как в книге - лёгкая неточность в описании, мне даже и незаметная(ясно о чём речь)
; бьюсь об заклад, что написано хотя бы полвека тому назад и местами звучит устарело, даже нестрого 
Научусь.
