Modal Quantification over Structured Domains

this paper can be viewed both as a new semantics for generalized quantifiers and as a new look at standard first-order quantification, bringing the latter closer to modal logic. The standard semantics for generalized quantifiers interprets a monadic generalized quantifier Q as a set of subsets of a domain. For example, the quantifier "there are precisely two" is interpreted by the set of all subsets of the domain which contain precisely two elements. A formula Qx' is true in a model if the set of elements satisfying ' belongs to the interpretation of the quantifier; in our example, if there are precisely two elements satisfying '. The existential quantifier can be treated as a generalized quantifier, too: it is interpreted as the set of all non-empty subsets of the domain. The universal quantifier is interpreted by the singleton set containing the whole domain. The quantifiers listed so far are first-order definable in the following sense: they can be defined using ordinary quantifiers and equality. Many interesting generalized quantifiers are not first-order definable. The present study is motivated by the work of Michiel van Lambalgen (1991) on Gentzen-style proof theory for the quantifiers "for many" (its dual is interpreted as a non-principal filter), "for uncountably many" and "for almost all" (the latter contains all subsets of the domain which have Lebesgue measure 1). All those quantifiers are not first-order definable. They have Hilbert-style axiomatizations, but until lately no one believed that they can have a reasonable Gentzen-style proof theory. In order to devise such a proof theory, van Lambalgen used a translation of generalized quantifier formulas into a first-order language enriched with a predicate R of indefinite arity