Английская Википедия:Filter quantifier
In mathematics, a filter on a set <math>X</math> informally gives a notion of which subsets <math>A \subseteq X</math> are "large". Filter quantifiers are a type of logical quantifier which, informally, say whether or not a statement is true for "most" elements of <math>X.</math> 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 <math>\mathcal{F}</math> on a set <math>X</math> is defined to be an order-theoretic filter in the poset <math>(\mathcal{P}(X), \subseteq),</math> that is, a subset of <math>\mathcal{P}(X)</math> such that:
- <math>\varnothing \notin \mathcal{F}</math> and <math>X \in \mathcal{F}</math>;
- For all <math>A, B \in \mathcal{F},</math> we have <math>A \cap B \in \mathcal{F}</math>;
- For all <math>A \subseteq B \subseteq X,</math> if <math>A \in \mathcal{F}</math> then <math>B \in \mathcal{F}.</math>
Recall a filter <math>\mathcal{F}</math> on <math>X</math> is an ultrafilter if, for every <math>A \subseteq X,</math> either <math>A \in \mathcal{F}</math> or <math>X \setminus A \in \mathcal{F}.</math>
Given a filter <math>\mathcal{F}</math> on a set <math>X,</math> we say a subset <math>A \subseteq X</math> is <math>\mathcal{F}</math>-stationary if, for all <math>B \in \mathcal{F},</math> we have <math>A \cap B \neq \varnothing.</math>[1]
Definition
Let <math>\mathcal{F}</math> be a filter on a set <math>X.</math> We define the filter quantifiers <math>\forall_\mathcal{F} x</math> and <math>\exists_\mathcal{F} x</math> as formal logical symbols with the following interpretation:
- <math>\forall_\mathcal{F} x\ \varphi(x) \iff \{ x \in X: \varphi(x) \} \in \mathcal{F}</math>
- <math>\exists_\mathcal{F} x\ \varphi(x) \iff \{ x \in X: \varphi(x) \}</math> is <math>\mathcal{F}</math>-stationary
for every first-order formula <math>\varphi(x)</math> with one free variable. These also admit alternative definitions as
- <math>\forall_\mathcal{F} x\ \varphi(x) \iff \exists A \in \mathcal{F}\ \ \forall x \in A\ \ \varphi(x)</math>
- <math>\exists_\mathcal{F} x\ \varphi(x) \iff \forall A \in \mathcal{F}\ \ \exists x \in A\ \ \varphi(x)</math>
When <math>\mathcal{F}</math> is an ultrafilter, the two quantifiers defined above coincide, and we will often use the notation <math>\mathcal{F} x</math> instead. Verbally, we might pronounce <math>\mathcal{F} x</math> as "for <math>\mathcal{F}</math>-almost all <math>x</math>", "for <math>\mathcal{F}</math>-most <math>x</math>", "for the majority of <math>x</math> (according to <math>\mathcal{F}</math>)", or "for most <math>x</math> (according to <math>\mathcal{F}</math>)". In cases where the filter is clear, we might omit mention of <math>\mathcal{F}.</math>
Properties
The filter quantifiers <math>\forall_\mathcal{F} x</math> and <math>\exists_\mathcal{F} x</math> satisfy the following logical identities,[1] for all formulae <math>\varphi, \psi</math>:
- Duality: <math>\forall_\mathcal{F} x\ \varphi(x) \iff \neg \exists_\mathcal{F} x\ \neg \varphi(x)</math>
- Weakening: <math>\forall x\ \varphi(x) \implies \forall_\mathcal{F} x\ \varphi(x) \implies \exists_\mathcal{F} x\ \varphi(x) \implies \exists x\ \varphi(x)</math>
- Conjunction:
- <math>\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)</math>
- <math>\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)</math>
- Disjunction:
- <math>\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)</math>
- <math>\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)</math>
- If <math>\mathcal{F} \subseteq \mathcal{G}</math> are filters on <math>X,</math> then:
- <math>\forall_\mathcal{F} x\ \varphi(x) \implies \forall_\mathcal{G} x\ \varphi(x)</math>
- <math>\exists_\mathcal{F} x\ \varphi(x) \;\Longleftarrow\; \exists_\mathcal{G} x\ \varphi(x)</math>
Additionally, if <math>\mathcal{F}</math> is an ultrafilter, the two filter quantifiers coincide: <math>\forall_\mathcal{F} x\ \varphi(x) \iff \exists_\mathcal{F} x\ \varphi(x).</math>Шаблон:Citation needed Renaming this quantifier <math>\mathcal{F} x,</math> the following properties hold:
- Negation: <math>\mathcal{F} x\ \varphi(x) \iff \neg \mathcal{F} x\ \neg \varphi(x)</math>
- Weakening: <math>\forall x\ \varphi(x) \implies \mathcal{F} x\ \varphi(x) \implies \exists x\ \varphi(x)</math>
- Conjunction: <math>\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)</math>
- Disjunction: <math>\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)</math>
In general, filter quantifiers do not commute with each other, nor with the usual <math>\forall</math> and <math>\exists</math> quantifiers.Шаблон:Citation needed
Examples
- If <math>\mathcal{F} = \{X\}</math> is the trivial filter on <math>X,</math> then unpacking the definition, we have <math>\forall_\mathcal{F} x\ \varphi(x) \iff \{x \in X: \varphi(x)\} = X,</math> and <math>\exists_\mathcal{F} x\ \varphi(x) \iff \{x \in X: \varphi(x)\} \cap X \neq \varnothing.</math> This recovers the usual <math>\forall</math> and <math>\exists</math> quantifiers.
- Let <math>\mathcal{F}^\infty</math> be the Fréchet filter on an infinite set <math>X,</math> Then, <math>\forall_{\mathcal{F}^\infty} x\ \varphi(x)</math> holds iff <math>\varphi(x)</math> holds for cofinitely many <math>x \in X,</math> and <math>\exists_{\mathcal{F}^\infty} x\ \varphi(x)</math> holds iff <math>\varphi(x)</math> holds for infinitely many <math>x \in X.</math> The quantifiers <math>\forall_{\mathcal{F}^\infty}</math> and <math>\exists_{\mathcal{F}^\infty}</math> are more commonly denoted <math>\forall^\infty</math> and <math>\exists^\infty,</math> respectively.
- Let <math>\mathcal{M}</math> be the "measure filter" on <math>[0, 1],</math> generated by all subsets <math>A \subseteq [0,1]</math> with Lebesgue measure <math>\mu(A) = 1.</math> The above construction gives us "measure quantifiers": <math>\forall_\mathcal{M} x\ \varphi(x)</math> holds iff <math>\varphi(x)</math> holds almost everywhere, and <math>\exists_\mathcal{M} x\ \varphi(x)</math> holds iff <math>\varphi(x)</math> holds on a set of positive measure.[2]
- Suppose <math>\mathcal{F}_A</math> is the principal filter on some set <math>A \subseteq X.</math> Then, we have <math>\forall_{\mathcal{F}_A} x\ \varphi(x) \iff \forall x \in A\ \varphi(x),</math> and <math>\exists_{\mathcal{F}_A} x\ \varphi(x) \iff \exists x \in A\ \varphi(x).</math>
- If <math>\mathcal{U}_d</math> is the principal ultrafilter of an element <math>d \in X,</math> then we have <math>\mathcal{U}_d\, x\ \varphi(x) \iff \varphi(d).</math>
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 <math>(a_n)_{n \in \N} \subseteq \R</math> converges to a point <math>a \in \R</math> if
- <math>\forall \varepsilon > 0\ \ \exists N \in \mathbb{N}\ \ \forall n \in \N\ \big(\ n \geq N \implies \vert a_n - a \vert < \varepsilon\ \big)</math>
Using the Fréchet quantifier <math>\forall^\infty</math> as defined above, we can give a nicer (equivalent) definition:
- <math>\forall \varepsilon > 0\ \ \forall^\infty n \in \mathbb{N}:\ \vert a_n - a \vert < \varepsilon</math>
Filter quantifiers are especially useful in constructions involving filters. As an example, suppose that <math>X</math> has a binary operation <math>+</math> defined on it. There is a natural way to extend[3] <math>+</math> to <math>\beta X,</math> the set of ultrafilters on <math>X</math>:[4]
- <math>\mathcal{U} \oplus \mathcal{V} = \big\{ A \subseteq X :\ \mathcal{U}x\ \mathcal{V}y\ \ x+y \in A \big\}</math>
With an understanding of the ultrafilter quantifier, this definition is reasonably intuitive. It says that <math>\mathcal{U} \oplus \mathcal{V}</math> is the collection of subsets <math>A \subseteq X</math> such that, for most <math>x</math> (according to <math>\mathcal{U}</math>) and for most <math>y</math> (according to <math>\mathcal{V}</math>), the sum <math>x+y</math> is in <math>A.</math> Compare this to the equivalent definition without ultrafilter quantifiers:
- <math>\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\}</math>
The meaning of this is much less clear.
This increased intuition is also evident in proofs involving ultrafilters. For example, if <math>+</math> is associative on <math>X,</math> using the first definition of <math>\oplus,</math> it trivially follows that <math>\oplus</math> is associative on <math>\beta X.</math> Proving this using the second definition takes a lot more work.[5]
See also
- Шаблон:Annotated link
- Шаблон:Annotated link
- Шаблон:Annotated link
- Шаблон:Annotated link
- Шаблон:Annotated link
- Шаблон:Annotated link
References
- ↑ 1,0 1,1 Шаблон:Cite web
- ↑ Шаблон:Cite web
- ↑ This is an extension of <math>+</math> in the sense that we can consider <math>X</math> as a subset of <math>\beta X</math> by mapping each <math>x \in X</math> to the principal ultrafilter <math>\mathcal{U}_x</math> on <math>x.</math> Then, we have <math>\mathcal{U}_x \oplus \mathcal{U}_y = \mathcal{U}_{(x+y)}.</math>
- ↑ Шаблон:Cite web
- ↑ Шаблон:Cite book
