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 ").
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.
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 :
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
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.