Filter quantifier

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, and in other fields of mathematical logic where filters are used.

Background

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

Definition

Let be a filter on a set We define the filter quantifiers and as formal logical symbols with the following interpretation:
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 ", or "for most ". In cases where the filter is clear, we might omit mention of

Properties

The filter quantifiers and satisfy the following logical identities, for all formulae :

Duality:
Weakening:
Conjunction:
*
*
Disjunction:
*
*
If are filters on then:
*
*

Additionally, if is an ultrafilter, the two filter quantifiers coincide: 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.

Examples

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.
Suppose is the principal filter on some set Then, we have and
* If is the principal ultrafilter of an element then we have

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 converges to a point if
Using the Fréchet quantifier as defined above, we can give a nicer 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 to the set of ultrafilters on :
With an understanding of the ultrafilter quantifier, this definition is reasonably intuitive. It says that is the collection of subsets such that, for most and for most, 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.