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

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

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

История

Формальная логика, как наука, берёт начало в работах Аристотеля, который разработал силлогистику — первую систематическую теорию логического вывода. Однако современная логика первого порядка была разработана в конце XIX — начале XX века.

В 1879 году немецкий логик и математик Готлоб Фреге опубликовал работу «Исчисление понятий» (Begriffsschrift), в которой впервые ввёл формальный язык, включающий кванторы, предикаты и переменные. Фреге фактически создал первую версию логики первого порядка, хотя и не использовал этот термин. Его работа заложила основы для современной математической логики.

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

В 1928 году Давид Гильберт и Вильгельм Аккерман в книге «Основы теоретической логики» чётко сформулировали синтаксис и семантику логики первого порядка. В 1930 году Курт Гёдель доказал теорему о полноте для логики первого порядка, показав, что любая логически истинная формула (общезначимая) может быть выведена с помощью формальной системы вывода. В 1936 году Алонзо Чёрч и Алан Тьюринг независимо друг от друга доказали неразрешимость логики первого порядка, то есть невозможность создания алгоритма, который бы для любой формулы определял, является ли она общезначимой.

Синтаксис

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

Алфавит

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

Термы

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

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

Примеры термов: x, 0, f(x, y), g(f(x), a).

Формулы

Формулы строятся из атомарных формул с помощью логических связок и кванторов.

1. Атомарная формула: если P — предикатный символ арности n, и t₁, t₂, …, tₙ — термы, то P(t₁, t₂, …, tₙ) — атомарная формула.
2. Сложные формулы:

• Если φ — формула, то ¬φ — формула.
• Если φ и ψ — формулы, то (φ ∧ ψ), (φ ∨ ψ), (φ → ψ), (φ ↔ ψ) — формулы.
• Если φ — формула и x — переменная, то ∀x φ и ∃x φ — формулы.

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

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

Пример: в формуле ∀x (P(x) → Q(x, y)) переменная x связана, а y — свободна.

Семантика

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

Модель

Модель M — это пара ⟨D, I⟩, где:

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

Оценка переменных

Оценка переменных s — это функция, которая каждой переменной x ставит в соответствие элемент s(x) ∈ D.

Истинность формулы

Истинность формулы φ в модели M при оценке s (обозначается M, s ⊧ φ) определяется рекурсивно:

1. Атомарная формула: M, s ⊧ P(t₁, …, tₙ) тогда и только тогда, когда ⟨I(t₁, s), …, I(tₙ, s)⟩ ∈ I(P) (где I(t, s) — значение терма t при оценке s).
2. Отрицание: M, s ⊧ ¬φ тогда и только тогда, когда не M, s ⊧ φ.
3. Конъюнкция: M, s ⊧ (φ ∧ ψ) тогда и только тогда, когда M, s ⊧ φ и M, s ⊧ ψ.
4. Дизъюнкция: M, s ⊧ (φ ∨ ψ) тогда и только тогда, когда M, s ⊧ φ или M, s ⊧ ψ (или оба).
5. Импликация: M, s ⊧ (φ → ψ) тогда и только тогда, когда если M, s ⊧ φ, то M, s ⊧ ψ.
6. Квантор общности: M, s ⊧ ∀x φ тогда и только тогда, когда для любого элемента d ∈ D, M, s[x/d] ⊧ φ, где s[x/d] — оценка, совпадающая с s, за исключением того, что переменной x присвоено значение d.
7. Квантор существования: M, s ⊧ ∃x φ тогда и только тогда, когда существует элемент d ∈ D такой, что M, s[x/d] ⊧ φ.

Общезначимость и выполнимость

• Формула φ называется общезначимой (логически истинной), если она истинна во всех моделях при любых оценках. Например, ∀x (P(x) ∨ ¬P(x)).
• Формула φ называется выполнимой, если существует модель M и оценка s такие, что M, s ⊧ φ.
• Формула φ называется противоречивой (невыполнимой), если она не истинна ни в одной модели.

Системы вывода

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

Гильбертовский тип исчислений

Этот тип включает набор аксиом и правил вывода. Например, модус поненс (из φ и φ → ψ выводится ψ) и правило обобщения (из φ выводится ∀x φ, если x не свободна в φ). Аксиомы включают, например, схемы аксиом для исчисления высказываний и аксиомы для кванторов.

Натуральное исчисление

Разработанное Герхардом Генценом в 1934 году, это исчисление более интуитивно понятно и использует правила введения и удаления логических связок и кванторов. Каждый логический коннектор имеет два правила: введение (как вывести формулу с этим коннектором) и удаление (как использовать формулу с этим коннектором).

Исчисление секвенций

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

Метод резолюций

Этот метод, разработанный Жаном Эрбраном и Аланом Робинсоном в 1960-х годах, используется в автоматическом доказательстве теорем. Формула приводится к клаузальной форме (конъюнкция дизъюнктов), после чего применяется правило резолюций: из двух дизъюнктов (C₁ ∨ L) и (C₂ ∨ ¬L) выводится (C₁ ∨ C₂) при условии унификации.

Свойства

Полнота

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

Непротиворечивость

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

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

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

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

Теорема о компактности утверждает, что бесконечное множество формул выполнимо тогда и только тогда, когда каждое его конечное подмножество выполнимо.

Применение

Математика

Логика первого порядка является основой для формальной аксиоматизации многих математических теорий. Например, теория множеств Цермело-Френкеля (ZF) и арифметика Пеано формулируются как теории первого порядка. Это позволяет изучать математику с единой формальной точки зрения и доказывать метатеоремы о непротиворечивости и независимости аксиом.

Информатика

• Базы данных: логика первого порядка используется в реляционной алгебре и для формулировки запросов к базам данных (например, на языке SQL). Реляционная модель данных может быть выражена с помощью формул логики первого порядка.
• Искусственный интеллект: логика первого порядка служит языком для представления знаний в экспертных системах. Языки программирования, такие как Prolog, основаны на логике первого порядка (точнее, на хорновских дизъюнктах).
• Автоматическое доказательство теорем: системы, подобные Otter и Vampire, используют методы резолюций для автоматического доказательства теорем первого порядка.
• Формальная верификация: логика первого порядка применяется для проверки корректности программ и аппаратного обеспечения, например, с помощью инструментов статического анализа.

Лингвистика

В формальной семантике логика первого порядка используется для моделирования значения естественноязыковых предложений, особенно с квантифицированными выражениями («все», «некоторые», «каждый»). Например, предложение «Каждый человек смертен» формализуется как ∀x (Человек(x) → Смертен(x)).

Философия

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

Ограничения

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

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

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

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

См. также

• Логика высказываний
• Логика второго порядка
• Исчисление предикатов
• Теорема Гёделя о полноте
• Теорема Чёрча
• Унификация (логика)

Источники

• Чёрч, Алонзо. Введение в математическую логику. — М.: Издательство иностранной литературы, 1960.
• Гильберт, Давид; Аккерман, Вильгельм. Основы теоретической логики. — М.: Государственное издательство иностранной литературы, 1947.
• Мендельсон, Эллиотт. Введение в математическую логику. — М.: Наука, 1976.
• Клини, Стивен. Математическая логика. — М.: Мир, 1973.
• Эндертон, Герберт. Элементы теории множеств и математической логики. — М.: МЦНМО, 2001.