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

Lindström quantifier

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

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

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

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

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

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

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

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

куда

для ппара переменных.

Кванторы Линдстрема классифицируются в соответствии с числовой структурой их параметров. Например квантор типа (1,1), тогда как квантор типа (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 году Линдстрем доказал гораздо более сильный результат, теперь известный как Теорема Линдстрема, который интуитивно утверждает, что логика первого порядка - это самая «сильная» логика, обладающая обоими свойствами.

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

Рекомендации

  • Линдстрем, П. (1966). «Логика предикатов первого порядка с обобщенными кванторами». Теория. 32 (3): 186–195. Дои:10.1111 / j.1755-2567.1966.tb00600.x.
  • Л. Хелла. "Иерархии определимости обобщенных кванторов", Анналы чистой и прикладной логики, 43(3):235–271, 1989, Дои:10.1016/0168-0072(89)90070-5.
  • Л. Хелла. «Логические иерархии в PTIME». В материалах от 7-го Симпозиум IEEE по логике в компьютерных науках, 1992.
  • Л. Хелла, К. Луосто и Й. Ваананен. «Теорема об иерархии для обобщенных кванторов». Журнал символической логики, 61(3):802–817, 1996.
  • Burtschick, Hans-Jörg; Фоллмер, Хериберт (1999), Квантификаторы Линдстрема и определяемость конечного языка, ECCC TR96-005
  • Вестерстол, Даг (2001), «Квантификаторы», в Гобле, Лу (ред.), Руководство Блэквелла по философской логике, Blackwell Publishing, стр. 437–460..
  • Антонио Бадиа (2009). Квантификаторы в действии: обобщенная количественная оценка в запросах, логических и естественных языках. Springer. ISBN 978-0-387-09563-9.

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

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

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