Математическая логика

Одной из основных задач математической логики является изучение математического доказательства рассуждений. При этом имеются исходные, принимаемые без доказательства положения (аксиомы), из которых с помощью определенных принципов рассуждений выводятся заключения. Их истинность зависит как от самих исходных положений, так и от использованных в процессе доказательства принципов рассуждений. Развиваемые таким образом математические теории называются аксиоматическими; с ними связаны важнейшие разделы математической логики, изучающие вопросы независимости аксиом и непротиворечивости теорий.

Основоположником аксиоматической теории математической логики является российский математик, профессор Казанского университета Н.И.Лобачевский. Классический пример этой теории – евклидова геометрия, построенная на нескольких постулатах Евклида, в число которых входит пятый постулат о параллельных прямых. Безуспешные попытки вывести пятый постулат Евклида из остальных аксиом геометрии побудили Лобачевского высказать положение о его независимости от остальных аксиом евклидовой геометрии.

Он разработал новую геометрию (1826), известную как геометрия Лобачевского (см. Лобачевского геометрия), в которой данный постулат был заменен утверждением, прямо противоположным исходному. Позднее итальянский математик Е.Бельтрами построил модель геометрии (1868), в которой выполняются аксиомы Лобачевского, а немецкий математик Ф.Клейн привел строгое доказательство непротиворечивости геометрии Лобачевского (1872). Таким образом, была установлена независимость пятого постулата от остальных аксиом геометрии Евклида.

Важные результаты математической логики были получены в ХХ в. в теории множеств: австрийский математик К.Гедель доказал непротиворечивость аксиомы выбора и проблемы континуума с аксиомами теории множеств (1934), американский математик П.Коэн установил их независимость от аксиом теории множеств (1963).

При проведении исследований в математической логике строятся формальные системы, определенным образом связанные с рассматриваемой математической теорией. Идея такого подхода принадлежит немецкому математику Д.Гильберту. Его работе (1922–1939) предшествовала разработка алгебры логики в трудах английского логика Дж.Буля, немецких математиков Э.Шредера и Г.Фреге, итальянского математика Дж.Пеано и профессора Казанского университета астронома П.С.Порецкого. Работа Порецкого «О способах решения логических равенств и об обратном способе математической логики» (1884) сыграла значительную роль в развитии алгебры логики. На основе этой работы ученым впервые в России был прочитан курс математической логики в Казанском университете (1887).

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

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

С 1960-х гг. в Казанском университете под руководством Н.К.Замова ведутся исследования в области теории доказательств, прикладной математической логики, теории искусственного интеллекта, синтеза программ и методики преподавания программирования. В методе резолюций получена стратегия упорядочения термов, которая является разрешающей процедурой для широкого класса формул исчисления предикатов; разработаны варианты метода резолюций для модальных логик. На основе метода резолюций создана программа доказательства теорем, с помощью которой в автоматическом режиме возможно доказательство многих теорем модальных логик и теории множеств (В.Ю.Базылев, В.Ю.Михайлов).

Математическая логика имеет принципиальную связь с теорией алгоритмов. В середине ХХ в. в работах английского математика А.Тьюринга и американского математика А.Черча было уточнено понятие алгоритмически вычислимой функции, что позволило доказать алгоритмическую неразрешимость многих математических проблем, для которых ранее не удавалось найти алгоритмы решения.

В 1970-е гг. ученые Казанского университета под руководством М.М.Арсланова классифицировали алгоритмически неразрешимые теории по их степеням неразрешимости; нашли критерии принадлежности математических проблем конкретным уровням возникающей при такой классификации иерархии; получили результаты в разработке алгебраические структуры упорядочения степеней неразрешимости по основным сводимостям.

Клини С.К. Математическая логика. Москва, 1973.

Арсланов М.М. Рекурсивное перечисление множества и степени неразрешимости. Казань, 1986.

Resolution methods for the decision problem. Berlin–New York, 1993.

Автор – М.М.Арсланов