Основы математической логики
Элементы теории алгоритмов[править]
1. Интуитивное понятие алгоритма, вычислимой функции. Ансамбли конструктивных объектов. Область возможных исходных данных. Область применимости алгоритма. Примеры алгоритмов. Вычислимая функция.
2. Модели вычислений. Машины Тьюринга. Машины с неограниченными регистрами (МНР). Тезис Чёрча.
3. Разрешимость, перечислимость подмножества ансамбля конструктивных объектов. Критерий разрешимости перечислимого множества (теорема Поста). Свойства перечислимых, разрешимых множеств. Теорема о графике вычислимой функции. Теорема о проекции.
4. Универсальная вычислимая функция. Невозможность вычислимой функции, универсальной для класса всех всюду определённых вычислимых функций. Главная универсальная вычислимая функция. Теорема о трансляторе (s-m-n-теорема).
Примеры неразрешимых проблем. Неразрешимость проблемы остановки. Примеры неразрешимых перечислимых множеств.
Многозначная (m-сводимость). Свойства m-сводимости. Теорема Райса о неразрешимости нетривиальных классов в.ф. Примеры применения теоремы Райса.
Диофантовы множества. Десятая проблема Гильберта и ее отрицательное решение.
Логика высказываний[править]
1. Язык логики высказываний. Логические связки и таблицы истинности. Приведение формул к дизъюнктивной и конъюнктивной нормальным формам. Булевы функции. Полные системы булевых функций. Теорема Поста. Полиномы Жегалкина.
2. Гильбертовский вариант исчисления для логики высказываний. Алфавит, формулы, схемы аксиом и правила вывода исчисления высказываний. Вывод, выводимая формула. Семантическая корректность исчисления высказываний.
Вывод из гипотез. Теорема о дедукции для исчисления высказываний. Теорема о семантической полноте исчисления высказываний.
3. Генценовский вариант исчисления для логики высказываний. Понятие секвенциального вывода. Эквивалентность гильбертовского и генценовского вариантов исчисления высказываний. Теорема об устранении сечения. Алгоритм поиска вывода в исчислении высказываний.
Логика первого порядка[править]
1. Язык первого порядка. Понятие переменной, предиката, квантора. Сигнатура языка первого порядка, терм, формула. Применение языков первого порядка для описания фрагментов естественных языков.
Примеры языков первого порядка: языки теории полей, групп, частичного упорядочения, язык арифметики.
2. Семантика языков первого порядка. Интерпретация языка первого порядка. Выполнимые формулы, общезначимые формулы. Равносильность формул языка первого порядка. Основные равносильности. Предваренные формулы. Приведение формулы к предваренной форме.
3. Исчисление предикатов. Схемы аксиом и правила вывода исчисления предикатов. Вывод из гипотез в исчислении предикатов. Теорема о дедукции для исчисления предикатов. Теорема о корректности исчисления предикатов.
Теорема Гёделя о полноте исчисления предикатов. Невозможность аксиоматизации предиката равенства в языке первого порядка. Нормальные модели. Исчисление предикатов с равенством, его корректность и полнота относительно нормальных моделей.
Неразрешимость исчисления предикатов.
4. Теории первого порядка. Примеры теорий первого порядка: теория равенства, теория плотного линейного порядка, теория групп, теория полей, арифметика Пеано.
Теорема Гёделя о полноте для теорий первого порядка. Теорема Лёвенгейма-Скулема. Теорема компактности для языков первого порядка.
Невозможность аксиоматизации свойства конечности в языке первого порядка. Существование счётных нестандартных моделей арифметики.
Логика второго порядка[править]
1. Логика 2-го порядка, основные отличия ее от логики 1-го порядка. Определение предиката равенства. Формула, выражающая конечность. Аксиоматизация арифметики. Неперечислимость логики второго порядка.
Неклассические логики[править]
1. Интуиционистская логика высказываний. Конструктивное понимание логических связок, семантика Крипке.
Аксиомы интуиционистского исчисления высказываний. Теорема о корректности и полноте интуиционистского исчисления высказываний относительно семантики Крипке.
Доказательство невыводимости законов исключенного третьего и снятия двойного отрицания в интуиционистском исчислении высказываний. Свойство дизъюнктивности для интуиционистской логики. Невозможность задания интуиционистских связок истинностными таблицами с конечным числом значений.
2. Многозначная логика.
3. Модальная логика. Язык модальной логики. Примеры модальностей в естественном языке. Системы аксиом для логик K, K4, S4, S5, GL, Grz. Семантика Крипке для модального языка. Классы шкал Крипке, соответствующие основным аксиомам логик K, K4, S4, S5, Grz. Полнота K, K4, S4, S5, Grz относительно семантики Крипке. Вложение интуиционистской логики высказываний в S4.
4. Временные операторы, языки временных логик. Логика данной шкалы времени. Примеры временных логик: логики линейного времени, логики ветвящегося времени. Перевод формул языка пропозициональной временной логики на языки классической логики I-го и II-го порядка. Пример неэлементарной временной логики. Разрешимость линейных временных логик. Временные логики и верификация программ.