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

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

Обобщение кванторов первого порядка

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

$\phi ^{A,x,{\bar {a}}}=\{x\in A\colon A\models \phi [x,{\bar {a}}]\}$

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

$A\models \forall x\phi [x,{\bar {a}}]\iff \phi ^{A,x,{\bar {a}}}\in \forall _{A}$

$A\models \exists x\phi [x,{\bar {a}}]\iff \phi ^{A,x,{\bar {a}}}\in \exists _{A},$

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

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

Квантор Линдстрема — это полиадический обобщенный квантор, поэтому вместо того, чтобы быть отношением между подмножествами области, это отношение между отношениями, определенными в области. Например, квантификатор $Q_{A}x_{1}x_{2}y_{1}z_{1}z_{2}z_{3}(\phi (x_{1}x_{2}),\psi (y_{1}),\theta (z_{1}z_{2}z_{3}))$ определяется семантически как

$A\models Q_{A}x_{1}x_{2}y_{1}z_{1}z_{2}z_{3}(\phi ,\psi ,\theta )[a]\iff (\phi ^{A,x_{1}x_{2},{\bar {a}}},\psi ^{A,y_{1},{\bar {a}}},\theta ^{A,z_{1}z_{2}z_{3},{\bar {a}}})\in Q_{A}$

где

$\phi ^{A,{\bar {x}},{\bar {a}}}=\{(x_{1},\dots ,x_{n})\in A^{n}\colon A\models \phi [{\bar {x}},{\bar {a}}]\}$

для n -кортежа ${\bar {x}}$ переменных.

Кванторы Линдстрема классифицируются по числовой структуре их параметров. Например $Qxy\phi (x)\psi (y)$ является квантором типа (1,1), тогда как $Qxy\phi (x,y)$ является квантором типа (2). Примером квантора типа (1,1) является квантор Хартига, проверяющий эквикардинальность, т.е. расширение {A, B ⊆ M: |A| = |В|}. Примером квантора типа (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. дои : 10.1111/j.1755-2567.1966.tb00600.x .
• Л. Хелла. «Иерархии определимости обобщенных кванторов», Annals of Pure and Applied Logic , 43(3):235–271, 1989, дои : 10.1016/0168-0072(89)90070-5 .
• Л. Хелла. «Логические иерархии в PTIME». В материалах 7-го симпозиума IEEE по логике в информатике , 1992 г.
• Л. Хелла, К. Луосто и Й. Ваананен . «Теорема об иерархии для обобщенных кванторов». Журнал символической логики , 61(3):802–817, 1996.
• Бурчик, Ханс-Йорг; Фоллмер, Гериберт (1999), Кванторы Линдстрема и определяемость листового языка , ECCC   TR96-005
• Вестерстол, Даг (2001), «Кванторы», в Гобл, Лу (редактор), «Руководство Блэквелла по философской логике» , Blackwell Publishing, стр. 437–460 .
• Антонио Бадиа (2009). Кванторы в действии: обобщенная квантификация в запросах, логических и естественных языках . Спрингер. ISBN  978-0-387-09563-9 .

Дальнейшее чтение

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

Внешние ссылки

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