Исчисление предикатов

Исчисление предикатов — это формальная система, раздел математической логики, изучающий логические законы и правила вывода для высказываний, внутренняя структура которых раскрывается через предикаты (свойства и отношения) и кванторы. Является расширением логики высказываний и служит основой для формализации значительной части математических и научных рассуждений. В отличие от логики высказываний, где атомарными единицами являются целые пропозиции, исчисление предикатов позволяет анализировать их состав: субъект (предмет речи) и предикат (то, что утверждается о субъекте).

История

Основы исчисления предикатов были заложены в трудах немецкого математика и логика Готлоба Фреге, который в 1879 году опубликовал работу «Исчисление понятий» (нем. Begriffsschrift). В ней он впервые построил формальный язык, включающий кванторы и предикатные символы, и сформулировал аксиомы и правила вывода для логики первого порядка. Работа Фреге оставалась малоизвестной до её популяризации Бертрандом Расселом и Альфредом Нортом Уайтхедом в их монументальном труде «Principia Mathematica» (1910–1913), где исчисление предикатов было использовано для обоснования математики.

Дальнейшее развитие связано с работами Леопольда Лёвенгейма (теорема Лёвенгейма — Сколема), Торальфа Сколема, Курта Гёделя (теорема о полноте, 1930) и Альфреда Тарского (формальная семантика, определение истины). Гёдель доказал, что исчисление предикатов первого порядка является семантически полным: любая общезначимая формула выводима в системе. Это принципиально отличает его от логики высших порядков, где полнота отсутствует.

Синтаксис

Синтаксис исчисления предикатов определяет, какие последовательности символов являются корректно построенными формулами (КПФ). Алфавит включает:

• Предметные переменные (x, y, z, ...) — обозначают объекты из области рассуждения.
• Предметные константы (a, b, c, ...) — обозначают конкретные объекты (например, 0, 1).
• Предикатные символы (P, Q, R, ...) — обозначают свойства (одноместные) и отношения (многоместные). Каждый предикатный символ имеет арность (число аргументов).
• Функциональные символы (f, g, h, ...) — обозначают операции, отображающие объекты в объекты (например, сложение, умножение).
• Логические связки: ¬ (отрицание), ∧ (конъюнкция), ∨ (дизъюнкция), → (импликация), ↔ (эквиваленция).
• Кванторы:
• ∀ (квантор всеобщности) — «для всех», «каждый».
• ∃ (квантор существования) — «существует», «некоторый».
• Вспомогательные символы: скобки ( и ), запятая.

Термы и формулы

Терм — это выражение, обозначающее объект:

• Любая константа или переменная — терм.
• Если f — n-местный функциональный символ, а t₁, ..., tₙ — термы, то f(t₁, ..., tₙ) — терм.

Атомарная формула — это предикатный символ, применённый к термам: P(t₁, ..., tₙ).

Формулы строятся рекурсивно:

• Любая атомарная формула — формула.
• Если A и B — формулы, то ¬A, A∧B, A∨B, A→B, A↔B — формулы.
• Если A — формула, а x — переменная, то ∀x A и ∃x A — формулы.

Свободные и связанные переменные

Вхождение переменной в формулу может быть свободным или связанным. Переменная связана, если она находится в области действия квантора (∀x или ∃x). В противном случае она свободна. Формула, не содержащая свободных переменных, называется замкнутой (или предложением). Замкнутая формула выражает законченное утверждение об области рассуждения.

Семантика

Семантика исчисления предикатов определяет, как интерпретировать формулы в некоторой модели. Модель (или структура) состоит из:

1. Непустого множества D (область рассуждения или универсум) — совокупность объектов, о которых идёт речь.
2. Функции интерпретации I, которая:

• каждой константе c сопоставляет элемент из D;
• каждому n-местному функциональному символу f сопоставляет функцию fᴵ: Dⁿ → D;
• каждому n-местному предикатному символу P сопоставляет отношение Pᴵ ⊆ Dⁿ (множество n-ок объектов, для которых P истинно).

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

• Атомарная формула P(t₁, ..., tₙ) истинна, если кортеж значений термов (t₁ᴵ, ..., tₙᴵ) принадлежит отношению Pᴵ.
• ∀x A истинно, если A истинно для любого объекта из D (при подстановке его вместо x).
• ∃x A истинно, если существует хотя бы один объект из D, для которого A истинно.

Формула называется общезначимой (логически истинной), если она истинна во всех моделях. Формула называется выполнимой, если существует хотя бы одна модель, в которой она истинна.

Исчисление предикатов первого порядка

Наиболее распространённым и фундаментальным является исчисление предикатов первого порядка (логика первого порядка). В нём кванторы могут связывать только предметные переменные, но не предикаты или функции. Это накладывает ограничение: нельзя, например, сказать «для любого свойства P...» (это требует квантора по предикату, что является логикой второго порядка).

Аксиомы и правила вывода

Существует несколько эквивалентных аксиоматизаций. Классическая система включает:

• Все тавтологии логики высказываний (после замены пропозициональных переменных на формулы логики предикатов).
• Аксиомы для кванторов:
• ∀x A(x) → A(t), где t — терм, свободный для подстановки вместо x.
• A(t) → ∃x A(x).
• Правила вывода:
• Modus ponens: из A и A→B выводится B.
• Правило обобщения (∀-введение): из A → B(x), где x не свободна в A, выводится A → ∀x B(x).
• Правило конкретизации (∃-введение): из A(x) → B, где x не свободна в B, выводится ∃x A(x) → B.

Теорема о полноте

Ключевой результат для логики первого порядка — теорема Гёделя о полноте (1930): формула является общезначимой тогда и только тогда, когда она выводима в исчислении предикатов первого порядка. Это означает, что формальная система выводимости в точности соответствует семантической общезначимости. Следствием является теорема о компактности: если каждое конечное подмножество множества формул имеет модель, то и всё множество имеет модель.

Разрешимость

В отличие от логики высказываний, исчисление предикатов первого порядка неразрешимо. Это означает, что не существует алгоритма, который для любой формулы за конечное число шагов определял бы, является ли она общезначимой (или, что эквивалентно, выводимой). Этот факт был установлен Алонзо Чёрчем (1936) и Аланом Тьюрингом (1936) на основе понятия алгоритмической неразрешимости проблемы остановки. Однако существуют разрешимые фрагменты (например, логика одноместных предикатов).

Исчисления высших порядков

Логика второго порядка допускает кванторы по предикатам и функциям. Это значительно увеличивает выразительную силу: в ней можно формализовать понятия индукции, равенства мощностей множеств, полноты вещественных чисел. Однако она не является полной (теорема Гёделя о неполноте применима к ней) и не имеет эффективной аксиоматизации.

Логика высших порядков (третьего, четвёртого и т.д.) допускает кванторы по предикатам от предикатов. Они ещё более выразительны, но также неполны и неразрешимы.

Применение

Исчисление предикатов является фундаментальным инструментом в:

• Математике: формализация аксиоматических теорий (теория множеств Цермело — Френкеля, арифметика Пеано, теория групп). Доказательства теорем о неполноте и неразрешимости.
• Информатике:
• Логическое программирование: язык Пролог основан на подмножестве логики первого порядка (хорновские дизъюнкты).
• Базы данных: язык запросов SQL содержит фрагменты логики первого порядка (реляционное исчисление).
• Искусственный интеллект: представление знаний, автоматическое доказательство теорем (системы, такие как E, Vampire, Z3).
• Верификация программ: формальная проверка корректности программного и аппаратного обеспечения (модель-чекинг, дедуктивная верификация).
• Лингвистике: формальная семантика естественного языка (семантика Монтегю) использует исчисление предикатов для моделирования значения предложений.
• Философии: анализ логической структуры научных теорий, онтология, метафизика.

Интересные факты

• Исчисление предикатов первого порядка является основой для ZF-теории множеств (Цермело — Френкеля), которая, несмотря на свою неполноту, служит стандартным фундаментом для современной математики.
• Парадокс Рассела возникает именно при попытке использовать неограниченное понимание множеств в логике первого порядка, что привело к созданию аксиоматических теорий множеств.
• Теорема Лёвенгейма — Сколема утверждает, что любая теория первого порядка, имеющая бесконечную модель, имеет модель любой бесконечной мощности. Это показывает, что логика первого порядка не может однозначно охарактеризовать бесконечные структуры (например, натуральные числа).

Источники

1. Гильберт Д., Аккерман В. Основы теоретической логики. — М.: Иностранная литература, 1947.
2. Клини С. К. Введение в метаматематику. — М.: Издательство иностранной литературы, 1957.
3. Мендельсон Э. Введение в математическую логику. — М.: Наука, 1976.
4. Новиков П. С. Элементы математической логики. — М.: Наука, 1973.
5. Чёрч А. Введение в математическую логику. — М.: Издательство иностранной литературы, 1960.