Квантификатор Линдстрема

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

• 1 Обобщение кванторы первого порядка
• 2 Иерархия выразительности
• 3 Как предшественники теоремы Линдстрема
• 4 Алгоритмическая характеристика
• 5 Ссылки
• 6 Дополнительная литература
• 7 Внешние ссылки

Чтобы облегчить обсуждение, некоторые условные обозначения нуждаются в пояснении. Выражение

$\varphi \; A,\; x,\; a\; ¯\; =\; \{x\; \in \; A:\; A\; \models \; \varphi \; [x,\; a\; ¯]\}\; \{\backslash \; displaystyle\; \backslash \; phi\; ^\; \{A,\; x,\; \{\backslash \; bar\; \{a\}\}\}\; =\; \backslash \; \{\; x\; \backslash \; in\; A\; \backslash \; двоеточие\; A\; \backslash \; models\; \backslash \; phi\; [x,\; \{\backslash \; bar\; \{a\}\}]\; \backslash \}\}$

для A L-структура (или L-модель) в языке L, φ L-формула, и $a\; ¯\; \{\backslash \; displaystyle\; \{\backslash \; bar\; \{a\}\}\}$кортеж элементов домена dom (A) из A. Другими словами, $\varphi \; A,\; x,\; a\; ¯\; \{\backslash \; displaystyle\; \backslash \; phi\; ^\; \{A,\; x,\; \{\backslash \; bar\; \{a\}\}\}\}$обозначает (монадическое ) свойство, определенное в dom (A). Как правило, если x заменяется кортежем из n $x\; ¯\; \{\backslash \; displaystyle\; \{\backslash \; bar\; \{x\}\}\}$свободных переменных, $\varphi \; A,\; x\; ¯,\; a\; ¯\; \{\; \backslash \; displaystyle\; \backslash \; phi\; ^\; \{A,\; \{\backslash \; bar\; \{x\}\},\; \{\backslash \; bar\; \{a\}\}\}\}$обозначает n-арное отношение, определенное на dom (A). Каждый квантор $Q\; A\; \{\backslash \; displaystyle\; Q\_\; \{A\}\}$относителен к структуре, поскольку каждый квантор рассматривается как семейство отношений (между отношениями) в этой структуре. В качестве конкретного примера возьмем универсальный и экзистенциальный кванторы ∀ и ∃ соответственно. Их условия истинности могут быть определены как

$A\; \models \; \forall \; x\; \varphi \; [x,\; a\; ¯]\; ⟺\; \varphi \; A,\; x,\; a\; ¯\; \in \; \forall \; A\; \{\backslash \; displaystyle\; A\; \backslash \; models\; \backslash \; forall\; x\; \backslash \; phi\; [x,\; \{\backslash \; bar\; \{\; a\}\}]\; \backslash \; iff\; \backslash \; phi\; ^\; \{A,\; x,\; \{\backslash \; bar\; \{a\}\}\}\; \backslash \; in\; \backslash \; forall\; \_\; \{A\}\}$

$A\; \models \; \exists \; x\; \varphi \; [x,\; a\; ¯]\; ⟺\; \varphi \; A,\; x,\; a\; ¯\; \in \; \exists \; A,\; \{\backslash \; displaystyle\; A\; \backslash \; models\; \backslash \; exists\; x\; \backslash \; phi\; [x,\; \{\backslash \; bar\; \{a\}\}]\; \backslash \; iff\; \backslash \; phi\; ^\; \{A,\; x,\; \{\backslash \; bar\; \{a\}\}\}\; \backslash \; in\; \backslash \; существует\; \_\; \{A\},\}$

где $\forall \; A\; \{\backslash \; displaystyle\; \backslash \; forall\; \_\; \{A\}\}$- одноэлементный элемент, единственным членом которого является dom (A), а $\exists \; A\; \{\backslash \; displaystyle\; \backslash \; exists\; \_\; \{A\}\}$- это набор всех непустых подмножеств dom (A) (т. е. power set dom (A) минус пустое множество). Другими словами, каждый квантор - это семейство свойств на dom (A), поэтому каждое из них называется монадическим квантором. Любой квантор, определенный как n>0-арное отношение между свойствами на dom (A), называется монадическим. Линдстрем ввел полиадические отношения, которые представляют собой n>0-арные отношения между отношениями в областях структур.

Прежде чем мы перейдем к обобщению Линдстрема, обратите внимание, что любое семейство свойств на dom (A) можно рассматривать как монадический обобщенный квантор. Например, квантификатор «существует ровно n таких вещей, что...» - это семейство подмножеств домена структуры, каждое из которых имеет мощность n. Тогда «есть ровно две вещи, такие что φ» истинно в A тогда и только тогда, когда множество таких вещей, что φ является членом множества всех подмножеств dom (A) размера 2.

Квантор Линдстрема - это полиадический обобщенный квантор, поэтому вместо того, чтобы быть отношением между подмножествами области, это отношение между отношениями, определенными в области. Например, квантор $QA\; x\; 1\; x\; 2\; y\; 1\; z\; 1\; z\; 2\; z\; 3\; (\varphi \; (x\; 1\; x\; 2),\; \psi \; (y\; 1),\; \theta \; (z\; 1\; z\; 2\; z\; 3))\; \{\backslash \; displaystyle\; Q\_\; \{A\}\; x\_\; \{1\}\; x\_\; \{2\}\; y\_\; \{1\}\; z\_\; \{1\}\; z\_\; \{2\}\; z\_\; \{3\}\; (\backslash \; phi\; (x\_\; \{1\}\; x\_\; \{2\}),\; \backslash \; psi\; (y\_\; \{1\}),\; \backslash \; theta\; (z\_\; \{1\}\; z\_\; \{2\}\; z\_\; \{3\}))\}$семантически определяется как

$A\; \models \; QA\; x\; 1\; x\; 2\; y\; 1\; z\; 1\; z\; 2\; z\; 3\; (\varphi ,\; \psi ,\; \theta )\; [a]\; ⟺\; (\varphi \; A,\; x\; 1\; x\; 2,\; a\; ¯,\; \psi \; A,\; y\; 1,\; a\; ¯,\; \theta \; A,\; z\; 1\; z\; 2\; z\; 3,\; a\; ¯)\; \in \; QA\; \{\backslash \; displaystyle\; A\; \backslash \; models\; Q\_\; \{A\}\; x\_\; \{1\}\; x\_\; \{2\}\; y\_\; \{1\}\; z\_\; \{1\}\; z\_\; \{2\}\; z\_\; \{3\}\; (\backslash \; phi,\; \backslash \; psi,\; \backslash \; theta)\; [a]\; \backslash \; iff\; (\backslash \; phi\; ^\; \{A,\; x\_\; \{1\}\; x\_\; \{2\},\; \{\backslash \; bar\; \{a\}\}\},\; \backslash \; psi\; ^\; \{A,\; y\_\; \{1\},\; \{\backslash \; bar\; \{a\}\}\},\; \backslash \; theta\; ^\; \{A,\; z\_\; \{1\}\; z\_\; \{2\; \}\; z\_\; \{3\},\; \{\backslash \; bar\; \{a\}\}\})\; \backslash \; in\; Q\_\; \{A\}\}$

где

$\varphi \; A,\; x\; ¯,\; a\; ¯\; =\; \{(x\; 1,\dots ,\; xn)\; \in \; A\; n\; :\; A\; \models \; \varphi \; [x\; ¯,\; a\; ¯]\}\; \{\backslash \; displaystyle\; \backslash \; phi\; ^\; \{A,\; \{\backslash \; bar\; \{x\}\},\; \{\backslash \; bar\; \{a\}\}\}\; =\; \backslash \; \{(x\_\; \{1\},\; \backslash \; dots,\; x\_\; \{n\})\; \backslash \; in\; A\; ^\; \{n\}\; \backslash \; двоеточие\; A\; \backslash \; models\; \backslash \; phi\; [\{\backslash \; bar\; \{x\}\},\; \{\backslash \; bar\; \{a\}\}]\; \backslash \}\}$

для кортежа из n $x\; ¯\; \{\backslash \; displaystyle\; \{\backslash \; bar\; \{x\}\}\}$переменных.

Кванторы Lindström классифицируются в соответствии с числовой структурой их параметров. Например, $Q\; xy\; \varphi \; (x)\; \psi \; (y)\; \{\backslash \; displaystyle\; Qxy\; \backslash \; phi\; (x)\; \backslash \; psi\; (y)\}$является квантификатором типа (1,1), тогда как $Q\; xy\; \varphi \; (x,\; y)\; \{\backslash \; displaystyle\; Qxy\; \backslash \; phi\; (x,\; y)\}$- квантор типа (2). Примером квантификатора типа (1,1) является проверка эквикардинальности, то есть расширения {A, B ⊆ M: | A | = | B |}. Примером квантора типа (4) является квантор Хенкина.

Первый результат в этом направлении был получен Линдстремом (1966), который показал, что тип (1,1) квантор не может быть определен в терминах квантора типа (1). После того как Лаури Хелла (1989) разработал общую технику доказательства относительной выразительности кванторов, полученная иерархия оказалась лексикографически упорядоченной по типу квантора:

(1) < (1, 1) <... < (2) < (2, 1) < (2, 1, 1) <... < (2, 2) <... (3) <...

Для каждого типа t, существует квантор этого типа, который не может быть определен в логике первого порядка, расширенный кванторами, которые имеют типы меньше t.

Хотя Линдстрем лишь частично разработал иерархию кванторов, которые теперь носят его имя, ему было достаточно заметить, что некоторые прекрасные свойства логики первого порядка являются теряется, когда он расширяется некоторыми обобщенными кванторами. Например, добавление квантора «существует конечное число» приводит к потере компактности, тогда как добавление квантора «существует несчетное количество» к логике первого порядка приводит к тому, что логика больше не удовлетворяет Теорема Лёвенгейма – Сколема. В 1969 году Линдстрем доказал гораздо более сильный результат, теперь известный как теорема Линдстрема, которая интуитивно утверждает, что логика первого порядка является «самой сильной» логикой, обладающей обоими свойствами.

• Линдстрем, П. (1966). «Логика предикатов первого порядка с обобщенными кванторами». Теория. 32(3): 186–195. doi : 10.1111 / j.1755-2567.1966.tb00600.x.
• L. Hella. «Иерархии определимости обобщенных кванторов», 43 (3): 235–271, 1989, doi : 10.1016 / 0168-0072 (89) 90070-5.
• L. Hella. «Логические иерархии в PTIME». В материалах 7-го симпозиума IEEE по логике в компьютерных науках, 1992.
• Л. Хелла, К. Луосто и. «Теорема об иерархии для обобщенных кванторов». Journal of Symbolic Logic, 61 (3): 802–817, 1996.
• Burtschick, Hans-Jörg; Фоллмер, Хериберт (1999), Lindström Quantifiers and Leaf Language Definability, ECCC TR96-005
• Westerståhl, Dag (2001), «Quantifiers», в Goble, Lou (ed.), Руководство Блэквелла по философской логике, Блэквелл Паблишинг, стр. 437–460.
• Антонио Бадиа (2009). Квантификаторы в действии: обобщенная количественная оценка в запросах, логических и естественных языках. Springer. ISBN 978-0-387-09563-9.

• Йоуко Вяананен (ред.), Обобщенные квантификаторы и вычисления. 9-я Европейская летняя школа по логике, языку и информации. ESSLLI’97 Мастерская. Экс-ан-Прованс, Франция, 11–22 августа 1997 г. Пересмотренные лекции, Springer Лекции по информатике 1754, ISBN 3-540-66993 -0

• Dag Westerståhl, 2011. «Обобщенные квантификаторы ». Стэнфордская энциклопедия философии.