Компьютерная логика (спецкурс, весна 2003)

Лектор: профессор С. Н. Артёмов.

Из двух направлений в математической логике — классического (Фреге, Гильберт, Гёдель, Тарский) и интуиционистского (Брауэр, Колмогоров, Карри, Чёрч) — последнее оказывает наибольшее влияние на области науки, лежащие вне пределов традиционной логики. Интуиционистская логика и функциональные исчисления были открыты в первой трети ХХ века как средства изучения оснований математики и впоследствии оказались мостом, соединяющим доказательства и вычислительные программы. К настоящему времени можно говорить о новом научном направлении «Компьютерная Логика», выросшем на интуиционистской традиции в математической логике и ставшем неотьемлемой частью как математической логики так и Computer Science.

Программа:

Интуиционистская логика: исходная семантика Брауэра-Гейтинта-Колмогорова. Исчисление. Модели.
Генценовские исчисления и естественный вывод.
Модальная логика, модели. Гёделевское сведение интуиционистской логики к модальной.
Типовая комбинаторная логика, типовое лямбда-исчисление. Изоморфизм Карри-Ховарда естественных выводов и типовых лямбда-термов.
Полиномы доказательств и формулы, несущие доказательства. Логика доказательств.
Решение задачи Гёделя о реализуемости модальной и интуиционистской логики в классической логике доказательств. Математическая форма семантики Брауэра-Гейтинта-Колмогорова
Функциональная логика доказательств.
Рефлекcивная комбинаторная логика и лямбда-исчисление.

Спецкурс будет читаться с 24 февраля по 7 марта 2003 года

понедельник	с 18:05	ауд. 12-12
четверг	с 18:05	ауд.13-04
пятница	с 16:20	ауд. 14-14

В некоторые дни возможно изменение аудитории на 13-05

Первая лекция состоится …>>

Страница спецкурса http://markov.math.msu.ru/rus/cl.htm

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

С.Н.Артемов (МГУ и CUNY Graduate Center, New York)

Может ли классическая математика мыслить интуиционистски?

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

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

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

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