В математической логике квантификатор Линдстрема — это обобщенный полиадический квантификатор . Квантификаторы Линдстрема обобщают квантификаторы первого порядка, такие как квантификатор существования , квантификатор всеобщности и квантификаторы подсчета . Они были введены Пером Линдстремом в 1966 году. Позднее они изучались на предмет их применения в логике, в компьютерной науке и языках запросов к базам данных .
Для облегчения обсуждения необходимо пояснить некоторые условные обозначения. Выражение
для A L -структуры (или L -модели) на языке L , φ L -формулы и кортежа элементов домена dom( A ) A . [ необходимо разъяснение ] Другими словами, обозначает ( монадическое ) свойство, определенное на dom(A). В общем случае, где x заменяется на n -кортеж свободных переменных, обозначает n -арное отношение, определенное на dom( A ). Каждый квантификатор релятивизируется к структуре, поскольку каждый квантификатор рассматривается как семейство отношений (между отношениями) на этой структуре. Для конкретного примера возьмем универсальные и экзистенциальные квантификаторы ∀ и ∃ соответственно. Их условия истинности можно задать как
где — синглтон, единственным членом которого является dom( A ), а — множество всех непустых подмножеств dom( A ) (т. е. множество степеней dom( A ) минус пустое множество). Другими словами, каждый квантификатор — это семейство свойств на dom( A ), поэтому каждый называется монадическим квантификатором. Любой квантификатор, определенный как n > 0-арное отношение между свойствами на dom( A ), называется монадическим . Линдстрём ввел полиадические квантификаторы, которые являются n > 0-арными отношениями между отношениями на доменах структур.
Прежде чем перейти к обобщению Линдстрема, заметим, что любое семейство свойств на dom( A ) можно рассматривать как монадический обобщенный квантификатор. Например, квантификатор «существует ровно n вещей, таких что...» является семейством подмножеств домена структуры, каждое из которых имеет мощность размера n . Тогда «существует ровно 2 вещи, такие что φ» истинно в A тогда и только тогда, когда множество вещей, которые таковы, что φ, является членом множества всех подмножеств dom( A ) размера 2.
Квантификатор Линдстрема — это полиадический обобщенный квантификатор, поэтому вместо отношения между подмножествами домена он является отношением между отношениями, определенными в домене. Например, квантификатор определяется семантически как
где
для n - го набора переменных.
Квантификаторы Линдстрема классифицируются в соответствии с числовой структурой их параметров. Например, является квантификатором типа (1,1), тогда как является квантификатором типа (2). Примером квантификатора типа (1,1) является квантификатор Хартига, проверяющий равномощность, т. е. расширение {A, B ⊆ M: |A| = |B|}. [ необходимо пояснение ] Примером квантификатора типа (4) является квантификатор Хенкина .
Первый результат в этом направлении был получен Линдстрёмом (1966), который показал, что квантификатор типа (1,1) не может быть определен в терминах квантификатора типа (1). После того, как Лаури Хелла (1989) разработал общую технику доказательства относительной выразительности квантификаторов, полученная иерархия оказалась лексикографически упорядоченной по типу квантификатора:
Для каждого типа t существует квантификатор этого типа, который не может быть определен в логике первого порядка, расширенной квантификаторами, имеющими типы, меньшие t .
Хотя Линдстрём лишь частично разработал иерархию кванторов, которая теперь носит его имя, ему было достаточно заметить, что некоторые хорошие свойства логики первого порядка теряются, когда она расширяется некоторыми обобщенными кванторами. Например, добавление квантора «существует конечное множество» приводит к потере компактности , тогда как добавление квантора «существует несчетное множество» к логике первого порядка приводит к логике, больше не удовлетворяющей теореме Лёвенгейма–Сколема . В 1969 году Линдстрём доказал гораздо более сильный результат, теперь известный как теорема Линдстрёма , которая интуитивно утверждает, что логика первого порядка является «сильнейшей» логикой, обладающей обоими свойствами.
![{\displaystyle \phi ^{A,x,{\bar {a}}}=\{x\in A\colon A\models \phi [x,{\bar {a}}]\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/af0af3e10102ddaa9fc10a6be34c2ed108b4cab5)
![{\displaystyle A\models \forall x\phi [x,{\bar {a}}]\ifl \phi ^{A,x,{\bar {a}}}\in \forall _{A}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e29fdb907a4941ef604e326cd84225b462c4e4ec)
![{\displaystyle A\models \exists x\phi [x,{\bar {a}}]\iff \phi ^{A,x,{\bar {a}}}\in \exists _{A},}](https://wikimedia.org/api/rest_v1/media/math/render/svg/0b8fdb6bcb66501587ff4fd0df5ea8bd4c54567b)
![{\displaystyle A\models Q_{A}x_{1}x_{2}y_{1}z_{1}z_{2}z_{3}(\phi ,\psi ,\theta )[a]\ifl (\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}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/eb4409eee02e8299a4408df5157f3a27d5348be3)
![{\displaystyle \phi ^{A,{\bar {x}},{\bar {a}}}=\{(x_{1},\dots ,x_{n})\in A^{n}\colon A\models \phi [{\bar {x}},{\bar {a}}]\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4f53a028db508aa0b70498549f248861d92cd852)
