In mathematics, a filter on a set informally gives a notion of which subsets are "large". Filter quantifiers are a type of logical quantifier which, informally, say whether or not a statement is true for "most" elements of 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.
Here we will use the set theory convention, where a filter on a set is defined to be an order-theoretic proper filter in the poset that is, a subset of such that:
- and ;
- For all we have ;
- For all if then
Recall a filter on is an ultrafilter if, for every either or
Given a filter on a set we say a subset is -stationary if, for all we have [1]
Let be a filter on a set We define the filter quantifiers and as formal logical symbols with the following interpretation:
- is -stationary
for every first-order formula with one free variable. These also admit alternative definitions as
When is an ultrafilter, the two quantifiers defined above coincide, and we will often use the notation instead. Verbally, we might pronounce as "for -almost all ", "for -most ", "for the majority of (according to )", or "for most (according to )". In cases where the filter is clear, we might omit mention of
The filter quantifiers and satisfy the following logical identities,[1] for all formulae :
- Duality:
- Weakening:
- Conjunction:
- Disjunction:
- If are filters on then:
Additionally, if is an ultrafilter, the two filter quantifiers coincide: [citation needed] Renaming this quantifier the following properties hold:
- Negation:
- Weakening:
- Conjunction:
- Disjunction:
In general, filter quantifiers do not commute with each other, nor with the usual and quantifiers.[citation needed]
- If is the trivial filter on then unpacking the definition, we have and This recovers the usual and quantifiers.
- Let be the Fréchet filter on an infinite set Then, holds iff holds for cofinitely many and holds iff holds for infinitely many The quantifiers and are more commonly denoted and respectively.
- Let be the "measure filter" on generated by all subsets with Lebesgue measure The above construction gives us "measure quantifiers": holds iff holds almost everywhere, and holds iff holds on a set of positive measure.[2]
- Suppose is the principal filter on some set Then, we have and
- If is the principal ultrafilter of an element then we have
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 converges to a point if
Using the Fréchet quantifier as defined above, we can give a nicer (equivalent) definition:
Filter quantifiers are especially useful in constructions involving filters. As an example, suppose that has a binary operation defined on it. There is a natural way to extend[3] to the set of ultrafilters on :[4]
With an understanding of the ultrafilter quantifier, this definition is reasonably intuitive. It says that is the collection of subsets such that, for most (according to ) and for most (according to ), the sum is in 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 is associative on using the first definition of it trivially follows that is associative on Proving this using the second definition takes a lot more work.[5]