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

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

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

Синтаксис

Язык логики первого порядка строится на основе алфавита, который включает:

• Предметные переменные (обычно обозначаются строчными латинскими буквами: \(x, y, z\));
• Предметные константы (обозначают конкретные объекты, например, \(0, 1, a\));
• Функциональные символы (обозначают операции над объектами, например, \(f(x, y)\));
• Предикатные символы (обозначают свойства и отношения, например, \(P(x), Q(x, y)\));
• Логические связки: \(\neg\) (отрицание), \(\land\) (конъюнкция), \(\lor\) (дизъюнкция), \(\rightarrow\) (импликация), \(\leftrightarrow\) (эквиваленция);
• Кванторы: \(\forall\) (квантор всеобщности — «для всех») и \(\exists\) (квантор существования — «существует»);
• Вспомогательные символы: скобки и запятые.

Термы — это выражения, обозначающие объекты. Они строятся из переменных, констант и функциональных символов. Например, \(f(x, g(y))\) — терм, если \(f\) и \(g\) — функциональные символы.

Формулы (или правильно построенные формулы) — это выражения, которые могут быть истинными или ложными. Простейшая формула — атомарная: \(P(t_1, t_2, \dots, t_n)\), где \(P\) — предикатный символ, а \(t_1, \dots, t_n\) — термы. Сложные формулы образуются с помощью логических связок и кванторов.

Семантика

Семантика логики первого порядка определяется через интерпретацию (или модель). Интерпретация задаёт:

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

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

Кванторы

Кванторы играют ключевую роль в логике первого порядка:

• Квантор всеобщности (\(\forall x\)) означает, что утверждение верно для всех объектов из предметной области. Например, \(\forall x (P(x) \rightarrow Q(x))\) читается как «для всех \(x\), если \(x\) обладает свойством \(P\), то \(x\) обладает свойством \(Q\)».
• Квантор существования (\(\exists x\)) означает, что существует хотя бы один объект, для которого утверждение верно. Например, \(\exists x (P(x) \land Q(x))\) читается как «существует \(x\) такой, что \(x\) обладает свойством \(P\) и свойством \(Q\)».

Переменные, связанные квантором, называются связанными, а остальные — свободными. Формула без свободных переменных называется замкнутой (или предложением).

История

Логика предикатов первого порядка была разработана в конце XIX — начале XX века в рамках программы формализации математики. Основоположниками считаются:

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

Свойства и теоремы

Полнота и непротиворечивость

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

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

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

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

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

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

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

Применение

В математике

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

• Теория множеств (ZFC — Цермело — Френкеля с аксиомой выбора);
• Арифметика Пеано (аксиомы натуральных чисел);
• Теория групп, колец, полей;
• Геометрия (аксиомы Гильберта).

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

• Базы данных: реляционные базы данных используют язык запросов SQL, основанный на логике первого порядка (реляционное исчисление кортежей и доменов).
• Искусственный интеллект: логическое программирование (язык Пролог) базируется на хорновских дизъюнктах — подклассе формул логики первого порядка.
• Формальная верификация: системы автоматического доказательства теорем (например, Coq, Isabelle, Z3) используют логику первого порядка для проверки корректности программ и аппаратуры.
• Семантическая паутина: язык описания онтологий OWL (Web Ontology Language) основан на дескрипционных логиках, которые являются фрагментом логики первого порядка.

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

Формальная семантика естественных языков часто использует логику первого порядка для представления значения предложений. Например, предложение «Каждый студент сдал экзамен» может быть записано как \(\forall x (Student(x) \rightarrow PassedExam(x))\).

Ограничения

Логика первого порядка имеет ряд ограничений:

• Невыразимость некоторых понятий: например, нельзя определить понятие «конечности» (существует только конечное число объектов) или «связности» графа, не прибегая к логике второго порядка.
• Отсутствие кванторов по предикатам: нельзя напрямую говорить о свойствах свойств (например, «существует свойство, которым обладают все чётные числа»). Для этого используется логика второго порядка.
• Неразрешимость: как уже упоминалось, не существует общего алгоритма для проверки общезначимости.

Связь с другими логиками

• Логика второго порядка допускает кванторы по предикатам и функциям, что делает её более выразительной, но неполной и некомпактной.
• Логика высших порядков позволяет кванторы по предикатам от предикатов и т.д.
• Модальная логика вводит операторы необходимости и возможности, которые могут быть интерпретированы как кванторы по возможным мирам.
• Интуиционистская логика отвергает закон исключённого третьего и требует конструктивных доказательств.

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

• Логика первого порядка лежит в основе теоремы Гёделя о неполноте: в любой достаточно богатой формальной системе (например, арифметике Пеано) существуют истинные, но недоказуемые утверждения.
• В 2000 году Институт Клэя включил проблему «P vs NP» в список «задач тысячелетия», которая формулируется на языке логики первого порядка.
• Язык Пролог, созданный в 1972 году, стал одним из первых практических применений логики первого порядка в программировании.

Источники

1. Гёдель К. «О полноте исчисления логики». — 1930.
2. Гильберт Д., Аккерман В. «Основы теоретической логики». — 1928.
3. Чёрч А. «Введение в математическую логику». — 1956.
4. Мендельсон Э. «Введение в математическую логику». — 1964.
5. Шенфилд Дж. «Математическая логика». — 1967.
6. Эндертон Г. «Математическое введение в логику». — 1972.