Filter quantifier
In mathematics, a filter on a set formula_1 informally gives a notion of which subsets formula_2 are "large". Filter quantifiers are a type of logical quantifier which, informally, say whether or not a statement is true for "most" elements of formula_1. Such quantifiers are often used in combinatorics, model theory (such as when dealing with ultraproducts), and in other fields of mathematical logic where (ultra)filters are used. Background. Here we will use the set theory convention, where a filter formula_4 on a set formula_1 is defined to be an order-theoretic filter in the poset formula_6, i.e. a  subset of formula_7 such that: Recall a filter formula_4 on formula_1 is an "ultrafilter" if, for every formula_2, either formula_13 or formula_19. Given a filter formula_4 on a set formula_1, we say a subset formula_2 is "formula_4-stationary" if, for all formula_14, we have formula_25. Definition. Let formula_4 be a filter on a set formula_1. We define the "filter quantifiers" formula_28 and formula_29 as formal logical symbols with the following interpretation: for every first-order formula formula_33 with one free variable. These also admit alternative definitions as When formula_4 is an ultrafilter, the two quantifiers defined above coincide, and we  will often use the notation formula_37 instead. Verbally, we might pronounce formula_37 as "for formula_4-almost all formula_40", "for formula_4-most formula_40", "for the majority of formula_40 (according to formula_4)", or "for most formula_40 (according to formula_4)". In cases where the filter is clear, we might omit mention of formula_4. Properties. The filter quantifiers formula_28 and formula_29 satisfy the following logical identities, for all formulae formula_50: Additionally, if formula_4 is an ultrafilter, the two filter quantifiers coincide: formula_62. Renaming this quantifier formula_37, the following properties hold: In general, filter quantifiers do not commute with each other, nor with the usual  formula_68 and formula_69 quantifiers. Use. The utility of filter quantifiers is that they often give a more concise or clear way to express certain mathematical ideas. For example, take the definition of convergence of a real-valued sequence: a sequence formula_103 converges to a point formula_104 if Using the Fréchet quantifier formula_86 as defined above, we can give a nicer (equivalent) definition: Filter quantifiers are especially useful in constructions involving filters. As an example, suppose that formula_1 has a binary operation formula_109 defined on it. There is a natural way to extend formula_109 to formula_111, the set of ultrafilters on  formula_1: With an understanding of the ultrafilter quantifier, this definition is reasonably intuitive. It says that formula_114 is the collection of subsets formula_2 such that, for most formula_40 (according to formula_117) and for most formula_118 (according to formula_119), the sum formula_120 is in formula_121. Compare this to the equivalent definition without ultrafilter quantifiers: The meaning of this is much less clear. This increased intuition is also evident in proofs involving ultrafilters. For example, if formula_109 is associative on formula_1, using the first definition of formula_125, it trivially follows that formula_125 is associative on formula_111. Proving this using the second definition  takes a lot more work.