# Filter quantifier

In mathematics, a filter on a set $X$ informally gives a notion of which subsets $A\subseteq X$ are "large". Filter quantifiers are a type of logical quantifier which, informally, say whether or not a statement is true for "most" elements of $X.$ 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 ${\mathcal {F}}$ on a set $X$ is defined to be an order-theoretic proper filter in the poset $({\mathcal {P}}(X),\subseteq ),$ that is, a subset of ${\mathcal {P}}(X)$ such that:
* $\varnothing \notin {\mathcal {F}}$ and $X\in {\mathcal {F}}$;
* For all $A,B\in {\mathcal {F}},$ we have $A\cap B\in {\mathcal {F}}$;
* For all $A\subseteq B\subseteq X,$ if $A\in {\mathcal {F}}$ then $B\in {\mathcal {F}}.$
Recall a filter ${\mathcal {F}}$ on $X$ is an ultrafilter if, for every $A\subseteq X,$ either $A\in {\mathcal {F}}$ or $X\setminus A\in {\mathcal {F}}.$
Given a filter ${\mathcal {F}}$ on a set $X,$ we say a subset $A\subseteq X$ is ${\mathcal {F}}$-stationary if, for all $B\in {\mathcal {F}},$ we have $A\cap B\neq \varnothing .$

## Definition

Let ${\mathcal {F}}$ be a filter on a set $X.$ We define the filter quantifiers $\forall _{\mathcal {F}}x$ and $\exists _{\mathcal {F}}x$ as formal logical symbols with the following interpretation:
    $\forall _{\mathcal {F}}x\ \varphi (x)\iff \{x\in X:\varphi (x)\}\in {\mathcal {F}}$
    $\exists _{\mathcal {F}}x\ \varphi (x)\iff \{x\in X:\varphi (x)\}$ is ${\mathcal {F}}$-stationary
for every first-order formula $\varphi (x)$ with one free variable. These also admit alternative definitions as
    $\forall _{\mathcal {F}}x\ \varphi (x)\iff \exists A\in {\mathcal {F}}\ \ \forall x\in A\ \ \varphi (x)$
    $\exists _{\mathcal {F}}x\ \varphi (x)\iff \forall A\in {\mathcal {F}}\ \ \exists x\in A\ \ \varphi (x)$
When ${\mathcal {F}}$ is an ultrafilter, the two quantifiers defined above coincide, and we will often use the notation ${\mathcal {F}}x$ instead. Verbally, we might pronounce ${\mathcal {F}}x$ as "for ${\mathcal {F}}$-almost all $x$", "for ${\mathcal {F}}$-most $x$", "for the majority of $x$ (according to ${\mathcal {F}}$)", or "for most $x$ (according to ${\mathcal {F}}$)". In cases where the filter is clear, we might omit mention of ${\mathcal {F}}.$

## Properties

The filter quantifiers $\forall _{\mathcal {F}}x$ and $\exists _{\mathcal {F}}x$ satisfy the following logical identities, for all formulae $\varphi ,\psi$:
* Duality: $\forall _{\mathcal {F}}x\ \varphi (x)\iff \neg \exists _{\mathcal {F}}x\ \neg \varphi (x)$
* Weakening: $\forall x\ \varphi (x)\implies \forall _{\mathcal {F}}x\ \varphi (x)\implies \exists _{\mathcal {F}}x\ \varphi (x)\implies \exists x\ \varphi (x)$
* Conjunction:
** $\forall _{\mathcal {F}}x\ {\big\varphi (x)\land \psi (x){\big )}\iff {\big\forall _{\mathcal {F}}x\ \varphi (x){\big )}\land {\big\forall _{\mathcal {F}}x\ \psi (x){\big )}$
** $\exists _{\mathcal {F}}x\ {\big\varphi (x)\land \psi (x){\big )}\implies {\big\exists _{\mathcal {F}}x\ \varphi (x){\big )}\land {\big\exists _{\mathcal {F}}x\ \psi (x){\big )}$
* Disjunction:
** $\forall _{\mathcal {F}}x\ {\big\varphi (x)\lor \psi (x){\big )}\;\Longleftarrow \;{\big\forall _{\mathcal {F}}x\ \varphi (x){\big )}\lor {\big\forall _{\mathcal {F}}x\ \psi (x){\big )}$
** $\exists _{\mathcal {F}}x\ {\big\varphi (x)\lor \psi (x){\big )}\;\Longleftrightarrow \;{\big\exists _{\mathcal {F}}x\ \varphi (x){\big )}\lor {\big\exists _{\mathcal {F}}x\ \psi (x){\big )}$
* If ${\mathcal {F}}\subseteq {\mathcal {G}}$ are filters on $X,$ then:
** $\forall _{\mathcal {F}}x\ \varphi (x)\implies \forall _{\mathcal {G}}x\ \varphi (x)$
** $\exists _{\mathcal {F}}x\ \varphi (x)\;\Longleftarrow \;\exists _{\mathcal {G}}x\ \varphi (x)$
Additionally, if ${\mathcal {F}}$ is an ultrafilter, the two filter quantifiers coincide: $\forall _{\mathcal {F}}x\ \varphi (x)\iff \exists _{\mathcal {F}}x\ \varphi (x).$ Renaming this quantifier ${\mathcal {F}}x,$ the following properties hold:
* Negation: ${\mathcal {F}}x\ \varphi (x)\iff \neg {\mathcal {F}}x\ \neg \varphi (x)$
* Weakening: $\forall x\ \varphi (x)\implies {\mathcal {F}}x\ \varphi (x)\implies \exists x\ \varphi (x)$
* Conjunction: ${\mathcal {F}}x\ {\big\varphi (x)\land \psi (x){\big )}\iff {\big{\mathcal {F}}x\ \varphi (x){\big )}\land {\big{\mathcal {F}}x\ \psi (x){\big )}$
* Disjunction: ${\mathcal {F}}x\ {\big\varphi (x)\lor \psi (x){\big )}\iff {\big{\mathcal {F}}x\ \varphi (x){\big )}\lor {\big{\mathcal {F}}x\ \psi (x){\big )}$
In general, filter quantifiers do not commute with each other, nor with the usual $\forall$ and $\exists$ quantifiers.

## Examples

* If ${\mathcal {F}}=\{X\}$ is the trivial filter on $X,$ then unpacking the definition, we have $\forall _{\mathcal {F}}x\ \varphi (x)\iff \{x\in X:\varphi (x)\}=X,$ and $\exists _{\mathcal {F}}x\ \varphi (x)\iff \{x\in X:\varphi (x)\}\cap X\neq \varnothing .$ This recovers the usual $\forall$ and $\exists$ quantifiers.
* Let ${\mathcal {F}}^{\infty }$ be the Fréchet filter on an infinite set $X,$ Then, $\forall _{{\mathcal {F}}^{\infty }}x\ \varphi (x)$ holds iff $\varphi (x)$ holds for cofinitely many $x\in X,$ and $\exists _{{\mathcal {F}}^{\infty }}x\ \varphi (x)$ holds iff $\varphi (x)$ holds for infinitely many $x\in X.$ The quantifiers $\forall _{{\mathcal {F}}^{\infty }}$ and $\exists _{{\mathcal {F}}^{\infty }}$ are more commonly denoted $\forall ^{\infty }$ and $\exists ^{\infty },$ respectively.
* Let ${\mathcal {M}}$ be the "measure filter" on $[0,1],$ generated by all subsets $A\subseteq [0,1]$ with Lebesgue measure $\mu (A)=1.$ The above construction gives us "measure quantifiers": $\forall _{\mathcal {M}}x\ \varphi (x)$ holds iff $\varphi (x)$ holds almost everywhere, and $\exists _{\mathcal {M}}x\ \varphi (x)$ holds iff $\varphi (x)$ holds on a set of positive measure.
* Suppose ${\mathcal {F}}_{A}$ is the principal filter on some set $A\subseteq X.$ Then, we have $\forall _{{\mathcal {F}}_{A}}x\ \varphi (x)\iff \forall x\in A\ \varphi (x),$ and $\exists _{{\mathcal {F}}_{A}}x\ \varphi (x)\iff \exists x\in A\ \varphi (x).$
** If ${\mathcal {U}}_{d}$ is the principal ultrafilter of an element $d\in X,$ then we have ${\mathcal {U}}_{d}\,x\ \varphi (x)\iff \varphi (d).$

## 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 $(a_{n})_{n\in \mathbb {N} }\subseteq \mathbb {R}$ converges to a point $a\in \mathbb {R}$ if
    $\forall \varepsilon >0\ \ \exists N\in \mathbb {N} \ \ \forall n\in \mathbb {N} \ {\big\ n\geq N\implies \vert a_{n}-a\vert <\varepsilon \ {\big )}$
Using the Fréchet quantifier $\forall ^{\infty }$ as defined above, we can give a nicer (equivalent) definition:
    $\forall \varepsilon >0\ \ \forall ^{\infty }n\in \mathbb {N} :\ \vert a_{n}-a\vert <\varepsilon$
Filter quantifiers are especially useful in constructions involving filters. As an example, suppose that $X$ has a binary operation $+$ defined on it. There is a natural way to extend $+$ to $\beta X,$ the set of ultrafilters on $X$:
    ${\mathcal {U}}\oplus {\mathcal {V}}={\big \A\subseteq X:\ {\mathcal {U}}x\ {\mathcal {V}}y\ \ x+y\in A{\big \}}$
With an understanding of the ultrafilter quantifier, this definition is reasonably intuitive. It says that ${\mathcal {U}}\oplus {\mathcal {V}}$ is the collection of subsets $A\subseteq X$ such that, for most $x$ (according to ${\mathcal {U}}$) and for most $y$ (according to ${\mathcal {V}}$), the sum $x+y$ is in $A.$ Compare this to the equivalent definition without ultrafilter quantifiers:
    ${\mathcal {U}}\oplus {\mathcal {V}}={\big \A\subseteq X:\ \{x\in X:\ \{y\in X:\ x+y\in A\}\in {\mathcal {V}}\}\in {\mathcal {U}}{\big \}}$
The meaning of this is much less clear.
This increased intuition is also evident in proofs involving ultrafilters. For example, if $+$ is associative on $X,$ using the first definition of $\oplus ,$ it trivially follows that $\oplus$ is associative on $\beta X.$ Proving this using the second definition takes a lot more work.