Lindström quantifier

In mathematical logic, a Lindström quantifier is a generalized polyadic quantifier. Lindström quantifiers generalize first-order quantifiers, such as the existential quantifier, the universal quantifier, and the counting quantifiers. They were introduced by Per Lindström in 1966. They were later studied for their applications in logic in computer science and database query languages.

Generalization of first-order quantifiers

In order to facilitate discussion, some notational conventions need explaining. The expression

: $\phi^=\$

for ''A'' an ''L''-structure (or ''L''-model) in a language ''L'', ''φ'' an ''L''-formula, and $\bar$ a tuple of elements of the domain dom(''A'') of ''A''. In other words, $\phi^$ denotes a ( monadic) property defined on dom(A). In general, where ''x'' is replaced by an ''n''-tuple $\bar$ of free variables, $\phi^$ denotes an ''n''-ary relation defined on dom(''A''). Each quantifier $Q_A$ is relativized to a structure, since each quantifier is viewed as a family of relations (between relations) on that structure. For a concrete example, take the universal and existential quantifiers ∀ and ∃, respectively. Their truth conditions can be specified as

: A\models\forall x\phi ,\bar\iff \phi^\in\forall_A
: A\models\exists x\phi ,\bar\iff \phi^\in\exists_A,

where $\forall_A$ is the singleton whose sole member is dom(''A''), and $\exists_A$ is the set of all non-empty subsets of dom(''A'') (i.e. the power set of dom(''A'') minus the empty set). In other words, each quantifier is a family of properties on dom(''A''), so each is called a ''monadic'' quantifier. Any quantifier defined as an ''n'' > 0-ary relation between properties on dom(''A'') is called ''monadic''. Lindström introduced polyadic ones that are ''n'' > 0-ary relations between relations on domains of structures.

Before we go on to Lindström's generalization, notice that any family of properties on dom(''A'') can be regarded as a monadic generalized quantifier. For example, the quantifier "there are exactly ''n'' things such that..." is a family of subsets of the domain of a structure, each of which has a cardinality of size ''n''. Then, "there are exactly 2 things such that φ" is true in A if and only if the set of things that are such that φ is a member of the set of all subsets of dom(''A'') of size 2.

A Lindström quantifier is a polyadic generalized quantifier, so instead being a relation between subsets of the domain, it is a relation between relations defined on the domain. For example, the quantifier $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))$ is defined semantically as

: A\models Q_Ax_1x_2y_1z_1z_2z_3(\phi,\psi,\theta) \iff (\phi^,\psi^,\theta^)\in Q_A

where

: $\phi^=\$

for an ''n''-tuple $\bar$ of variables.

Lindström quantifiers are classified according to the number structure of their parameters. For example $Qxy\phi(x)\psi(y)$ is a type (1,1) quantifier, whereas $Qxy\phi(x,y)$ is a type (2) quantifier. An example of type (1,1) quantifier is Hartig's quantifier testing equicardinality, i.e. the extension of . An example of a type (4) quantifier is the Henkin quantifier.

Expressiveness hierarchy

The first result in this direction was obtained by Lindström (1966) who showed that a type (1,1) quantifier was not definable in terms of a type (1) quantifier. After Lauri Hella (1989) developed a general technique for proving the relative expressiveness of quantifiers, the resulting hierarchy turned out to be lexicographically ordered by quantifier type:

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

For every type ''t'', there is a quantifier of that type that is not definable in first-order logic extended with quantifiers that are of types less than ''t''.

As precursors to Lindström's theorem

Although Lindström had only partially developed the hierarchy of quantifiers which now bear his name, it was enough for him to observe that some nice properties of first-order logic are lost when it is extended with certain generalized quantifiers. For example, adding a "there exist finitely many" quantifier results in a loss of compactness, whereas adding a "there exist uncountably many" quantifier to first-order logic results in a logic no longer satisfying the Löwenheim–Skolem theorem. In 1969 Lindström proved a much stronger result now known as Lindström's theorem, which intuitively states that first-order logic is the "strongest" logic having both properties.

Algorithmic characterization

References

*
* L. Hella. "Definability hierarchies of generalized quantifiers", Annals of Pure and Applied Logic, 43(3):235–271, 1989, .
* L. Hella. "Logical hierarchies in PTIME". In Proceedings of the 7th IEEE Symposium on Logic in Computer Science, 1992.
* L. Hella, K. Luosto, and J. Vaananen. "The hierarchy theorem for generalized quantifiers". ''Journal of Symbolic Logic'', 61(3):802–817, 1996.
*
*.
*

Further reading

* Jouko Väänanen (ed.), ''Generalized Quantifiers and Computation. 9th European Summer School in Logic, Language, and Information. ESSLLI’97 Workshop. Aix-en-Provence, France, August 11–22, 1997. Revised Lectures'', Springer Lecture Notes in Computer Science 1754,

External links

*Dag Westerståhl, 2011.
Generalized Quantifiers
. Stanford Encyclopedia of Philosophy.

{{DEFAULTSORT:Lindstrom quantifier
Finite model theory
Quantifier (logic)