A filter on is a consistent notion of largeness for subsets of
. “Largeness” has the following properties.
- if
is large and
then
is large
- if
and
are large then
is large
- the empty set is not large
At most one of and
is large; an ultrafilter is a filter which always has an opinion about which it is.
- either
or
is large
The usual notation for “ is large” is
, where
is the ultrafilter. This casts ultrafilters as sets, rather than notions of largeness. To bring the notion of largeness to the foreground we can use ultrafilter quantifiers; we write
, read “for
-most
,
holds” (where we have also identified
with the predicate “is a member of
“).
- if
and
then
- if
and
then
From this point of view says that the set of elements with property
is everything, and
that the set of elements with property
is non-empty.
behaves like a mixture of
and
, with the considerable advantage that logical operations pass through
unchanged without having to worry about De Morgan’s laws.
Adding ultrafilters
It turns out that the set of ultrafilters on is a model for the Stone–Čech compactification
of
.
is embedded as the set of principal ultrafilters (“
is large if and only if
“), and the addition on
extends to
:
(Here should be interpreted as
.) But to use this addition with quantifiers all we need to know is that
. If you can see that from the first definition then your brain is wired differently from mine.
It is a fact that there exist idempotent ultrafilters, with . Given such a
, we can play the following game. Suppose that
. Then
, so
and therefore
(by ANDing with the original assertion, and the original assertion with the dummy variable
replaced by
). In particular,
. But now we can fix a good choice of
and repeat the whole process with
in place of
to get that
Iterating, we eventually obtain an infinite sequence such that
holds for every sum of finitely many of the
. Together with the observation that whenever
is finitely coloured exactly one of the colour classes is
-large this proves Hindman’s theorem, that we can always find an infinite sequence
such that every sum of finitely many terms has the same colour.
A version of this argument with more of the details filled in is on the Tricki.