Логика предикатов (логика первого порядка) — формальная система, расширяющая логику высказываний введением переменных, кванторов и предикатов. Создана Готлобом Фреге в 1879 году в работе "Begriffsschrift" (Исчисление понятий). Логика предикатов позволяет формализовать утверждения вида "Все люди смертны", "Существует простое число больше 100", которые невыразимы в логике высказываний.
Представьте предикат как свойство с пустыми слотами: "x > 5" — предикат, превращающийся в высказывание, когда подставляем число (7 > 5 — истина, 3 > 5 — ложь). Кванторы ∀ ("для всех") и ∃ ("существует") позволяют говорить о всех или некоторых объектах сразу: ∀x(x > 0 → x² > 0) — "для любого положительного x его квадрат положителен".
Основные понятия
Предикат P(x₁, x₂, ..., xₙ) — функция от n переменных, возвращающая истину или ложь. Примеры: P(x) = "x — простое число", Q(x, y) = "x < y", R(x, y, z) = "x + y = z".
Квантор всеобщности ∀x — "для всех x". Утверждение ∀x P(x) истинно, если P(x) истинно для каждого объекта в области определения. Пример: ∀x(x² ≥ 0) — квадрат любого числа неотрицателен.
Квантор существования ∃x — "существует x". Утверждение ∃x P(x) истинно, если P(x) истинно хотя бы для одного объекта. Пример: ∃x(x² = 4) — существует число, квадрат которого равен 4 (x = 2 или x = -2).
Свободные и связанные переменные: В формуле ∀x(x > y) переменная x связана квантором, y — свободна (значение не определено). Формула с свободными переменными — предикат, без свободных — высказывание.
Формулы и правила построения
Формулы строятся рекурсивно:
- Атомарная формула: P(t₁, t₂, ..., tₙ), где P — предикат, tᵢ — термы (переменные, константы, функции).
- Если A, B — формулы, то ¬A, A ∧ B, A ∨ B, A → B, A ↔ B — формулы.
- Если A — формула, x — переменная, то ∀x A и ∃x A — формулы.
Пример сложной формулы: ∀x(∃y(y > x) → ∀z(z < y → z < x + 1)). "Для любого x, если существует y > x, то для всех z < y выполняется z < x + 1". Формализует свойства вещественных чисел.
Отрицание кванторов
Правила де Моргана для кванторов:
- ¬∀x P(x) ≡ ∃x ¬P(x). "Неверно, что все x обладают P" = "Существует x, не обладающий P".
- ¬∃x P(x) ≡ ∀x ¬P(x). "Не существует x с P" = "Для всех x неверно P".
Пример: "Неверно, что все студенты сдали экзамен" = "Существует студент, не сдавший экзамен". ¬∀x Сдал(x) = ∃x ¬Сдал(x).
Выполнимость и общезначимость
Выполнимая формула — истинная хотя бы в одной интерпретации (модели). Пример: ∃x(x > 0) выполнима на натуральных числах (x = 1), но не на пустом множестве.
Общезначимая формула (тавтология) — истинная во всех интерпретациях. Пример: ∀x(P(x) ∨ ¬P(x)) — закон исключённого третьего, истина для любого предиката P и любой области.
Противоречие — ложная во всех интерпретациях. Пример: ∃x(P(x) ∧ ¬P(x)) — объект не может одновременно обладать и не обладать свойством.
Системы вывода
Естественный вывод (Герхард Генцен, 1934) — формальная система доказательства. Правила введения и удаления кванторов:
- ∀-введение: Если P(x) доказано для произвольного x, то ∀x P(x).
- ∀-удаление: Из ∀x P(x) следует P(t) для любого терма t.
- ∃-введение: Из P(t) следует ∃x P(x).
- ∃-удаление: Из ∃x P(x) и P(c) → Q (где c — новая константа) следует Q.
Секвенциальное исчисление (Генцен, 1934) — альтернативная система с секвенциями Γ ⊢ Δ ("из Γ следует Δ"). Используется в автоматическом доказательстве теорем.
Теорема Гёделя о полноте
Курт Гёдель в 1929 году доказал: логика первого порядка полна — любая общезначимая формула выводима из аксиом. Это означает: семантическая истинность (истина во всех моделях) эквивалентна синтаксической выводимости (доказуемость правилами).
Полнота не означает, что можно доказать всё. Теорема о неполноте (Гёдель, 1931) утверждает: в достаточно мощных теориях (например, арифметике) есть истинные, но недоказуемые утверждения.
Применение в математике
Формализация определений: "Функция f непрерывна в точке a" записывается как ∀ε > 0 ∃δ > 0 ∀x(|x - a| < δ → |f(x) - f(a)| < ε). Логика предикатов делает определения точными и однозначными.
Доказательство теорем: "Существует бесконечно много простых чисел". Доказательство от противного: предположим ∀n ∃k(n < k ∧ Простое(k)) ложно, получаем противоречие.
Теория моделей: Изучает связь между синтаксисом (формулы) и семантикой (модели). Теорема Лёвенхейма-Сколема (1915-1920): если теория имеет бесконечную модель, у неё есть модель любой бесконечной мощности.
Применение в информатике
Языки программирования: Типизация в Haskell, OCaml использует логику предикатов. Полиморфизм ∀α(α → α) — функция, работающая для любого типа α.
Базы данных: SQL-запросы — логика предикатов. SELECT * FROM users WHERE age > 18 эквивалентно ∃x(Пользователь(x) ∧ Возраст(x) > 18).
Верификация программ: Формальное доказательство корректности кода. Инвариант цикла формализуется через кванторы: ∀i(0 ≤ i < n → a[i] ≥ 0).
Автоматическое доказательство: Резолюция (Робинсон, 1965) — алгоритм проверки выполнимости формул в КНФ. Используется в Prolog и SAT-решателях.
Расширения логики первого порядка
Логика второго порядка: Кванторы по предикатам. ∀P(∀x(P(x) ∨ ¬P(x))) — "для любого предиката P и любого x выполняется P(x) или не-P(x)". Мощнее первого порядка, но не полна.
Модальная логика: Добавляет операторы необходимости □ и возможности ◇. □P — "необходимо P", ◇P — "возможно P". Применяется в философии, верификации систем.
Темпоральная логика: Операторы времени: G ("всегда"), F ("когда-нибудь"), X ("в следующий момент"). Используется для спецификации параллельных систем.