Логика предикатов

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

История

Предпосылки возникновения

Идея разложения суждения на субъект и предикат восходит к «Категориям» Аристотеля (IV век до н. э.), который заложил основы силлогистики — первой формальной логической системы. Однако силлогистика Аристотеля была ограничена одноместными предикатами (свойствами) и не включала кванторы в современном понимании. В Средние века схоласты (Петр Испанский, Уильям Оккам) развивали теорию суппозиций, пытаясь уточнить смысл терминов, но формальный аппарат оставался неполным.

Создание современной логики предикатов

Решающий прорыв произошёл в конце XIX века. В 1879 году немецкий логик Готлоб Фреге опубликовал работу «Исчисление понятий» (нем. Begriffsschrift), где впервые ввёл формальный язык с кванторами (∀ — всеобщности, ∃ — существования) и предикатными символами. Фреге построил аксиоматическую систему логики предикатов первого порядка, которая позволяла выражать утверждения о всех или некоторых объектах предметной области. Независимо от Фреге, американский логик Чарльз Сандерс Пирс в 1880-х годах разработал собственную версию логики предикатов, используя кванторы и предикатные буквы, а также ввёл понятие «логического графа».

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

Развитие в XX–XXI веках

После работ Гёделя логика предикатов стала стандартным инструментом в математике, лингвистике (формальная семантика, теория речевых актов), информатике (логическое программирование, базы данных, верификация программ). Были разработаны расширения: логика предикатов высших порядков (допускающая кванторы по предикатам и функциям), модальная логика предикатов, темпоральная логика. В 1965 году Джон Алан Робинсон предложил метод резолюций, позволивший автоматизировать доказательство теорем в логике предикатов. Этот лёг в основу языка программирования Prolog (1972).

Основные понятия

Язык логики предикатов

Формальный язык логики предикатов состоит из следующих компонентов:

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

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

• Терм — это выражение, обозначающее объект. Термами являются предметные переменные, предметные константы, а также результаты применения функциональных символов к термам (например, f(x, g(a, y))).
• Атомарная формула — это предикатный символ, применённый к термам (например, P(x), R(f(a), y)).
• Формула строится из атомарных формул с помощью логических связок и кванторов. Например: ∀x (P(x) → ∃y R(x, y)).

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

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

Интерпретация

Интерпретация задаёт предметную область (непустое множество объектов) и приписывает значения всем символам языка:

• каждой предметной константе — конкретный объект из области;
• каждому функциональному символу — функцию на области;
• каждому предикатному символу — отношение (множество кортежей) на области.

Формула считается истинной в данной интерпретации, если она выполняется при подстановке всех значений в соответствии с интерпретацией. Например, формула ∀x (x > 0 → x² > 0) истинна в области натуральных чисел, но ложна в области целых чисел (так как для x = -1 условие x > 0 ложно, но импликация всё равно истинна; однако если рассматривать x = 0, то 0² = 0, что не больше 0, но посылка 0 > 0 ложна, поэтому импликация истинна; на самом деле формула истинна и для целых чисел, если предикат «>» интерпретируется как «строго больше»; для проверки нужно рассмотреть x = -1: -1 > 0 ложно, импликация истинна; для x = 0: 0 > 0 ложно, импликация истинна; для x = 1: 1 > 0 истинно, 1² = 1 > 0 истинно, импликация истинна; таким образом, формула истинна для всех целых чисел. Пример неточный — лучше использовать другую формулу, например ∀x (x > 0 → x + 1 > 0), которая также истинна для целых чисел).

Виды логики предикатов

Логика предикатов первого порядка

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

Логика предикатов высших порядков

Допускает кванторы по предикатам и функциям. Например, формула ∀P (P(0) ∧ ∀x (P(x) → P(x+1)) → ∀x P(x)) выражает принцип математической индукции. Логика второго порядка (кванторы по одноместным предикатам) более выразительна, но не является полной и не имеет эффективной аксиоматизации. Логики третьего и более высоких порядков используются в теории типов и основаниях математики.

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

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

Применение

В математике

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

В информатике

• Логическое программирование: язык Prolog основан на логике предикатов первого порядка. Программа состоит из фактов и правил, а выполнение сводится к автоматическому доказательству теорем методом резолюций.
• Базы данных: реляционная модель данных (Эдгар Кодд, 1970) тесно связана с логикой предикатов. Запросы SQL могут быть интерпретированы как формулы логики предикатов с кванторами.
• Верификация программ: формальные спецификации (например, на языке Z или в нотации VDM) используют логику предикатов для описания предусловий, постусловий и инвариантов.
• Искусственный интеллект: системы представления знаний (фреймы, онтологии) часто базируются на логике предикатов или её расширениях (дескрипционные логики).

В лингвистике

Формальная семантика (Ричард Монтегю, 1970-е) применяет логику предикатов для моделирования значения естественно-языковых выражений. Например, предложение «Все студенты сдали экзамен» переводится в формулу ∀x (Студент(x) → Сдал(x, экзамен)). Кванторы и предикаты позволяют точно описать семантические отношения.

В философии

Логика предикатов используется в аналитической философии для анализа онтологических и метафизических вопросов. Например, проблема универсалий (существуют ли общие свойства независимо от вещей) обсуждается в терминах предикации и квантификации.

Критика и ограничения

Выразительная сила

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

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

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

Сложность доказательств

Даже для разрешимых фрагментов (например, одноместные предикаты без функциональных символов) задача проверки выполнимости может быть экспоненциально сложной. На практике используются эвристики и ограниченные методы (например, SMT-решатели).

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

• Система аксиом логики предикатов первого порядка, предложенная Фреге, содержала 6 аксиом и одно правило вывода (modus ponens). Позднее были разработаны более экономичные системы (например, система Гильберта, система натурального вывода Генцена).
• Теорема Лёвенгейма-Скулема (1915–1920) утверждает, что любая выполнимая формула логики первого порядка имеет модель не более чем счётной мощности. Это означает, что логика первого порядка не может однозначно охарактеризовать несчётные структуры (например, вещественные числа).
• В 1970-х годах логика предикатов была использована для формализации семантики естественного языка в рамках «грамматики Монтегю», что позволило автоматически переводить предложения с английского на логические формулы.

Источники

• Фреге Г. «Исчисление понятий» (1879).
• Гильберт Д., Аккерман В. «Основы теоретической логики» (1928).
• Чёрч А. «Введение в математическую логику» (1956).
• Мендельсон Э. «Введение в математическую логику» (1964).
• Гёдель К. «О полноте исчисления логики» (1930).
• Робинсон Дж. А. «Машино-ориентированная логика, основанная на принципе резолюции» (1965).