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

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

¶История

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

В 1920-х годах австрийский логик Курт Гёдель доказал теорему о полноте логики первого порядка (1930), установив, что любое общезначимое утверждение (истинное во всех моделях) может быть выведено в рамках данной системы. В 1931 году Гёдель также доказал теоремы о неполноте, которые показали, что для арифметики Пеано (формализованной в логике первого порядка) существуют истинные, но недоказуемые утверждения. В 1936 году американский логик Алонзо Чёрч доказал неразрешимость логики первого порядка — отсутствие общего алгоритма для проверки общезначимости произвольного утверждения.

В середине XX века логика первого порядка стала фундаментом для математической логики, теории моделей, теории доказательств и информатики. В 1960-х годах были разработаны методы автоматического доказательства теорем (например, принцип резолюции Джона Робинсона), что привело к созданию систем логического программирования (Prolog).

¶Синтаксис

Синтаксис исчисления предикатов первого порядка определяет, какие последовательности символов являются корректными формулами. Он включает:

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

• Термы — выражения, обозначающие объекты:
• Переменная или константа — терм.
• Если f — функциональный символ арности n, а t1, ..., tn — термы, то f(t1, ..., tn) — терм.

• Формулы:
• Если P — предикатный символ арности n, а t1, ..., tn — термы, то P(t1, ..., tn) — атомарная формула.
• Если φ и ψ — формулы, то ¬φ, φ ∧ ψ, φ ∨ ψ, φ → ψ, φ ↔ ψ — формулы.
• Если φ — формула, а x — переменная, то ∀x φ и ∃x φ — формулы.

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

¶Семантика

Семантика определяет, как интерпретировать формулы в математических структурах. Основные понятия:

• Модель (или структура) M = (D, I), где:
• D — непустое множество (универсум).
• I — интерпретация, которая сопоставляет:
• Каждой константе c — элемент из D.
• Каждому функциональному символу f арности n — функцию f^I: D^n → D.
• Каждому предикатному символу P арности n — отношение P^I ⊆ D^n.

• Истинность формулы определяется относительно модели и приписывания значений свободным переменным (функции v: Var → D). Формула ∀x φ истинна, если φ истинна для всех возможных значений x в D. Формула ∃x φ истинна, если существует хотя бы одно значение x в D, при котором φ истинна.

• Общезначимость: Формула общезначима, если она истинна во всех моделях. Выполнимость: формула выполнима, если существует модель, в которой она истинна.

• Логическое следствие: Формула ψ является логическим следствием множества формул Γ, если во всех моделях, где истинны все формулы из Γ, истинна и ψ.

¶Аксиоматизация и правила вывода

Исчисление предикатов первого порядка может быть аксиоматизировано различными способами. Одна из классических систем (Гильберта) включает:

• Аксиомы логики высказываний (например, φ → (ψ → φ), (φ → (ψ → χ)) → ((φ → ψ) → (φ → χ)), (¬φ → ¬ψ) → (ψ → φ)).
• Аксиомы для кванторов:
• ∀x φ(x) → φ(t), где t — терм, свободный для подстановки в φ (не содержит захвата переменных).
• φ(t) → ∃x φ(x), где t — терм, свободный для подстановки.
• Правила вывода:
• Modus ponens: из φ и φ → ψ выводится ψ.
• Правило обобщения: из φ выводится ∀x φ (если x не свободна в посылках).

¶Свойства

¶Полнота

Теорема Гёделя о полноте (1930) утверждает, что для любого множества формул Γ и любой формулы φ, если φ является логическим следствием Γ, то φ выводимо из Γ в рамках аксиоматизации. Это означает, что синтаксическое доказательство эквивалентно семантическому следованию.

¶Компактность

Теорема компактности: если каждое конечное подмножество множества формул Γ выполнимо, то всё множество Γ выполнимо. Это свойство важно для теории моделей и позволяет строить нестандартные модели.

¶Неразрешимость

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

¶Теорема Лёвенгейма — Сколема

Теорема Лёвенгейма — Сколема утверждает, что если теория первого порядка имеет бесконечную модель, то она имеет модель любой бесконечной мощности. В частности, существуют счётные модели для теорий, которые описывают несчётные объекты (например, теория действительных чисел).

¶Применение

¶Математика

Логика первого порядка является стандартным языком для аксиоматизации математических теорий. Наиболее известные примеры:

• Теория множеств Цермело — Френкеля (ZF): аксиоматизирует понятие множества, включая аксиомы объединения, степени, выделения, замены и регулярности.
• Арифметика Пеано (PA): аксиоматизирует натуральные числа с операциями сложения и умножения, включая аксиому индукции.
• Теория групп: аксиомы ассоциативности, существования нейтрального элемента и обратного элемента.

¶Информатика

• Автоматическое доказательство теорем: Системы, такие как Prover9, E, Vampire, используют резолюцию и другие методы для проверки выводимости формул.
• Логическое программирование: Язык Prolog основан на хорновских дизъюнктах (подмножество логики первого порядка) и использует унификацию и обратный вывод.
• Базы данных: Реляционные базы данных могут быть описаны как модели первого порядка, а запросы SQL — как формулы (например, с кванторами существования).
• Верификация программ: Формальная верификация использует логику первого порядка для спецификации и доказательства корректности программ (например, в системе Coq, Isabelle/HOL).

¶Философия

Логика первого порядка применяется для анализа структуры научных теорий, онтологии (категории объектов и отношений) и метафизики (например, проблема универсалий).

¶Ограничения и расширения

Логика первого порядка не позволяет выражать некоторые важные математические понятия, такие как:

• Конечность: Нельзя выразить «существует только конечное число объектов».
• Счётность: Нельзя выразить «множество счётно».
• Индукция: Аксиома индукции в арифметике Пеано является схемой аксиом (бесконечным множеством), а не одной формулой.

Для преодоления этих ограничений существуют расширения:

• Логика второго порядка: Позволяет кванторовать по предикатам и функциям (например, ∀P ∃x P(x)).
• Логика высших порядков: Позволяет кванторовать по предикатам от предикатов.
• Логика с фиксированной точкой: Добавляет операторы наименьшей и наибольшей неподвижной точки.
• Модальная логика: Добавляет модальные операторы (необходимость, возможность).

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

• Теорема Гёделя о неполноте показывает, что любая непротиворечивая аксиоматизация арифметики (в логике первого порядка) неполна — существуют истинные, но недоказуемые утверждения.
• Логика первого порядка является «наименьшей» логикой, в которой можно выразить все математические утверждения, но она не является «наиболее выразительной» — существуют более мощные логики.
• В 1970-х годах была разработана теория моделей, которая изучает взаимосвязь между синтаксисом (формулами) и семантикой (моделями) в логике первого порядка.

¶Источники

• Гёдель, К. «О полноте исчисления логики предикатов» (1930).
• Чёрч, А. «Замечание о проблеме разрешимости» (1936).
• Эндертон, Г. «Математическое введение в логику» (2001).
• Мендельсон, Э. «Введение в математическую логику» (2010).
• Ван Дален, Д. «Логика и структура» (2013).