en>David Eppstein: rewrite with more context and references

2014-01-28T23:17:04Z

rewrite with more context and references

New page

In [[mathematical logic]], a '''Lindström quantifier''' is a [[generalized quantifier|generalized polyadic quantifier]]. They are a generalization of first-order quantifiers, such as the [[existential quantifier]], the [[universal quantifier]], and the [[counting quantifier]]s. They were introduced by [[Per Lindström]] in 1966. They were later studied for their applications in [[logic in computer science]] and database [[query language]]s.

==Generalization of first-order quantifiers==
In order to facilitate discussion, some notational conventions need explaining. The expression

: <math>\phi^{A,x,\bar{a}}=\{x\in A\colon A\models\phi[x,\bar{a}]\}</math>

for ''A'' an ''L''-structure (or ''L''-model) in a language ''L'',''φ'' an ''L''-formula, and <math>\bar{a}</math> a tuple of elements of the domain dom(''A'') of ''A''.{{clarify|reason=The verb-phrase of the preceding sentence seems to be missing.|date=October 2013}} In other words, <math>\phi^{A,x,\bar{a}}</math> denotes a ([[monadic (arity)|monadic]]) property defined on dom(A). In general, where ''x'' is replaced by an ''n''-tuple <math>\bar{x}</math> of free variables, <math>\phi^{A,\bar{x},\bar{a}}</math> denotes an ''n''-ary relation defined on dom(''A''). Each quantifier <math>Q_A</math> 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

: <math>A\models\forall x\phi[x,\bar{a}] \iff \phi^{A,x,\bar{a}}\in\forall_A</math>
: <math>A\models\exists x\phi[x,\bar{a}] \iff \phi^{A,x,\bar{a}}\in\exists_A,</math>

where <math>\forall_A</math> is the singleton whose sole member is dom(''A''), and <math>\exists_A</math> 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 a structure, each of which has a cardinality off size ''n''. Then, "there are exactly 2 things such that φ" is true in A iff 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 <math>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))</math> is defined semantically as

: <math>A\models Q_Ax_1x_2y_1z_1z_2z_3(\phi,\psi,\theta)[a] \iff (\phi^{A,x_1x_2,\bar{a}},\psi^{A,y_1,\bar{a}},\theta^{A,z_1z_2z_3,\bar{a}})\in Q_A</math> {{clarify|reason=The 'a' on the left hand side of ⇔ should have an overline?|date=October 2013}}

where

: <math>\phi^{A,\bar{x},\bar{a}}=\{(x_1,\dots,x_n)\in A^n\colon A\models\phi[\bar{x},\bar{a}]\}</math>

for an ''n''-tuple <math>\bar{x}</math> of variables.

Lindström quantifiers are classified according to the number structure of their parameters. For example <math>Qxy\phi(x)\psi(y)</math> is a type (1,1) quantifier, whereas <math>Qxy\phi(x,y)</math> is a type (2) quantifier. An example of type (1,1) quantifier is [[Hartig's quantifier]] testing equicardinality, i.e. the extension of {A, B ⊆ M: |A| = |B|}.{{clarify|reason=Should be the set of pairs of equal cardinality { (A,B): A,B ⊆ M and !A! = !B!} ?|date=October 2013}} 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 [[Lexicographical order|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 theorem|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 know as [[Lindström's theorem]], which intuitively states that first-order logic is the "strongest" logic having both properties.

== Algorithmic characterization ==
{{empty section|date=October 2012}}

==References==
* P. Lindstrom. "First order predicate logic with generalized quantifiers". ''[[Theoria (philosophy journal)|Theoria]]'', 32, 1966, {{doi|10.1111/j.1755-2567.1966.tb00600.x}}
* L. Hella. "Definability hierarchies of generalized quantifiers", [[Annals of Pure and Applied Logic]], 43(3):235–271, 1989, {{doi|10.1016/0168-0072(89)90070-5}}.
* 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.
*{{citation | last1 = Burtschick | first1 = Hans-Jörg | first2 = Heribert | last2= Vollmer | title = Lindström Quantifiers and Leaf Language Definability | id={{ECCC|1996|96|005}}| year = 1999}}
*{{citation|first=Dag|last=Westerståhl|contribution=Quantifiers|title=The Blackwell Guide to Philosophical Logic|editor-first=Lou|editor-last=Goble|publisher=Blackwell Publishing|year=2001|pages=437–460}}.
* {{cite book|author=Antonio Badia|title=Quantifiers in Action: Generalized Quantification in Query, Logical and Natural Languages|year=2009|publisher=Springer|isbn=978-0-387-09563-9}}

== 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, ISBN 3-540-66993-0

== External links ==
*Dag Westerståhl, 2011. '[http://plato.stanford.edu/entries/generalized-quantifiers/ Generalized Quantifiers]'. [[Stanford Encyclopedia of Philosophy]].

{{DEFAULTSORT:Lindstrom quantifier}}
[[Category:Finite model theory]]
[[Category:Quantification]]

Continuous knapsack problem - Revision history

en>David Eppstein: rewrite with more context and references