Квантификатор Линдстрема - Lindström quantifier

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

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

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

{displaystyle phi ^ {A, x, {ar {a}}} = {xin Acolon Amodels phi [x, {ar {a}}]}}

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

{displaystyle Amodels forall xphi [x, {ar {a}}] iff phi ^ {A, x, {ar {a}}} in forall _ {A}}

{displaystyle Amodels существует xphi [x, {ar {a}}] тогда и только тогда, когда phi ^ {A, x, {ar {a}}} in exists _ {A},}

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

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

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

{displaystyle Amodels Q_ {A} x_ {1} x_ {2} y_ {1} z_ {1} z_ {2} z_ {3} (phi, psi, heta) [a] iff (phi ^ {A, x_ { 1} x_ {2}, {ar {a}}}, psi ^ {A, y_ {1}, {ar {a}}}, heta ^ {A, z_ {1} z_ {2} z_ {3} , {ar {a}}}) в Q_ {A}}

^{[требуется разъяснение ]}

куда

{displaystyle phi ^ {A, {ar {x}}, {ar {a}}} = {(x_ {1}, dots, x_ {n}) в A ^ {n} двоеточие Amodels phi [{ar {x }}, {ар {а}}]}}

для ппара ${displaystyle {ar {x}}}$ переменных.

Кванторы Линдстрема классифицируются в соответствии с числовой структурой их параметров. Например ${displaystyle Qxyphi (x) psi (y)}$ квантор типа (1,1), тогда как ${displaystyle Qxyphi (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) < . . .

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

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

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

Алгоритмическая характеристика

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

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

внешняя ссылка

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