Кафедра математической логики и теории алгоритмов

Механико-математического факультета МГУ


Теория доказательств и основания математики

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

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

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

Традиция исследований по теории доказательств на кафедре восходит к работам П. С. Новикова по формальной арифметике 1940-х годов и работам Ан. А. Маркова по конструктивной математике, которые были c успехом продолжены его учениками А. Г. Драгалиным и С. Н. Артёмовым (см. далее). долгое время работавшими на нашей кафедре В настоящее время в области теории доказательств работает профессор кафедры, чл.-корр. РАН Лев Дмитриевич Беклемишев, а также его ученики, Данияр Салкарбекович Шамканов и Федор Николаевич Пахомов (МИАН и факультет математики НИУ ВШЭ).

Исследования Л. Д. Беклемишева касаются формальной арифметики, связей между аксиомами арифметики и классами вычислимых функций, которые можно верифицировать с помощью тех или иных аксиом. Другое направление относится к изучению прогрессий Тьюринга — последовательностей теорий, получающихся каждый раз расширением системы аксиомой, выражающей её непротиворечивость. Эти результаты приводят к глубоким обобщениям теоремы Гёделя о неполноте и позволяют увидеть интересные математические (порядковые и алгебраические) структуры в мире арифметических теорий.

Ф.Н. Пахомов, защитивший кандидатскую диссертацию в 2015 году, в одной из своих последних работ исследовал остроумное понятие «медленной доказуемости», которое приводит к новому классу независимых утверждений более слабых, чем гёделевское утверждение о непротиворечивости формальной арифметики.

Д.С. Шамканов занимается структурной теорией доказательств, то есть наукой о построении формальных доказательств и о преобразованиях одного формального доказательства в другое. Недавно им был исследован новый интересный класс выводов — так называемые циклические выводы — которым позволяется до некоторой степени иметь «порочный круг». С помощью этого понятия, проходящего в опасной близости от противоречивости, он получил несколько впечатляющих результатов, относящихся к исследованию традиционных систем.

Исследованиями в области аксиоматики теории множеств занимаются наши выпускники, ученики В. А. Успенского: профессор нашей кафедры Василий Александрович Любецкий и профессор Владимир Григорьевич Кановей, работающие также в Институте проблем передачи информации РАН.

В течение столетий и даже тысячелетий математики в своих рассуждениях использовали интуитивные представления о бесконечно малых и бесконечно больших величинах. Формальное построение математики на основе теории действительных чисел обошлось без этих представлений. Однако математическим логикам удалось построить так называемый «нестандартный анализ», где бесконечно малые и бесконечно большие существуют и помогают доказывать теоремы обычного анализа. В. Г. Кановей и В. А. Любецкий ведут работы и в этом направлении.