An operator—first introduced by Per Lindström (1936–2009)—that generalizes the truth conditions associated with the universal and existential quantifiers in classical logic. Generalized quantifiers are useful because they may provide formal accounts of many quantifier expressions that are too fine-grained to be captured by combinations of such quantifiers, e.g.,
In the first two cases, the appropriate kind of quantifier should have truth conditions such as:
where and bind instances of free variables and in the first and second subformulae, respectively. In the third case, however, an appropriate truth condition must involve more than one formula, as the number of elements satisfying ‘ is Alice’s apple’ and ‘ is Bob’s orange’ are being compared. A notion of type serves to classify generalized quantifiers, which is a tuple where the quantifier accepts arguments and binds many variables in formula . The quantifier in the third case binds one variable in each of two formulae, and is thus type . A well-known quantifier of type is the Härtig quantifier named for Klaus Härtig (1936–2013),
is type because it takes as arguments two formulae and binds a single variable in each.