Логика предикатов первого порядка¶
Логика предикатов первого порядка (также исчисление предикатов, логика первого порядка) — это формальная система в математической логике, которая расширяет логику высказываний путём введения кванторов, предикатов и предметных переменных. В отличие от логики высказываний, где атомарными единицами являются целые утверждения, логика первого порядка позволяет анализировать внутреннюю структуру высказываний, выделяя объекты, их свойства и отношения между ними. Она является основой для формализации значительной части математики, информатики и искусственного интеллекта, обеспечивая строгий язык для записи аксиом, теорем и доказательств.
¶Основные понятия
¶Синтаксис
Язык логики первого порядка строится на основе алфавита, который включает:
- Предметные переменные (обычно обозначаются строчными латинскими буквами: \(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 году, стал одним из первых практических применений логики первого порядка в программировании.
¶Источники
- Гёдель К. «О полноте исчисления логики». — 1930.
- Гильберт Д., Аккерман В. «Основы теоретической логики». — 1928.
- Чёрч А. «Введение в математическую логику». — 1956.
- Мендельсон Э. «Введение в математическую логику». — 1964.
- Шенфилд Дж. «Математическая логика». — 1967.
- Эндертон Г. «Математическое введение в логику». — 1972.