Математическая логика
Формализация логики математическими методами. Включает теорию доказательств, теорию моделей, теорию рекурсии. Гёдель (1931) доказал неполноту арифметики.
Математическая логика
Логика предикатов
Расширение пропозициональной логики кванторами. ∀x (для всех), ∃x (существует). Предикаты: P(x) = "x чётное". Аксиоматика: Пеано (1889, арифметика), ZFC (1908, теория множеств). Теоремы Гёделя (1931): неполнота арифметики.
Теория моделей
Изучение интерпретаций формальных систем. Модель = множество + функции + отношения, удовлетворяющие аксиомам. Полнота (Гёдель, 1929): синтаксис ≡ семантика. Компактность: бесконечная теория непротиворечива ⇔ каждое конечное подмножество непротиворечиво.
Теория доказательств
Формализация математических доказательств. Натуральный вывод (Генцен, 1935), секвенциальное исчисление. Нормализация: устранение обходных путей. Соответствие Карри-Ховарда: доказательства ≃ программы (1958/1969). Автоматизация: Coq, Lean (proof assistants).
Теоремы неполноты
Гёдель (1931): революция в основаниях математики. Первая теорема: в достаточно богатой непротиворечивой системе есть истинные, но недоказуемые утверждения. Вторая: система не может доказать свою непротиворечивость. Следствия: пределы формализации, проблема остановки. Гёделева нумерация.
Теория вычислимости
Что можно вычислить алгоритмически? Машина Тьюринга (1936): универсальная модель вычислений. Тезис Чёрча-Тьюринга: всё интуитивно вычислимое = тьюринг-вычислимое. Неразрешимость: проблема остановки (Halting problem). Рекурсивные и рекурсивно перечислимые множества.