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

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


Семинар «Глобус» Московского Независимого Университета. Заседание 6 марта 2003 года

С.Н.Артемов (МГУ и CUNY Graduate Center, New York)
Может ли классическая математика мыслить интуиционистски?
Интуиционистское направление в математике возникло в работах Брауэра, а также Кронекера, Вейля и других. Согласно Брауэру, интуиционистская истинность есть ничто иное, как доказуемость. Нетрудно видеть, что, скажем, логический закон исключенного третьего «А или не А» неверен интуиционистски, т.к. утверждает, что для любого высказывания либо оно само, либо его отрицание доказуемо.

В начале 1930-х годов Колмогоров и Гейтинг предложили неформальное определение интуиционистской истинности по Брауэру на основе понятия доказательства; это определение стало общепринятой семантикой для интуиционистской логики. Естественная математическая задача нахождения точной формулировки для семантики Брауэра-Гейтинга- Колмогорова привлекла большое внимание специалистов.

Принципиальное продвижение было сделано в работах Геделя 1933 и 1938 годов, однако, задача оставалась нерешенной из-за возникших трудностей, казавшихся непреодолимыми. Позже были найдены другие, искусственные модели интуиционистской логики, которая выросла в мощную математическую дисциплину, тесно связанную с приложениями. Безуспешность попыток найти точную доказуемостную семантику интуиционистской логики поддерживала идею о необходимости новых оснований математики.

Докладчику удалось, соединив результаты Геделя и современную технику теории доказательств, завершить решение задачи о классической доказуемостной семантике для интуиционистской логики, начатое Геделем. Значение найденной при этом логики доказательств выходит за пределы оснований математики. Она устанавливает неожиданную связь между ранее далекими разделами логики и дает новый математический аппарат, вызывающий значительный интерес со стороны Computer Science.