Математическая логика — раздел математики, изучающий формальные системы вывода, вычислимость и основания математики. Возникла в конце XIX века на стыке философии и математики из попыток формализовать математическое рассуждение. Основатели: Джордж Буль (булева алгебра, 1854), Готлоб Фреге (логика предикатов, 1879), Давид Гильберт (программа формализации, 1900-е), Курт Гёдель (теоремы о неполноте, 1931).
Представьте математику как игру: фигуры (символы), правила (аксиомы и вывод), цель (теоремы). Математическая логика изучает эту игру изнутри: какие правила непротиворечивы? Можно ли выиграть (доказать теорему) по данным правилам? Есть ли невыигрываемые партии (недоказуемые истины)?
Основные разделы
Теория доказательств — изучает формальные системы вывода (естественный вывод, секвенциальное исчисление). Герхард Генцен в 1934-1936 годах разработал методы анализа структуры доказательств: устранение сечения, нормализация, ординальный анализ непротиворечивости.
Теория моделей — связь синтаксиса (формулы) и семантики (структуры, в которых формулы истинны). Альфред Тарский в 1930-1950-х годах создал теорию истины, элементарной эквивалентности, категоричности. Теоремы: Лёвенхейма-Сколема, компактность, Морли о категоричности.
Теория вычислимости — формализация понятия алгоритма. Алан Тюринг (машины Тюринга, 1936), Алонзо Чёрч (λ-исчисление, 1936), Эмиль Пост (канонические системы, 1936) независимо создали эквивалентные модели вычислимости. Тезис Чёрча-Тюринга: интуитивное понятие "алгоритм" совпадает с вычислимостью на машине Тюринга.
Теория множеств — основание математики. Георг Кантор в 1870-1890-х годах создал теорию бесконечных множеств (континуум-гипотеза). Эрнст Цермело и Абрахам Френкель в 1908-1922 годах разработали аксиоматику ZFC, избегающую парадоксов (Рассела, Кантора). Независимость аксиомы выбора и континуум-гипотезы (Гёдель, 1938-1940; Коэн, 1963).
Кризис оснований математики
В начале XX века обнаружились парадоксы в наивной теории множеств. Парадокс Рассела (1901): Пусть R — множество всех множеств, не содержащих себя. Содержит ли R само себя? Если да, то по определению R не должно содержать себя. Если нет, то должно. Противоречие.
Три программы решения кризиса:
1. Логицизм (Фреге, Рассел): Вся математика сводится к логике. "Principia Mathematica" (Рассел, Уайтхед, 1910-1913) — попытка формализовать математику из логических аксиом. Провалилась: нужна аксиома бесконечности (нелогическая) и теория типов (громоздкая).
2. Формализм (Гильберт): Математика — игра символами, непротиворечивость доказывается финитными методами. Программа Гильберта провалилась после теоремы Гёделя о неполноте (1931): достаточно мощная система не может доказать собственную непротиворечивость.
3. Интуиционизм (Брауэр): Признаются только конструктивные доказательства. Отвергается закон исключённого третьего A ∨ ¬A (утверждение может быть ни истинным, ни ложным, если не доказано). Интуиционистская логика — основа конструктивной математики и теории типов.
Теоремы Гёделя о неполноте
Курт Гёдель в 1931 году доказал две теоремы, перевернувшие представления о математике.
Первая теорема о неполноте: В любой достаточно мощной непротиворечивой формальной системе (содержащей арифметику) существуют истинные, но недоказуемые утверждения. Гёдель построил формулу G: "Формула G недоказуема". Если G доказуема, получаем противоречие (формула утверждает обратное). Если G недоказуема, она истинна (именно это она и утверждает), но не доказуема.
Вторая теорема о неполноте: Система не может доказать собственную непротиворечивость (если она непротиворечива). Удар по программе Гильберта: финитное обоснование математики невозможно изнутри системы.
Следствия: Математика неполна (не всё доказуемо), но это не катастрофа — можно расширять системы, добавляя новые аксиомы (например, большие кардиналы в теории множеств).
Теория вычислимости
Машина Тюринга (1936) — абстрактная модель компьютера: бесконечная лента, головка, конечное число состояний. Машина читает символ, пишет новый, двигает головку влево/вправо, меняет состояние. Функция вычислима, если существует машина Тюринга, вычисляющая её.
Проблема остановки (Тюринг, 1936): Невозможен алгоритм, определяющий для произвольной программы и входа, остановится ли программа. Доказательство диагонализацией: предположим, есть алгоритм H(P, x), возвращающий "остановится" или "зациклится". Построим программу D, которая на входе P вызывает H(P, P) и зацикливается, если H вернул "остановится", иначе останавливается. Что делает D(D)? Противоречие.
Арифметическая иерархия: Классификация проблем по сложности (не вычислимые, но различаются количеством кванторов в определении). Σ₁ (∃-проблемы, перечислимы), Π₁ (∀-проблемы, коперечислимы), Σ₂, Π₂ и т.д. Проблема остановки — Σ₁ (∃n(машина остановится за n шагов)).
Аксиоматика ZFC
Цермело-Френкелевская теория множеств с аксиомой выбора — стандартная основа математики. 9 аксиом:
1. Экстенсиональность: Множества с одинаковыми элементами равны.
2. Пустое множество: Существует ∅ (не содержит элементов).
3. Пара: Из x и y можно построить {x, y}.
4. Объединение: Из семейства множеств можно построить их объединение.
5. Степень: Из x можно построить 2^x (множество всех подмножеств).
6. Схема выделения: Из множества можно выделить подмножество по свойству (избегает парадокса Рассела).
7. Схема подстановки: Образ множества при функции — множество.
8. Бесконечность: Существует бесконечное множество (натуральные числа).
9. Аксиома выбора: Из каждого непустого множества можно выбрать элемент.
Независимость аксиомы выбора: Гёдель (1938) доказал: если ZF непротиворечива, то ZFC непротиворечива. Пол Коэн (1963, метод форсинга) доказал: если ZF непротиворечива, то ZF + ¬AC тоже. Следствие: аксиому выбора нельзя доказать или опровергнуть из ZF.
Континуум-гипотеза
Кантор (1878): Мощность континуума (множества вещественных чисел) 2^ℵ₀. Континуум-гипотеза (CH): 2^ℵ₀ = ℵ₁ (нет промежуточных мощностей между счётным и континуумом).
Гёдель (1938) доказал: если ZFC непротиворечива, ZFC + CH непротиворечива. Коэн (1963) доказал: если ZFC непротиворечива, ZFC + ¬CH тоже. Континуум-гипотеза независима от ZFC — неразрешима стандартными аксиомами.
Современные исследования: большие кардиналы (аксиомы, расширяющие ZFC) могут разрешить CH. Дескриптивная теория множеств изучает "естественные" множества (борелевские, проективные), для которых CH может быть разрешима.
Применение в информатике
Языки программирования: Теория типов (основанная на логике) — база Haskell, OCaml, Rust. Зависимые типы (Coq, Agda) — доказательства через программы (изоморфизм Карри-Ховарда).
Верификация: Формальное доказательство корректности программ (seL4 — верифицированная ОС, CompCert — верифицированный компилятор C). Используют теорию доказательств и теорию моделей.
Базы данных: Логика предикатов — основа SQL. Реляционная алгебра (Кодд, 1970) — применение теории множеств и логики к данным.
Искусственный интеллект: Автоматическое доказательство теорем (ATP), планирование, логическое программирование (Prolog). Резолюция Робинсона (1965) — основа многих ATP-систем.