Курс математической логики, КТ, осень 2025

Материалы

• Конспект 2018 года
• Конспект 2011 года
• Теоретические домашние задания
• Краткая инструкция по утилите make
• О способе оценивания курса
• Вопросы к экзамену

Лекция 1

Что такое логика и математическая логика. Исчисление высказываний

• История вопроса. Логика.
• Парадоксы теории множеств, необходимость формализации математики, программа Гильберта.
• Метаязык и предметный язык. Язык исчисления высказываний.
• Теория моделей, оценка высказываний.
• Теория доказательств, доказательства, выводимость.
• Теорема о корректности исчисления высказываний.
• Формулировка теоремы о дедукции.

Где почитать

• Н.К. Верещагин, А. Шень. Лекции по математической логике и теории алгоритмов. Языки и исчисления. https://www.mccme.ru/free-books/shen/shen-logic-part2-2.pdf
• Конспекты 2011 и 2018 года по логике.
• Хрестоматия по истории математики. Арифметика и алгебра. Теория чисел. Геометрия. Пособие для студентов физ.-мат. фак. пед. ин-тов. Под ред. А.П. Юшкевича. - М.: Просвещение, 1976. - 318 с.
• О противоречиях в математическом анализе: Джордж Беркли, «Аналитик. Беседа, адресованная неверному математику: где исследуется, являются ли объект, принципы и выводы современного анализа более отчетливо задуманы или более явно выведены, чем религиозные мистерии и точки веры» --- М.: Мысль, 1978

Лекция 2

Теоремы об исчислении высказываний, интуиционистское исчисление высказываний

• Теорема о дедукции
• Теорема о полноте исчисления высказываний
• Интуиционистское исчисление высказываний: история
• BHK-интерпретация связок
• Формализация ИИВ через изменение 10 схемы аксиом
• Нормальный вывод
• Общая топология, базовые определения
• Топологическое пространство как модель ИИВ

Где почитать

• Н.К. Верещагин, А. Шень. Лекции по математической логике и теории алгоритмов. Языки и исчисления. https://www.mccme.ru/free-books/shen/shen-logic-part2-2.pdf
• Конспекты 2011 и 2018 года по логике.
• О. Я. Виро, О. А. Иванов, Н. Ю. Нецветаев, В. М. Харламов. Элементарная топология. --- М.: Издательство МЦНМО, 2010
• В.Е.Плиско, В.Х.Хаханян, Интуиционистская логика, Мех-Мат МГУ 2009 http://logic.math.msu.ru/wp-content/uploads/plisko/intlog.pdf
• Morten Heine B. Sørensen, Pawel Urzyczyn: Lectures on the Curry-Howard Isomorphism https://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard.pdf

Лекция 3

Модели интуиционистского исчисления высказываний

• Мотивационный пример: Изоморфизм Карри-Ховарда
• Непрерывность, компактность
• Решётки, алгебра Гейтинга и булева алгебра
• Алгебра Линденбаума

Где почитать

• О. Я. Виро, О. А. Иванов, Н. Ю. Нецветаев, В. М. Харламов. Элементарная топология. --- М.: Издательство МЦНМО, 2010
• В.Е.Плиско, В.Х.Хаханян, Интуиционистская логика, Мех-Мат МГУ 2009 http://logic.math.msu.ru/wp-content/uploads/plisko/intlog.pdf
• Morten Heine B. Sørensen, Pawel Urzyczyn: Lectures on the Curry-Howard Isomorphism https://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard.pdf

Лекция 4

Теоремы об интуиционистском исчислении высказываний

• Модели Крипке
• Теорема о нетабличности ИИВ
• Теорема о дизъюнктивности ИИВ
• Теорема о разрешимости ИИВ

Где почитать

• В.Е.Плиско, В.Х.Хаханян, Интуиционистская логика, Мех-Мат МГУ 2009 http://logic.math.msu.ru/wp-content/uploads/plisko/intlog.pdf
• Morten Heine B. Sørensen, Pawel Urzyczyn: Lectures on the Curry-Howard Isomorphism https://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard.pdf

Лекция 5

Исчисление предикатов

• Категорические силлогизмы (общее понятие, примеры)
• Язык исчисления предикатов
• Теория моделей, теория доказательств
• Теорема о дедукции
• Теорема о корректности

Где почитать

• Бочаров В.А., Маркин В.И. Введение в логику: учебник. -- М.: ИД <<Форум>>: ИНФРА-М. 2008.
• Н.К. Верещагин, А. Шень. Лекции по математической логике и теории алгоритмов. Языки и исчисления. https://www.mccme.ru/free-books/shen/shen-logic-part2-2.pdf
• Стефан К. Клини, Математическая логика. Перевод с английского Ю.А. Гастева. Под редакцией Г.Е. Минца. Москва: Издательство «Мир». Редакция литературы по математическим наукам, 1973

Лекция 6

Теорема о полноте исчисления предикатов

• Непротиворечивые множества формул
• Модели для непротиворечивых множеств формул
• Теорема Гёделя о полноте исчисления предикатов
• Следствие о полноте исчисления предикатов
• Непротиворечивость исчисления предикатов
• Теорема Гёделя о компактности бескванторного подмножества исчисления предикатов

Где почитать

• П.Дж. Коэн, Теория множеств и континуум-гипотеза --- М.: Изд-во <<Мир>>, 1969.
• Н.К. Верещагин, А. Шень. Лекции по математической логике и теории алгоритмов. Языки и исчисления. https://www.mccme.ru/free-books/shen/shen-logic-part2-2.pdf

Лекция 7

Неразрешимость исчисления предикатов, аксиоматика Пеано

• Машина Тьюринга
• Неразрешимость исчисления предикатов
• Аксиоматика Пеано
• Порядок теории. Теории первого порядка
• Формальная арифметика

Где почитать

• П.Дж. Коэн, Теория множеств и континуум-гипотеза --- М.: Изд-во <<Мир>>, 1969.
• Джон Хопкрофт, Раджив Мотвани, Джеффри Ульман. Введение в теорию автоматов, языков и вычислений --- М.: Вильямс, 2002.

Лекция 8

Арифметизация логики

• История вопроса, работы Лейбница
• Рекурсивные функции
• Функция Аккермана, доказательство того, что она не является примитивно-рекурсивной
• Выразимость отношений и представимость функций в формальной арифметике
• Бета-функция Гёделя, теорема о представимости рекурсивных функций в арифметике
• Гёделева нумерация, теорема о рекурсивности представимых в формальной арифметике функций.

Где почитать

• Готфрид Вильгельм Лейбниц, Сочинения в четырёх томах, том 3 --- М.: Изд-во <<Мысль>>, 1984
• П.Дж. Коэн, Теория множеств и континуум-гипотеза --- М.: Изд-во <<Мир>>, 1969.
• Н.К. Верещагин, А. Шень. Лекции по математической логике и теории алгоритмов. Языки и исчисления. https://www.mccme.ru/free-books/shen/shen-logic-part2-2.pdf
• Э. Мендельсон, Введение в математическую логику --- М.: Изд-во <<Наука>>, 1971.

Лекция 9

Общие свойства формальной арифметики, теоремы Гёделя о неполноте

• Обзор общих свойств формальной арифметики (корректность, непротиворечивость, полнота, разрешимость).
• Классическая модель формальной арифметики, её корректность.
• Омега-непротиворечивость, семантическая и синтаксическая полнота.
• Первая теорема Гёделя о неполноте арифметики.
• Теорема Гёделя о неполноте арифметики в форме Россера.
• Consis.
• Условия выводимости Гильберта-Бернайса-Лёба.
• Лемма об автоссылках, другая формулировка теоремы Гёделя о неполноте арифметики.
• Вторая теорема Гёделя о неполноте арифметики.

Где почитать

• П.Дж. Коэн, Теория множеств и континуум-гипотеза --- М.: Изд-во <<Мир>>, 1969.
• Гилберт Д., Бернайс П., Основания математики --- М.: Изд-во <<Наука>>, 1982.

Лекция 10

Теория множеств

• Неразрешимость формальной арифметики, теорема Тарского о невыразимости истины.
• История возникновения теории
• Конструктивные аксиомы теории множеств, аксиома бесконечности.
• Дизъюнктное объединение множеств.
• Алгебраические типы
• Ординалы

Где почитать

• П.Дж. Коэн, Теория множеств и континуум-гипотеза --- М.: Изд-во <<Мир>>, 1969.
• Конспекты 2011 и 2018 года по логике.
• Френкель А.А., Бар-Хиллел И. Основания теории множеств. --- УРСС, 2010

Лекция 11

Ещё об ординалах, ещё аксиомы теории множеств.

• Операции на ординалах.
• Произведение ординалов, декартово произведение множеств.
• Степени ординалов.
• Аксиома выбора, аксиома подстановки, аксиома фундирования.

Где почитать

• Френкель А.А., Бар-Хиллел И. Основания теории множеств. --- УРСС, 2010
• П.Дж. Коэн, Теория множеств и континуум-гипотеза --- М.: Изд-во <<Мир>>, 1969.
• Chris Taylor, The Algebra of Algebraic Data Types. https://www.youtube.com/watch?v=YScIPA8RbVE

Лекция 12

Алгебраические типы, мощность множеств

• Мощность множеств и кардинальные числа
• Теорема Кантора-Бернштейна
• Диагональный метод и теорема Кантора
• Континуум-гипотеза
• Теорема Лёвенгейма-Сколема
• Парадокс Сколема

Где почитать

• Френкель А.А., Бар-Хиллел И. Основания теории множеств. --- УРСС, 2010
• П.Дж. Коэн, Теория множеств и континуум-гипотеза --- М.: Изд-во <<Мир>>, 1969.
• Chris Taylor, The Algebra of Algebraic Data Types. https://www.youtube.com/watch?v=YScIPA8RbVE

Лекция 13

Аксиома выбора

• Формулировки аксиомы выбора: определения, лемма Цорна, теорема Цермело
• Доказательство эквивалентности (кроме вывода леммы Цорна)
• Использование аксиомы выбора (на примере эквивалентности пределов по Гейне и по Коши)
• Теорема Диаконеску (ИИП + ZF влечёт исключённое третье)
• Ослабленные варианты аксиомы
• Усиленный вариант аксиомы: универсум фон-Неймана и аксиома конструктивности.

Где почитать

• П.Дж. Коэн, Теория множеств и континуум-гипотеза --- М.: Изд-во <<Мир>>, 1969.
• Конспекты 2011 и 2018 года по логике.
• Френкель А.А., Бар-Хиллел И. Основания теории множеств. --- УРСС, 2010

Лекция 14

Трансфинитная индукция. Доказательство непротиворечивости формальной арифметики

• Математическая и трансфинитная индукция, различные формулировки.
• Система S-бесконечность
• Сечения. Теорема об устранении сечений
• Теорема о непротиворечивости формальной арифметики

Где почитать

• П.Дж. Коэн, Теория множеств и континуум-гипотеза --- М.: Изд-во <<Мир>>, 1969.
• Френкель А.А., Бар-Хиллел И. Основания теории множеств. --- УРСС, 2010
• Э. Мендельсон, Введение в математическую логику --- М.: Изд-во <<Наука>>, 1971.

Лекция 15

Метод резолюции

• Постановка задачи
• Сколемизация
• Эрбранов универсум
• Теорема Эрбрана
• Метод резолюций
• Унификация
• Метод резолюций для исчисления предикатов
• Использование метода резолюций

Где почитать

• Ч. Чень, Р. Ли, Математическая логика и автоматическое доказательство теорем --- М.: Изд-во <<Наука>>, 1983.

Лекция 16

Лямбда-исчисление

• Бестиповое лямбда-исчисление
• Натуральный вывод
• Импликационный фрагмент интуиционистского исчисления высказываний
• Просто-типизированное лямбда-исчисление, изоморфизм Карри-Ховарда
• Комбинаторы, изоморфизм Карри-Ховарда для гильбертового исчисления

Где почитать

• Morten Heine B. Sørensen, Pawel Urzyczyn: Lectures on the Curry-Howard Isomorphism https://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard.pdf

Лекция 17

Модальная и темпоральная логика. Проверка на моделях (model checking).

• Модальные логики.
• Постановка задачи
• Линейная темпоральная логика
• Пример простой программы со сложной логикой
• Примеры реализации, язык SPIN

Где почитать

• Mordechai (Moti) Ben-Ari. A Primer on Model Checking https://spinroot.com/spin/Doc/p40-ben-ari.pdf
• Christel Baier and Joost-Pieter Katoen. Principles of Model Checking https://is.ifmo.ru/books/_principles_of_model_checking.pdf