In
mathematical logic
Mathematical logic is the study of logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of for ...
, a Lindström quantifier is a
generalized polyadic quantifier. Lindström quantifiers generalize first-order quantifiers, such as the
existential quantifier
In predicate logic, an existential quantification is a type of quantifier, a logical constant which is interpreted as "there exists", "there is at least one", or "for some". It is usually denoted by the logical operator symbol ∃, which, w ...
, the
universal quantifier, and the
counting quantifiers. They were introduced by
Per Lindström
Per "Pelle" Lindström (9 April 1936 – 21 August 2009, Gothenburg) ASLbr>Newsletter September 2009 was a Swedish logician, after whom Lindström's theorem and the Lindström quantifier are named. (He also independently discovered Ehrenfeucht– ...
in 1966. They were later studied for their applications in
logic in computer science
Logic in computer science covers the overlap between the field of logic and that of computer science. The topic can essentially be divided into three main areas:
* Theoretical foundations and analysis
* Use of computer technology to aid logicians ...
and database
query language
Query languages, data query languages or database query languages (DQL) are computer languages used to make queries in databases and information systems. A well known example is the Structured Query Language (SQL).
Types
Broadly, query language ...
s.
Generalization of first-order quantifiers
In order to facilitate discussion, some notational conventions need explaining. The expression
:
for ''A'' an ''L''-structure (or ''L''-model) in a language ''L'', ''φ'' an ''L''-formula, and
a tuple of elements of the domain dom(''A'') of ''A''. In other words,
denotes a (
monadic) property defined on dom(A). In general, where ''x'' is replaced by an ''n''-tuple
of free variables,
denotes an ''n''-ary relation defined on dom(''A''). Each quantifier
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
:
:
where
is the singleton whose sole member is dom(''A''), and
is the set of all non-empty subsets of dom(''A'') (i.e. the
power set
In mathematics, the power set (or powerset) of a set is the set of all subsets of , including the empty set and itself. In axiomatic set theory (as developed, for example, in the ZFC axioms), the existence of the power set of any set is post ...
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 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
is defined semantically as
:
where
:
for an ''n''-tuple
of variables.
Lindström quantifiers are classified according to the number structure of their parameters. For example
is a type (1,1) quantifier, whereas
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 In logic a branching quantifier, also called a Henkin quantifier, finite partially ordered quantifier or even nonlinear quantifier, is a partial ordering
:\langle Qx_1\dots Qx_n\rangle
of quantifiers for ''Q'' ∈ . It is a special case ...
.
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 In mathematical logic, Lindström's theorem (named after Swedish logician Per Lindström, who published it in 1969) states that first-order logic is the '' strongest logic'' (satisfying certain conditions, e.g. closure under classical negation) h ...
, 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
The ACM–IEEE Symposium on Logic in Computer Science (LICS) is an annual academic conference on the theory and practice of computer science in relation to mathematical logic. Extended versions of selected papers of each year's conference appear i ...
, 1992.
* L. Hella, K. Luosto, and
J. Vaananen. "The hierarchy theorem for generalized quantifiers". ''
Journal of Symbolic Logic
The '' Journal of Symbolic Logic'' is a peer-reviewed mathematics journal published quarterly by Association for Symbolic Logic. It was established in 1936 and covers mathematical logic. The journal is indexed by '' Mathematical Reviews'', Zentra ...
'', 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
''Lecture Notes in Computer Science'' is a series of computer science books published by Springer Science+Business Media since 1973.
Overview
The series contains proceedings, post-proceedings, monographs, and Festschrifts. In addition, tutorial ...
1754,
External links
*Dag Westerståhl, 2011.
Generalized Quantifiers.
Stanford Encyclopedia of Philosophy.
{{DEFAULTSORT:Lindstrom quantifier
Finite model theory
Quantifier (logic)