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]