fbpx
Wikipedia

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

 

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.[clarification needed] 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 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

 [clarification needed]

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 {A, B ⊆ M: |A| = |B|}.[clarification needed] 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

  • Lindstrom, P. (1966). "First order predicate logic with generalized quantifiers". Theoria. 32 (3): 186–195. 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.
  • Burtschick, Hans-Jörg; Vollmer, Heribert (1999), Lindström Quantifiers and Leaf Language Definability, ECCC TR96-005
  • Westerståhl, Dag (2001), "Quantifiers", in Goble, Lou (ed.), The Blackwell Guide to Philosophical Logic, Blackwell Publishing, pp. 437–460.
  • Antonio Badia (2009). Quantifiers in Action: Generalized Quantification in Query, Logical and Natural Languages. 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

lindström, quantifier, mathematical, logic, generalized, polyadic, quantifier, generalize, first, order, quantifiers, such, existential, quantifier, universal, quantifier, counting, quantifiers, they, were, introduced, lindström, 1966, they, were, later, studi. In mathematical logic a Lindstrom quantifier is a generalized polyadic quantifier Lindstrom quantifiers generalize first order quantifiers such as the existential quantifier the universal quantifier and the counting quantifiers They were introduced by Per Lindstrom in 1966 They were later studied for their applications in logic in computer science and database query languages Contents 1 Generalization of first order quantifiers 2 Expressiveness hierarchy 3 As precursors to Lindstrom s theorem 4 Algorithmic characterization 5 References 6 Further reading 7 External linksGeneralization of first order quantifiers EditIn order to facilitate discussion some notational conventions need explaining The expression ϕ A x a x A A ϕ x a displaystyle phi A x bar a x in A colon A models phi x bar a for A an L structure or L model in a language L f an L formula and a displaystyle bar a a tuple of elements of the domain dom A of A clarification needed In other words ϕ A x a displaystyle phi A x bar a denotes a monadic property defined on dom A In general where x is replaced by an n tuple x displaystyle bar x of free variables ϕ A x a displaystyle phi A bar x bar a denotes an n ary relation defined on dom A Each quantifier Q A displaystyle 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 x ϕ x a ϕ A x a A displaystyle A models forall x phi x bar a iff phi A x bar a in forall A A x ϕ x a ϕ A x a A displaystyle A models exists x phi x bar a iff phi A x bar a in exists A where A displaystyle forall A is the singleton whose sole member is dom A and A displaystyle 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 gt 0 ary relation between properties on dom A is called monadic Lindstrom introduced polyadic ones that are n gt 0 ary relations between relations on domains of structures Before we go on to Lindstrom 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 f is true in A iff the set of things that are such that f is a member of the set of all subsets of dom A of size 2 A Lindstrom 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 ϕ x 1 x 2 ps y 1 8 z 1 z 2 z 3 displaystyle 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 Q A x 1 x 2 y 1 z 1 z 2 z 3 ϕ ps 8 a ϕ A x 1 x 2 a ps A y 1 a 8 A z 1 z 2 z 3 a Q A displaystyle A models Q A x 1 x 2 y 1 z 1 z 2 z 3 phi psi theta a iff 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 clarification needed where ϕ A x a x 1 x n A n A ϕ x a displaystyle phi A bar x bar a x 1 dots x n in A n colon A models phi bar x bar a for an n tuple x displaystyle bar x of variables Lindstrom quantifiers are classified according to the number structure of their parameters For example Q x y ϕ x ps y displaystyle Qxy phi x psi y is a type 1 1 quantifier whereas Q x y ϕ x y displaystyle 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 A B M A B clarification needed An example of a type 4 quantifier is the Henkin quantifier Expressiveness hierarchy EditThe first result in this direction was obtained by Lindstrom 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 lt 1 1 lt lt 2 lt 2 1 lt 2 1 1 lt lt 2 2 lt 3 lt dd 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 Lindstrom s theorem EditAlthough Lindstrom 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 Lowenheim Skolem theorem In 1969 Lindstrom proved a much stronger result now known as Lindstrom s theorem which intuitively states that first order logic is the strongest logic having both properties Algorithmic characterization EditThis section is empty You can help by adding to it October 2012 References EditLindstrom P 1966 First order predicate logic with generalized quantifiers Theoria 32 3 186 195 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 Burtschick Hans Jorg Vollmer Heribert 1999 Lindstrom Quantifiers and Leaf Language Definability ECCC TR96 005 Westerstahl Dag 2001 Quantifiers in Goble Lou ed The Blackwell Guide to Philosophical Logic Blackwell Publishing pp 437 460 Antonio Badia 2009 Quantifiers in Action Generalized Quantification in Query Logical and Natural Languages Springer ISBN 978 0 387 09563 9 Further reading EditJouko Vaananen 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 0External links EditDag Westerstahl 2011 Generalized Quantifiers Stanford Encyclopedia of Philosophy Retrieved from https en wikipedia org w index php title Lindstrom quantifier amp oldid 1070602920, wikipedia, wiki, book, books, library,

article

, read, download, free, free download, mp3, video, mp4, 3gp, jpg, jpeg, gif, png, picture, music, song, movie, book, game, games.