Математическая логика и теория алгоритмов

Математические доказательства состоят из шагов, в которых одни утверждения выводятся из других. Но что такое «правильный» шаг? Пропозициональная логика даёт точный язык: синтаксис (как записывать формулы) и семантику (что они означают). Это фундамент, на котором стоят автоматические доказатели, к...

Индуктивное определение формул: 1. Каждая переменная p — формула. 2. Если φ — формула, то ¬φ — формула. 3. Если φ и ψ — формулы, то (φ ∧ ψ), (φ ∨ ψ), (φ → ψ), (φ ↔ ψ) — формулы. 4. Ничто другое не является формулой.

Интерпретация (оценка): функция I: {переменные} → {0, 1}. Расширяется на все формулы:

Следование: Γ ⊨ φ, если любая I, делающая все ψ ∈ Γ истинными, делает истинным φ.

Задача SAT (SATisfiability) — проверить, выполнима ли пропозициональная формула — NP-полна, но на практике решается за секунды для миллионов переменных с помощью современных SAT-солверов. Они работают с формулами в конъюнктивной нормальной форме (КНФ) и используют алгоритм DPLL и его расширения. ...

Дизъюнкт: дизъюнкция литералов: (l₁ ∨ l₂ ∨ ... ∨ lₖ). Единичный дизъюнкт: дизъюнкт из одного литерала.

КНФ (конъюнктивная нормальная форма): конъюнкция дизъюнктов: D₁ ∧ D₂ ∧ ... ∧ Dₘ. Любая пропозициональная формула приводима к КНФ (равновыполнимой, если использовать трансформацию Цейтина).

Алгоритм приведения к КНФ: 1. Устранить → и ↔: p→q ≡ ¬p∨q; p↔q ≡ (¬p∨q)∧(p∨¬q) 2. Загнать ¬ внутрь (законы де Моргана, двойное отрицание) 3. Применить дистрибутивность ∨ над ∧

В пропозициональной логике мы имеем два независимых понятия: семантика (что истинно при каждой оценке) и синтаксис (что выводится из аксиом по правилам). Теорема полноты утверждает их совпадение: всё семантически истинное доказуемо. Теорема корректности — обратное: всё доказуемое истинно. Вместе ...

Вывод из Γ: последовательность φ₁, ..., φₙ, где каждая φᵢ — аксиома, либо принадлежит Γ, либо получена из предыдущих по MP. Γ ⊢ φ — φ выводима из Γ.

Теорема корректности (Soundness): Γ ⊢ φ ⟹ Γ ⊨ φ. Доказательство: индукция по длине вывода. Аксиомы — тавтологии; MP сохраняет истинность.

Теорема полноты (Completeness, Пост 1921): Γ ⊨ φ ⟹ Γ ⊢ φ. Любое семантическое следствие — синтаксически доказуемо. Это означает: система аксиом «достаточна» для всей классической логики.

Пропозициональная логика не может выразить «все натуральные числа чётны» или «существует простое число». Логика первого порядка (ЛПП, FOL) добавляет кванторы ∀ и ∃, предикатные символы и функциональные символы — это язык современной математики. В ЛПП формулируются теория групп, арифметика, теория...

Сигнатура σ: множество предикатных символов P (с арностью n), функциональных символов f (с арностью n) и констант c (нульарные функции).

Свободные и связанные переменные: x свободна в φ, если она не в области действия кванторов по x. В ∀x P(x,y): x — связана, y — свободна.

Предложение (замкнутая формула): нет свободных переменных. Истинность не зависит от оценки.

Определения

Подстановка σ

— отображение переменных → термы. σ(t) — результат применения σ к терму t.

Как компьютер может доказывать математические теоремы? Метод резолюций (Робинсон, 1965) — алгоритм, который сводит проверку логического следования к поиску противоречия: мы отрицаем заключение, добавляем к посылкам, и пытаемся вывести пустой дизъюнкт ☐. Это основа языка Prolog и современных ATP-с...

Шаги: 1. Устранить → и ↔. 2. Загнать ¬ внутрь (де Морган, снятие двойного отрицания). 3. Переименовать переменные (каждый квантор — своя переменная). 4. Вынести кванторы (привести к предварённой форме). 5. Сколемизация: устранить ∃. ∃x P(x) → P(c) (новая константа Сколема); ∀y ∃x P(x,y) → ∀y P(f(...

Подстановка σ — отображение переменных → термы. σ(t) — результат применения σ к терму t.

Унификатор для множества пар {(s₁,t₁),...,(sₙ,tₙ)}: σ такой, что σ(sᵢ) = σ(tᵢ) для всех i.

В начале XX века Гильберт мечтал: формализовать всю математику в единой полной и непротиворечивой системе. Гёдель в 1930–31 годах показал, что это невозможно. Его теоремы — важнейший философский и математический результат XX века, ограничивающий силу любой формальной системы.

Теорема: φ логически истинна в ЛПП (выполнена во всех структурах) ⟺ φ выводима из аксиом ЛПП (стандартное исчисление предикатов).

Ключевая идея доказательства — лемма Хенкина: если Γ непротиворечива, строим «каноническую модель» из термов языка, расширенного «константами-свидетелями» для каждого ∃-предложения.

Следствие — нестандартные модели: Рассмотрим Th(ℕ) ∪ {c > 0, c > 1, c > 2, ...}. Каждое конечное подмножество выполнимо в ℕ (возьмём c достаточно большим). По компактности, всё множество имеет модель *ℕ с «бесконечно большим» c. Это нестандартная модель арифметики — ℕ «не аксиоматизируется» первы...

Формулы

До 1930-х годов понятие «алгоритм» было интуитивным. Тьюринг в 1936 году предложил математическую модель вычислений — машину Тьюринга (МТ) — и обосновал тезис: любое, что человек может вычислить «механически», вычисляет МТ. Это позволило строго доказать существование невычислимых функций.

Конфигурация: (q, u, a, v) — состояние q, лента = u·a·v, головка над a. Компактная запись: u_q_v (подчёркивает позицию головки).

Принятие: M принимает w, если вычисление из начальной конфигурации достигает q_acc. Отвергает — если достигает q_rej. Зацикливается — если не достигает ни того, ни другого.

Разрешитель: МТ, которая останавливается на любом входе (принять или отвергнуть). Если L принимается разрешителем — L разрешим (decidable). Если только распознаётся МТ — L перечислим (RE, recursively enumerable).

Тьюринг в 1936 году доказал: не существует программы, которая для произвольной программы P и входа w определила бы, завершится ли P на w. Это проблема остановки (Halting Problem). Доказательство использует элегантный диагональный аргумент — тот же, что Кантор применял для несчётности ℝ.

Предположим, существует разрешитель H для HALT: H(⟨M,w⟩) = «да», если M(w) останавливается; «нет» — иначе.

Перечислимость: МТ U (универсальная МТ) симулирует M на w и принимает, если M останавливается. При M(w) = ∞ — U зацикливается (не останавливается с «нет»).

Теорема (Райс, 1953): Любое нетривиальное семантическое свойство вычислимых функций неразрешимо.

Проблема остановки неразрешима совсем. Но большинство практических задач вычислимы — вопрос в том, насколько быстро. Теория сложности изучает ресурсы (время, память), требуемые алгоритмами. Проблема P = NP? — важнейший открытый вопрос информатики: совпадают ли задачи, решения которых быстро наход...

P (Polynomial Time): L ∈ P, если ∃ детерминированная МТ M и полином p: M разрешает L за время O(p(|w|)) при любом входе w.

Примеры в P: сортировка массива (O(n log n)), поиск кратчайшего пути (алгоритм Дейкстры O(n²)), проверка простоты числа (алгоритм AKS, 2002, O((log n)^{12})).

NP (Nondeterministic Polynomial Time): L ∈ NP, если ∃ «верификатор» V (детерминированная МТ) с полиномиальным временем такой, что: w ∈ L ⟺ ∃ «сертификат» c (|c| ≤ poly(|w|)): V(w,c) = «принять».

Система аксиом Гильберта (A1, A2, A3 + MP) технически адекватна, но неудобна для работы: реальные математики не рассуждают «выведи p→p за пять шагов». Натуральный вывод (Gentzen, 1935) — система, имитирующая привычную математическую практику: вводим гипотезы, разбираем случаи, применяем правила в...

Вывод — дерево, в корне — доказываемая формула, в листьях — гипотезы (могут быть «разряжены»).

Отрицание: ¬φ := φ→⊥. Из φ и ¬φ ⊢ ⊥. Из [¬φ]⊢⊥ ⊢ φ (reductio ad absurdum — в классике).

Следствие: конструктивное доказательство φ → ψ — это программа, преобразующая доказательство φ в доказательство ψ. Coq и Agda: писать программы = строить математические доказательства.

Натуральный вывод несимметричен: гипотезы слева, заключение справа, и введение/устранение связок асимметрично. Секвенциальное исчисление (Gentzen, 1935) — симметричная система, где доказательства имеют явную структуру, удобную для мета-теоремы. Главный результат — теорема об устранении сечений — ...

Секвенция: Γ ⊢ Δ (читается «из гипотез Γ следует хотя бы одна из Δ»). Γ и Δ — мультимножества формул.

Логические правила (пример для ∧ справа): из Γ ⊢ Δ, φ и Γ ⊢ Δ, ψ → Γ ⊢ Δ, φ∧ψ.

Правило сечения (Cut): из Γ ⊢ Δ, φ и φ, Π ⊢ Λ → Γ, Π ⊢ Δ, Λ. Это «использование леммы φ».

Классическая математика принимает закон исключённого третьего: φ ∨ ¬φ — тавтология. Брауэр (1908) и интуиционисты настаивают: «доказать φ ∨ ψ» означает либо доказать φ, либо доказать ψ — нельзя просто «от противного». Это ведёт к более слабой логике, но зато каждое доказательство конструктивно — ...

Что принято: modus ponens, ∧-правила, →-правила, ∃xφ(x) лишь при наличии конкретного свидетеля.

Семантика Крипке (1965): «Миры» w (моменты знания) с отношением ≤ (рост знаний). w ⊩ φ ∨ ψ ⟺ w ⊩ φ или w ⊩ ψ. Контрмодель для ЛИТ: мир w с w ⊬ p и w ⊬ ¬p.

Теорема: Аксиома Выбора (полная) + Интуиционистская логика → Закон Исключённого Третьего.

Определения

Шаг 2. И ℚ, и ℝ — модели DLO. Теорема (Кантор, Гунтер): DLO — полная теория

— каждое предложение ЛПП либо выводится из DLO, либо его отрицание выводится. Следовательно, все модели DLO элементарно эквивалентны: ℚ ≡ ℝ ✓.

Теорема Лёвенхейма–Сколема — первый глубокий результат теории моделей. Она показывает, что первопорядковая теория не контролирует мощность своих моделей: теория, имеющая счётную модель, имеет несчётную, и наоборот. Это «парадокс Сколема» — счётная модель теории ZFC содержит «несчётные» множества.

Нисходящая (Löwenheim 1915, Skolem 1920): Если T имеет бесконечную модель, то T имеет счётную модель.

Восходящая (Тарский–Ваот): Если T имеет бесконечную модель мощности κ, то T имеет модель мощности λ для любой λ ≥ max(κ, |σ|, ℵ₀).

Объединённая версия: Если T имеет модель мощности κ ≥ |T|, то T имеет модель мощности λ для любой λ ≥ |T|.

Тип элемента — это совокупность всех свойств, которыми обладает данный элемент в данной теории. Две модели могут иметь разные типы элементов. «Насыщенная» модель «содержит» все возможные типы — она максимально богата. Теория типов — ключ к пониманию, когда модели изоморфны, и к построению «канони...

Частичный n-тип (над пустым множеством параметров): Множество формул p(x₁,...,xₙ) такое, что p ∪ T выполнимо (т.е. в некоторой модели T существуют элементы, удовлетворяющие всем φ ∈ p).

Полный n-тип: Для каждой формулы φ(x₁,...,xₙ): либо φ ∈ p, либо ¬φ ∈ p. Максимально информативный тип.

Реализация типа: Элементы (a₁,...,aₙ) ∈ Mⁿ реализуют тип p, если M ⊨ φ(a₁,...,aₙ) для всех φ ∈ p.

Теорема о компактности — один из самых мощных инструментов теории моделей. Она позволяет «строить» модели с нужными свойствами через проверку бесконечного набора требований: нужно лишь убедиться, что каждое конечное требование выполнимо. Так строятся нестандартный анализ, нестандартные модели ари...

Теорема (следует из теоремы полноты Гёделя): Множество предложений Γ ЛПП выполнимо ⟺ каждое конечное подмножество Γ₀ ⊂ Γ выполнимо.

Два способа доказательства: 1. Через теорему полноты: Γ невыполнимо ⟺ Γ ⊢ ⊥ ⟺ ⊢ используется лишь конечное число аксиом из Γ. 2. Через ультрапроизведения (более конструктивно).

Конструкция *ℝ: Рассмотрим Th(ℝ) ∪ {0 < ε, ε < 1, ε < 1/2, ε < 1/3, ...}. Каждое конечное подмножество выполнимо (взять ε < 1/n). По компактности → существует *ℝ с «бесконечно малым» ε > 0, меньшим 1/n для всех стандартных n.