Брайан Дэвис (Brian Davies),
профессор математики Лондонского Кингс Колледжа

Формальная проверка доказательств

Кому доводилось писать компьютерные программы, пусть даже самые простые и короткие, тот прекрасно знает, что они, в отличие от математиков, не прощают ошибок. Малейшая ошибка в синтаксисе будет замечена компилятором, и выполнение такой программы будет тут же остановлено. Использование одного и того же имени для двух разных переменных компилятор пропустит, но такую ошибку трудно не заметить, поскольку на выходе программы скорее всего окажется полная ерунда. Математические ошибки часто выявляются путем прогона программы для несложной задачи аналогичного типа, решение которой заведомо известно. Варьирование входных параметров задачи при этом позволяет удостовериться, что модель ведет себя предсказуемо. Возможные ошибки и погрешности в утилитах, входящих в стандартные пакеты программного обеспечения, выявить гораздо сложнее в силу их незначительности и редкости проявления. Тем не менее программа длиной всего лишь в несколько сот строк способна невероятно облегчить жизнь математикам, и практика показывает, что отладка программы позволяет в конце концов добиться от нее правильного поведения. Реальные проблемы возникают при использовании по-настоящему длинных и сложных программ — как раз недавно администрация правительства Великобритании была почти неделю парализована из-за того, что на компьютеры всех ее подразделений было установлено некорректное обновление программного обеспечения.

Формальная проверка корректности работы программного обеспечения — забота одновременно и специалистов в области прикладной математической логики, и представителей бизнеса. В частности, повышение надежности Windows XP было достигнуто благодаря мощному аппарату анализа корректности программного обеспечения, который основан на математических методах формальной проверки непротиворечивости математических же алгоритмов, лежащих в основе функционирования программ. Однако в некоторых отношениях проблемы кибернетики и математики лежат в принципиально различных плоскостях. Техническая документация некоторых языков программирования, таких как Java, может занимать сотни страниц — значительно больше, чем может потребоваться для формулировки самой заумной теоремы. Иногда трудно даже сказать, «своеобразное» поведение программного обеспечения — это ошибка или особенность программы. Зависания (часто вследствие переполнения буфера) — это, несомненно, недоработки программистов; сложнее сказать что-либо определенное, когда LATEX, например, отказывается делать по запросу пользователя что-то такое, о чем разработчикам не пришло в голову, что такая функция вообще может кому-нибудь понадобиться. Вообще, неадекватные технические задания на разработку крупных программных пакетов — гораздо более распространенная причина катастрофических сбоев с непредсказуемыми экономическими последствиями, нежели неправильное выполнение технических заданий программистами.

Доказанная ценность формальных доказательств корректности программного обеспечения подтолкнула некоторых кибернетиков к идее попытаться применить те же методы и в строгой математике, однако это поле деятельности на сегодняшний момент для сбора урожая явно не созрело. Из нижеследующих замечаний явственно видно, что в анализируемой мною области с реализацией предлагаемых методов формального доказательства корректности предвидятся большие трудности. В других областях, возможно, им и найдется достойное применение (например, в математической логике или алгебре), но об этом пусть судят специалисты, работающие в этих областях. Я же приведу лишь некоторые детали, чтобы дать читателям возможность почувствовать атмосферу происходящего, пусть эти детали и несущественны. Почти все доказательства теорем в математическом анализе опираются на внешние факты, которые обычно не объясняются, поскольку подразумеваются известными читателю. Статью можно начать заявлением, что она посвящена спектральному анализу лапласиана на ограниченной евклидовой области с граничными условиями Дирихле. По одной этой теме, наверное, имеются сотни монографий и тысячи публикаций, и автор берет на себя смелость утверждать, что с большей их частью он знаком. При этом автор будет ссылаться лишь на новые и малоизвестные работы, о которых читатель может быть не в курсе, подразумевая, что с «классикой жанра» человек, взявшийся за чтение такой статьи, скорее всего, знаком в силу полученного им образования.

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

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

Эксперты почти инстинктивно «понимают», когда возможно изменить классическую теорему так, чтобы она подошла к обсуждаемому контектсту; по-видимому, эта способность и отличает эксперта. Время от времени находятся математики, у которых хватило сил собраться и написать монографию с более или менее полным описанием какой-либо области. Это большое дело, поскольку коллегам впоследствии будет на что ссылаться. Однако иногда такая монография только искажает реальное состояние дел, поскольку автор вольно или невольно выстраивает ее в однородном контексте, и многие теоремы, приведенные в таких монографиях, верны и при более слабых условиях.


31
Показать комментарии (31)
Свернуть комментарии (31)

  • Александр Орлов  | 25.12.2005 | 19:10 Ответить
    Статья хорошо показывает, какой ерундой занимаются отдельные "математики".
    Делом надо заниматься, нужным для общества, тогда и не понадобятся подобные рассуждения.
    Ответить
    • algen > Александр Орлов | 25.12.2005 | 19:23 Ответить
      Ага, пусть лучше идут лес валить вместе с некоторыми поэтами :)
      Ответить
    • sergey-ivanov85 > Александр Орлов | 01.04.2015 | 16:11 Ответить
      Отличная статья, я вот недавно читал книгу на эту тематику Пинбол-эффект. Джеймс Бёрк меня она очень впечатлила, скачал ее здесь http://infosklad.org/threads/pinbol-ehffekt-dzhejms-bjork.8113/ кому интересно рекомендую к прочтению!
      Ответить
  • crealab  | 25.12.2005 | 22:09 Ответить
    Отличная статья.

    Счётчик задач на будущее инкрементирован... Усё решим. А не решим, так укажем пути решения! :)

    Имхо, нужно копать в направлении исследования мозга и мышления математика. Рассмотреть математику в контексте биологической/технологической эволюции. Искать следует ограничительные теоремы. Не от переусложнения, а от внешних по отношению к математике законов Природы. Это уже даст какие-то дополнительные сведения, сориентирует.

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

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

    Короче, масса НОВЫХ направлений и деятельностей. Только людей не хватает, по-видимому. Где люди? - Стало быть в этом, в кризисе... ;)
    Ответить
  • inhabitant  | 30.12.2005 | 16:58 Ответить
    1965 г., В.М.Глушков - ГНОСЕОЛОГИЧЕСКИЕ ОСНОВЫ МАТЕМАТИЗАЦИИ НАУКИ (http://library.ntu-kpi.kiev.ua/html/arh_ntuu/glushkov/Gnoseolog_osnovy.htm):

    "...То обстоятельство, что мы вступили в век автоматизации процессов познания, позволяет нам считать, что пройден рубеж, который искусственно сдерживал границы математики, когда лозунг развития естествознания гласил 'мир устроен просто'. Возник такой лозунг не случайно. Ведь всякий естествоиспытатель, находя какой-то сложный закон природы, какое-нибудь уравнение Ван дер Ваальса с дополнительными членами, чувствовал себя неудовлетворенным. В XIX веке над ним довлела мысль: не может быть! В действительности природа должна быть устроена просто.

    Таков был неявный познавательный принцип. Конечно, принцип наивный, но он был очень прогрессивным для своего времени. Он нацеливал внимание математиков, естествоиспытателей именно на те части естествознания, которые можно было описать простыми средствами, имевшимися тогда в распоряжении математиков.

    Сейчас - иное дело: к лозунгу, что мир устроен просто, мы вполне можем прибавить лозунг, что в кое-каких частях он все же устроен сложно, и включить в сферу своего внимания определенную часть сложно устроенных, по существу сложно устроенных, вещей, сложных систем..."
    Ответить
    • Ada > inhabitant | 01.01.2006 | 08:32 Ответить
      Я очень уважаю мнение академика Глушкова, пожалуй, приведённый здесь пример, может повлиять на упрощенные взгляды на мир в сторону усложнения именно в силу доверия авторитету Глушкова. Но всё же в это не тот случай, когда следовало бы безоговорочно доверяться. Проникая всё больше и больше в глубь понимания сложных систем, я всё больше убеждаюсь в том, что мир, действительно, "устроен просто". Возможно, заблуждение о сложности мира исходит из того, что мы применяем неверно его формализацию? То есть, создав излишне сложные математические теории, запутав себя в них окончательно, мы выбиваем у себя "из-под ног" основы, на которых можем строить и все другие науки. В самом деле, когда обращаешься к группам, то первое, что приходит в голову - это классифицировать их. Согласно статье Брайана Дэвиса это не только не сделано до сих пор, но и вообще вряд ли когда-либо будет сделано. Такая невозможность, по моему мнению, может происходить на основе причин: либо мы ещё недостаточно изучили мир, и не можем замкнуть множество групп, либо математика переусложнила свои возможности и семимильными шагами ушла от тех, возможно, единственных видов формализации, на которых следовало бы остановиться. По крайней мере, всё же не мешало бы поработать в тех областях математики, которые дают доказуемые в смысле их корректности результаты, и провести в них классификацию применимости.
      Всех поздравляю с Новым годом!
      Ответить
  • sergmain  | 06.02.2006 | 02:46 Ответить
    в данной статье про теорему о четырех цветах говорится о яхыке Coq.
    Может кто нибуль из математиков дать комментарий по тому языку в разрезе данной статьи

    http://www.hizone.info/index.html?di=200504212
    Ответить
  • dims  | 06.02.2006 | 14:36 Ответить
    Мне кажется, проблема не в сложности самих доказательств, а в узкости того горлышка, по которому его можно передать. 100 томов страшны не тем, что там много сложного, а тем, что если их читать последовательно, то это займёт много времени. Точно так же, много времени займёт проверка или перепроверка доказательств, составленных компьютером.

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

    Грубо говоря, будут изобретено средство для ввода или вывода знаний прямо в или из мыслей. Человек нажимает кнопку, у него дёргаются глаза, как в Матрице -- и вот он уже знает доказательство. Точнее говоря, вероятно, будут просто изобретены средства коммуникации, превосходящие язык и письменность.
    Ответить
  • nickfv  | 17.03.2006 | 14:26 Ответить
    Всем уважаемым людям учавствующим в форуме
    я считаю что нужно веруться к основам матиматики и пересмотреть основы. Кто найдет что такое ноль и почему на ноль делить нельзя без вот этого "На ноль делить нельзя" тот сможет произвоить волшебство.
    Ответить
    • alnomy > nickfv | 28.03.2006 | 19:02 Ответить
      Само слово "деление" подразумевает - распределение между кем-то/чем-то. Разделить там четыре на два - означает, например, распределить поровну четыре яблока между двумя людьми.Частное - это то, сколько яблок будет у каждого.

      Почему нельзя делить на ноль? Можно. Вот у меня четыре яблока. Мне их надо разделить между никем. Частное будет (сколько яблок у каждого из никого).. ? Бесконечность яблок? Откуда же? у меня ж только четыре было!

      Еще интересней - допустим, надо разделить на пол-люда (4/0.5). Тогда половинка человека получит, по математике, 8 яблок! другая половинка при этом ничего не получит. Впрочем, фиг и первой, у меня яблок от арифметики что-то не прибавляется.. :))
      Ответить
      • ananas > alnomy | 15.03.2012 | 19:07 Ответить
        На все твои умствования даётся ответ в учебнике арифметики для начальной школы. Возьми его, отбрось свою тупую самоуверенность и смиренно изучи -- и тебе станет стыдно за ту чушь, которую ты здесь порешь!
        Ответить
      • dlt > alnomy | 08.05.2012 | 14:37 Ответить
        Проблемы математики в том, что они используют допущения и упрощения, несвойственные реальному миру. А потом пытаются с помощью этих допущений строить картину реального мира.
        Ну, например, с чего математики взяли, что понятие "ноль" вообще существует в природе?
        Ответить
    • Golder > nickfv | 17.04.2006 | 21:10 Ответить
      Есть теория чисел, которой мы все с вами успешно пользуемся.
      Задано два действия сложение(A+B=C), и умножение(A*B=C)по сути сложение числа A, B раз).
      Вычитание(A-B=C); результат которого вычисляеться так: число которое необходимо прибавить к В что-бы получилось A)
      Деление(А/В=С); результат вычисляеться так : число которое умножить на В что-бы получилось А.
      Задано изначально самой теорией чисел, что при умножении числа(Х) на 0 получаеться 0.(Х*0=0)
      Вернёмся к делению(А/В=С), не существует такого числа которое при умножении на 0(то есть на В) будет равно А, ну кроме случая с А=0(0/0=0 почему бы и нет)
      А вот Х*0=0, это огрничения самой теории Чисел.
      Ну или взять к примеру теорию множеств. Множество Х "умножаем" на пустое множество(то есть ноль), получаеться пустое множество. Если в это трудно вериться то можно нарисовать на бумажке диаграмму Венна-Эйлера(если учесть что пустое множество "нигде", то нету у них(у Х и пустого мноежства) общей области пересечения(а по определению это и есть результат их умножения).
      Получаеться что мы пользуемся определённой системой, теорией в которой производим все наши вычисления и негодовать по поводу "почему делить на нуль нельзя" глупо, ведь Дано: "число * нуль = нуль", ведь так же можно возражать почему 2+3=5?! =)
      Может когда-нибудь кто-то и придумает такую основу(набор теорем аксиом теорий)для исчисления, в которой сможем обойтись без нынешнего нуля, и она будет много удобнее, и откроет безграничные возможности для математики и всего человечества... :D
      Ответить
    • AAKozlov > nickfv | 11.12.2006 | 18:30 Ответить
      На самом деле, на ноль уже делить МОЖНО...
      В "теории обобщенных функций" вы просто обозначаете "1/0" как некое обобщенное число (функцию) (результат деления единицы на ноль).
      У этого числа нет значения но есть свойства - его можно прибавлять к числам умножать и т.д.
      Ответить
    • ananas > nickfv | 15.03.2012 | 09:31 Ответить
      Неуч, пишущий "учаВствующим", "матИматика", берётся судить о математике! Цирк!
      Ответить
  • Конан-Варвар  | 04.04.2006 | 17:55 Ответить
    Да, статья, безусловно, интересна и показательна. Уместная, точнее своевременная. К эпохе своевременна. Математика, как методологический инструмент точного познания мира стоит на рубеже очередной переформализации методов. Или революции в способах формализации своих методик работы. Во все известные нам (или большинству из нас) эпохи, начиная с античности, методики формализации процессов количествоенного описания процессов познания мира (включая инженерию во всех формах) испытывали последовательные стадии усложнения, насыщения и пресыщения усложнениями, затем наступал период упрощения путем введения более ёмких способов формализации и потом процесс повторялся. Кратко поясню на примерах развития способов математической нотации решений уравнений в античные времена, во время средневековья, в эпоху Возрождения и, наконец, в настоящее время, когда относительно универсальная нотация позволяет заменять огромадное множество вычислительных алгоритмов и дает возможность преподавать данные дисциплины в школах на всех континентах независимо от рас и национальностей. Лишь бы мозги да языки были в налиции. И глаза с руками. А ведь еще в середине тысячелетия простое квадратное уравнение описывалось , к примеру, итальянскими математиками словами и занимало это не полстрочки , а целую страницу порой. Так и теперь имеющаяся и очень изощренная нотация в пограничных областях познания уперлась в тупик суперусложнения. Необходим другой вариант описания решений (доказательств). Причем, безусловно, реализуемый в кибернетическом пространстве. До сих пор мы исчерпывали только ресурсы человеческого мышления, не отягченного компьютером. Этот вариант решений можно назвать алгоритмическим, хотя это название применимо и ко все предыдущим эпохам развития математики (как до, так и после Ал-Хорезми, введшего понятие алгоритма около тысячи лет назад). Ведь запись решения того же квадратного уравнения (или кубического) - тоже алгоритм, но очень легко реализуемый в уме. А вот классы задач, с которыми имеет дела и на которых обламывает зубы современная математика, уже не могут быть решены никаким, даже очень изощренным, человеческим умом. Нужно много умов, помноженных на компьютеры. И тут уже необходима максимально верифицируемая матодика выполнения "доказательств" и производства "выкладок" именно компьютерным путем. И только таким путем можно было бы решить до максимально возможных пределов ту задачу классификации групп, которую приводил в качестве примера автор. и тогда цепочка последовательных фолрму какого либо "доказательства" бУдет иметь вид цепочки последовательно примененных алгоритмов вычислений с приведенными многотысячелистовыми распечатками результатов и трассировок (по необходимости), если говорить упрощенно. Собственно говоря, я не сомневаюсь, что такие методики уже работают, только пока еще в зачаточном состоянии, если вспомнить для сравнения путь развития современной высшей математики (в смысле развития нотации и формализации обработки данных и процессов работы), начиная с Ньютона и математиков-механиков-астрономов 18-го века.

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

    Пост Скриптум.
    Вообщето я просто сказал то же, что и автор статьи, только выпендрился сказать покороче и понепонятнее. Ну, просто эмоции выплеснул, сам давно об этом думаю, а давно уже слыхал про вычислительные методики в математических доказательствах, в смысле существования класса задач, к которым только так и можно приступаться.
    Ответить
    • NIRVANA > Конан-Варвар | 15.05.2008 | 09:30 Ответить
      В основаниях математики существуют серьезные проблемы. Но я разделяю мнение, что данные проблемы рано или поздно будут решены. Из гипотезы периодичности радикалов, несводимых к целым числам (статья "постижение иррационального": http://www.exponenta.ru/educat/news/art.asp), следует, что для кв. корня из 2 выполняется тождество приближения с недостатком и избытком - 1,99(9)=2=2,00(0)1. Если допустить такую формулировку, то можно получить непротиворечивую систему десятичного счисления, которую можно представить геометрически.
      Ответить
      • anton > NIRVANA | 13.10.2008 | 17:42 Ответить
        "Более непротиворечивую", чем арифметика Пеано? С использованием таких сложных конструкций как радикалы и предельные переходы? Или опираясь на непротиворечивость Евклидовой геометрии на плоскости?
        Но до сих пор непротиворечивость геометрии сводили к арифметике, а не наоборот.
        Ответить
      • ananas > NIRVANA | 15.03.2012 | 19:01 Ответить
        Бред!
        Ответить
    • ananas > Конан-Варвар | 15.03.2012 | 09:53 Ответить
      "Ал-Хорезми, введшего понятие алгоритма около тысячи лет назад"

      Никакого понятия алгоритма Ал-Хорезми не вводил. Алгоритмы были названы алгоритмами В ЧЕСТЬ Ал-Хорезми
      Ответить
  • morfius  | 06.05.2007 | 15:08 Ответить
    Математика абстрагирует действительность до такой степени,что она(действительность) становиться понятной человеческому мозгу!
    PS. Пожалуй соглашусь с автором в том,что нельзя доверять доказательство компьютеру-могут быть ошибки в програмном обеспечении,и даже если напишут идеальное ПО,можно усомниться в истинности алгоритма из-за открытия новых теорем,новых найденых "дыр" в теории.
    Ответить
    • Academon > morfius | 31.01.2012 | 17:51 Ответить
      Математика абстрагирует действительность до такой степени,что она(действительность) становиться понятной человеческому мозгу?!
      Может имеется ввиду какой-то необычный мозг?
      Т.к. все ровно наоборот.
      Тот самый, сакраментальный, пример о невозможности деления на нуль - отражение утраты математикой своей цели - описания мира. Как было резонно замечено - деление это распределение между кем-то и кем-то.
      А если нет никого - то и процесс распределения не имеет смысла. В реальности это объективный факт, а в математике.. дай бох условное понятие. И это только примитивный арифметический случай.

      Математика упрощает объекты избавляясь от их несущественного описания. Но упрощение это всегда потеря какой-то информации. В результате приходится принимать некоторые положения как аксиомы, а не как объективно доказуемые параметры.
      Ответить
  • morfius  | 06.05.2007 | 15:22 Ответить
    Природа и вся действительность настолько сложна,что можно усомниться в том,что все законы выражаются через сложение.(Если говорить абстрактно:умножение-сколько раз сложить,чтобы получить некоторую величину,деление-сколько раз нужно сложить некоторую величину,чтобы получить делимое...и так далее)Может быть ввести в действие новое алгебраическое действие-созидание(частным случаем этого действия будет сложение).Появиться новая математика;и получим новые проблемы :)
    Ответить
  • ferst  | 01.03.2008 | 13:05 Ответить
    То, что было написано мною год назад, удалено. Сегодня у меня уже есть другой ответ по теме статьи.

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

    Изменено 22.07.09г.
    Ответить
  • magistr  | 09.11.2009 | 18:18 Ответить
    В общем всё нормально. Статья мне понравилась. Вот если бы автор ещё показал чем он занимается, конкретно, в математике... А так, вполне сносная философская заявка ещё на одну тему для околоматематических рассуждений.
    Ответить
  • VladNSK  | 04.11.2010 | 23:16 Ответить
    Прочитал статью с удовольствием.

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

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

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

    Тут очень важно то, что при таком подходе не нужно будет проверять саму программу (ее алгоритм). Более того, вполне может случиться так, что в программе есть ошибки, но тем не менее она может напечатать верное доказательство (если повезет).

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

    Программа сработала очень быстро и выдала на экран около двух десятков строк. И она нашла верное решение! Более того, она нашла ДВА решения, что было для меня совершенно неожиданно. Оказалось, что у этой задачки есть два решения: они похожи, но всё-таки различны. И самое важное, что анализируя строчки, выданные программой, было видно, что других решений быть не может. Иными словами, напечатанный программой текст был строгим математическим доказательством, что у задачи о волке, козе и капусте есть ровно два решения, и больше решений нет.

    Я понимаю, что есть проблема переусложнения, то есть найденное компьютером доказательство, выданное на бумагу, может быть столь длинным, что десять лучших математиков не смогут проверить его за всю свою жизнь. Но и в этом случае, все-таки лучше проверять само доказательство, напечатанное на бумаге, чем проверять алгоритм, с помощью которого это доказательство было найдено.
    Ответить
  • voidcaller  | 12.03.2013 | 10:29 Ответить
    Теорема Геделя легко понимается и принимается прикладными математиками, но костью в горле стоит математикам-теоретикам и "игрокам в бисер". Говорю как мех-матовец, разобравший метод форсинга для континуум гипотезы, потративший на это полгода жизни. Уж больно хотелось мне на 2-м курсе разобраться в том, что такое математика в свете теоремы о неполноте. Тогда ничего лучше бесконечной системы вложенных моделей, начиная с арифметики, каждая из последующих моделей доказывающая "истинные, но недоказуемые" утверждения нижележащих моделей, в голове не сложилось.

    Теперь же я понимаю, что теорема Геделя - это способ "заземления" зазнавшихся теоретиков, считающих, что в их переусложненных конструкциях есть какой-то "собственный смысл и красота". А на самом деле, Математика это Язык! Но ни в коем случае не язык Богов, описывающий совершенную вселенную. Математика - лучший язык Людей для приближенного моделирования экспериментально постигаемой Физической Реальности. Нет ничего противоречивого в том, что грубая простая модель Реальности (например арифметика Пеано) позволяет сформулировать больше утверждений, чем может доказать. Если мы понимаем, что никакая модель не может быть 100% адекватна, бессмысленна и борьба за утопическую "всегда правоту" теорем, вместо поиска баланса между простотой и предсказательной силой приближенной математической модели.

    Деление на 0 замечательный пример. Много столетий +-*/ и дробей хватало всем. Потребовалось вслед за Ньютоном описывать более сложную физику, и развили теорию пределов, где "пределы вида 0/0" это нормальный случай. Потребовалось в Астрономии и "разрешили" формальные (не сходящиеся в смысле 1-го курса) ряды. Потребовалось чтобы БЫЛИ решения у важных физикам уравнений в частных производных и появились обобщенные функции. И т.д. и т.п.

    Пока "философы математики" и "математики-теоретики" спорят, караван науки спокойно проходит мимо.
    Ответить
  • Slavavecher  | 12.08.2013 | 18:27 Ответить
    Вы меня извените за возможную без грамотность мне бы узнать про характеристики геометрических чисел и геометрическую математику где это можно сделать
    Ответить
  • роткив  | 26.02.2014 | 20:25 Ответить
    куда движется математика-к своим физическим истокам и к соответствию к ним,где ее главный результат решения это энергии-движений. вот так мужики, круг замыкается на точности оборота.
    Ответить
  • meschjanov  | 13.11.2014 | 20:13 Ответить
    Девиз: Математический аппарат - это аналитическая система, предназначенная для моделирования, а в дальнейшем и построения реальных физических систем или объектов. Фундаментом МА являются множества. Множества состоят из элементов-объектов. Объекты не только должны иметь абстрактную символику, например числовую, но и физическую интерпретацию, т.е. обладать физическими свойства. Так упорядоченное множество натуральных чисел N с нулевым элементом расположенных в виде точек на луче одномерного полупространства интерпретируются упорядоченным набором масс физического пространства. Такая статическая формальная система, состоящая из непротиворечивых элементов непротиворечива. В такой непротиворечивой числовой системе отсутствуют отрицательные числа, так как в физическом мире отсутствует отрицательная масса, она может равняться нулю "0" или не нулю. Логически это утверждает формула: E=mС2. Поэтому числовая система не обладает симметрией, а значит и неполнотой. Других числовых систем в МА не существует по условию второго логического закона непротиворечия. Элементы множеств отрицательных -N и положительных +N чисел одномерного пространства R1 имеют противоположные знаки-аналоги направлений. По условию построения вектора число со знаком - является векторной величиной, ВЕКТОР – это отрезок состоящий как минимум из двух точек (точки начала «0» и точки конца «1») обладает дуализмом. Так и комплексное число (геометрическая точка на плоскости) обладает одновременностью "мнимого" и "действительного" числа, или обладает одновременностью лог."1" и лог."0",что запрещает закон ЗИТ формальной системы МА. Какой там вопрос о непротиворечивости формальной системы, которую пытаются разрешить или доказать академики, когда вирус противоречий в МА разрушает всю существующую формальную систему МА, а они этого не видят, или не замечают. Вот вам реальный пример: Каким образом и по сей день существует МАФЛ (Математический аппарат формальной логики) с элементами-объектами противоречивой структуры (Вектором и Комплексным числом)? И почему до сих пор в МА существует «мнимое» число? Какова его физическая сущность? Если это интересно, я покажу и предоставлю вам его физический аналог, т.е. вопрос, как убрать "мнимость" из математического аппарата решается. Или такой пример из упорядоченного множества целых чисел: существует положение, что -3 < +3, знак «<» утверждает, что одно количество меньше другого, а значит, их сумма должна быть больше большего из слагаемых чисел, т.е. сумма ∑ >3 - так утверждает закон натуральных чисел, а она равна «0». Получается нарушение закона, значит расширение множества натуральных чисел до множества целых чисел неправомерно. Это расширение формальной системы N0 на сопредельную территорию незаконно и приводит в физическом мире к войне, а в МАФЛ к логическим противоречиям.
    Ответить
  • Valery Uzdin  | 28.01.2015 | 00:57 Ответить
    Уважаемые Дамы и Господа!Предлагаю математические исследования и разработки и детальное их описание посвященные новому направлению в теории распознавания состояний, где совместно существуют три взаимосвязанных множества:параметров,диагнозов состояний и проверок этих состояний,причем отличительной особенностью этого направления
    является то,что области диагнозов существенно пересекаются из-за наличия наряду с недостаточным числом информативных параметров,параметров неспецифичных.
    Предложен новый,вероятностно-метрический подход.Даны его основные понятия,определения и принципы распознавания состояний,на основе которых созданы эффективные методы математической диагностики,которые могут быть применены в самых разных областях:ранней диагностике онкологических и хронических заболеваний,обнаружении и выявлении причин неисправного состояния сложных,технических объектов,обнаружения сигналов на фоне помех,поиске полезных ископаемых,прогнозировании землетрясений,прогнозе состояний в сфере экономики, социологии и других.
    Изложение,детальное описание методов диагностики,ведется на примере возможного использования предложенных методов для раннего распознавания рака и хронических заболеваний по привычным анализам крови и мочи.
    Дается теоретическое обоснование такой возможности–трансформации неспецифичных,каждого в отдельности параметров крови в специфичные для раковых и нераковых диагнозов,достигаемой применением новых математических решений на комплексе параметров.
    Исследования и вся методика предназначена для кибернетиков,специалистов в области технической и медицинской диагностики,знакомых с теорией распознавания образов.
    Мои исследования и методы ранней диагностики,адресованы также широкому
    кругу специалистов,занимающихся решением указанных выше задач.
    Методы математической диагностики перспективные,заслуживающие тщательного изучения и анализа,с целью дальнейшего их применения и внедрения в практике!
    Хотелось бы,чтобы лица,организации,инвесторы и специалисты заинтерессованные в этом новом направлении диагностики подумали над этой проблемой.Я же готов к совместной работе!

    C Уважением,УЗДИН!

    PS: Контакт по эл.почте: usdin@mail.ru (Skype- valery.uzdin)
    Ответить
Написать комментарий
Элементы

© 2005-2017 «Элементы»