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

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

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

Синтаксис логики второго порядка строится на основе синтаксиса логики первого порядка, но добавляет новые типы переменных и кванторов.

Переменные и типы

В логике второго порядка выделяют два основных типа переменных:

1. Индивидные переменные (обозначаются обычно строчными латинскими буквами: \(x, y, z, \dots\)). Они пробегают по элементам универсума (предметной области).
2. Предикатные переменные (обозначаются прописными латинскими буквами: \(P, Q, R, \dots\)). Каждая предикатная переменная имеет арность (число аргументов). Например, одноместный предикат \(P(x)\) обозначает свойство индивида \(x\), а двуместный предикат \(R(x, y)\) — бинарное отношение между \(x\) и \(y\).
3. Функциональные переменные (обозначаются строчными латинскими буквами, часто \(f, g, h, \dots\)). Они также имеют арность и обозначают функции, отображающие кортежи индивидов в индивиды.

Кванторы

Кванторы в логике второго порядка могут связывать как индивидные, так и предикатные и функциональные переменные:

• Квантор всеобщности (\(\forall\)): \(\forall P \varphi\) означает «для всех предикатов \(P\) верно \(\varphi\)».
• Квантор существования (\(\exists\)): \(\exists P \varphi\) означает «существует такой предикат \(P\), что верно \(\varphi\)».

Аналогичные кванторы применяются и к функциональным переменным (\(\forall f, \exists f\)).

Формулы

Формулы логики второго порядка строятся рекурсивно из атомарных формул с помощью логических связок (\(\neg, \land, \lor, \rightarrow, \leftrightarrow\)) и кванторов. Атомарная формула — это либо равенство \(t_1 = t_2\) (где \(t_1, t_2\) — термы, построенные из констант и функциональных символов), либо применение предиката к термам: \(P(t_1, \dots, t_n)\).

Семантика

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

Стандартная семантика (полная семантика)

В стандартной семантике кванторы по предикатам и функциям пробегают по всем возможным подмножествам и функциям универсума. Если универсум имеет мощность \(\kappa\), то число одноместных предикатов равно \(2^\kappa\), а число \(n\)-местных отношений — \(2^{\kappa^n}\). Эта семантика придаёт логике второго порядка огромную выразительную силу, но делает её неполной и некомпактной.

Семантика Хенкина (обобщённая семантика)

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

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

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

Примеры

• Аксиома индукции в арифметике Пеано: В логике первого порядка аксиома индукции представляется как схема аксиом (бесконечное множество формул). В логике второго порядка она записывается одной формулой:

\[ \forall P \left( (P(0) \land \forall x (P(x) \rightarrow P(S(x)))) \rightarrow \forall x P(x) \right) \] где \(S\) — функция следования.

• Полнота линейного порядка: Утверждение «каждое непустое подмножество имеет наименьший элемент» (свойство вполнеупорядоченности) записывается как:

\[ \forall P \left( \exists x P(x) \rightarrow \exists y (P(y) \land \forall z (P(z) \rightarrow y \le z)) \right) \]

• Конечность и бесконечность: Логика второго порядка может выразить, что область конечна или бесконечна. Например, бесконечность области выражается формулой, утверждающей существование инъективной, но не сюръективной функции:

\[ \exists f \left( \forall x \forall y (f(x) = f(y) \rightarrow x = y) \land \exists z \forall x (f(x) \neq z) \right) \] В логике первого порядка это невозможно, так как она не может отличить конечную модель от бесконечной (теорема Лёвенгейма — Скулема).

Отношение к логике первого порядка

Логика второго порядка является расширением логики первого порядка: любая формула логики первого порядка является формулой логики второго порядка. Однако обратное неверно.

Теоретико-модельные свойства

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

Применение

Несмотря на свои метатеоретические недостатки (неполнота, некомпактность), логика второго порядка находит применение в различных областях математики и информатики.

В математике

• Арифметика второго порядка: Используется для формализации значительной части классической математики. Система \(Z_2\) (арифметика второго порядка) является основой для программы обратной математики, которая изучает относительную силу аксиом, необходимых для доказательства теорем.
• Теория категорий: Многие понятия теории категорий (например, универсальные свойства, пределы, копределы) естественно формализуются в логике второго порядка.
• Аксиоматическая теория множеств: Хотя теория множеств Цермело — Френкеля (ZFC) является теорией первого порядка, некоторые её аксиомы (например, аксиома выделения) являются схемами аксиом, которые можно заменить одной аксиомой второго порядка.

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

• Логика второго порядка в информатике: Используется в базах данных (логическое программирование, Datalog с отрицанием), в верификации программ (логика Хоара, разделяющая логика), в теории сложности (дескриптивная сложность).
• Логика второго порядка в лингвистике: Применяется для формализации семантики естественного языка, особенно для выражения кванторных конструкций, таких как «большинство», «несколько», «все, кроме одного».

Ограничения и критика

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

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

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

• Логика второго порядка была впервые систематически изучена Готлобом Фреге в его «Исчислении понятий» (1879), хотя он использовал несколько иную терминологию.
• Теорема Гёделя о неполноте для арифметики первого порядка может быть доказана с использованием логики второго порядка: арифметика Пеано второго порядка является категоричной (все её модели изоморфны), но неполной.
• В 1950 году Леон Хенкин доказал теорему о полноте для логики второго порядка с обобщённой семантикой, что привело к развитию теории моделей для неклассических логик.

Источники

1. Эндертон, Г. «Математическое введение в логику». — М.: Мир, 1975.
2. Мендельсон, Э. «Введение в математическую логику». — М.: Наука, 1984.
3. Шапиро, С. «Логика второго порядка». — В кн.: «Справочная книга по философской логике». — Springer, 2001.
4. Ван Дален, Д. «Логика и структура». — М.: Мир, 1989.