Formalising Ramsey theory, I
[Ramsey's theorem To quote Herbert Ryser, Ramsey’s theorem is “a profound generalisation” of the pigeon-hole principle, which “asserts that if a set of sufficiently many elements is partitioned into not too many subsets, then at least one of the subsets must contain many of the elements”. Ramsey’s theorem initiated a new branch of infinitary combinatorics and is also the key to today’s software termination checkers.
Ramsey’s theorem in its finite and infinite forms
The theorem is often expressed in terms of graphs: if $p$ and $q$ are given positive integers then there exists some $k$ such that if the edges of any complete graph with at least $k$ vertices are coloured red and blue then it will contain either a blue clique on $p$ vertices or a red clique on $q$ vertices. (The colours represent a partitioning of the set of edges into two disjoint parts.) However, this graph-theoretic version understates Ramsey’s theorem almost as much as the pigeon-hole principle does.
To state Ramsey’s theorem properly, we need the concept of an $n$-set, which is simply a set containing $n$ elements for some integer $n$. The pigeon-hole principle is Ramsey’s theorem where $n=1$. The graph-theoretic version is where $n=2$. However, the theorem holds for all positive $n$. This is sometimes called the hypergraph version, with the $n$-sets referred to as hyperedges.
The full (finite) version of Ramsey’s theorem states that, for any positive integers $m_0$, $m_1$ and $n$, there is an integer $k$ such that for every set $X$ having at least $k$ elements, if we partition the $n$-subsets of $X$ into two parts, then there is a $m_i$-subset $Y_i\subseteq X$ for $i<2$ such that every $n$-subset of $Y$ is in the same part $i$ of the partition. The proof is by induction on $n$, and within that, by induction on $m_0+m_1$. When $n=0$ the theorem is trivial, as there exists only one 0-set. I was unable to find a good proof online, so the Isabelle version is based on an old textbook of mine: Combinatorial Mathematics by Herbert Ryser (CUP, 2014). This classic text (dated 1963) is still in print.
The theorem is easily generalised to multiple colours. Identifying two of the colours (let’s call the result grey) reduces their number. That observation allows an inductive argument with a further application of the two-colour version of the theorem in case the selected partition is the grey one.
Variants and extensions
Ramsey also proved an infinite version of the theorem stating that if $n$ is a positive integer and we partition the $n$-subsets of a given infinite set $X$ into multiple parts then there is an infinite subset $Y\subseteq X$ such that every $n$-subset of $Y$ is in the same part.
Ramsey’s theorem has been generalised in several directions. The most obvious of these is to go from finite integers to infinite cardinals and thus from finite subsets to subsets of specified infinite cardinalities. A separate direction is to consider transfinite ordinals. Here we have more complexity, as we are dealing with subsets of ordered sets (typically themselves ordinals) and the Ramsey property concerns the order types of those subsets. Yet another generalisation, due to Nash-Williams, relaxes the condition that the subsets of $X$ all have the same size. Many of these results have been formalised in Isabelle and will be covered in future posts.
Application to program termination
Ramsey’s theorem has innumerable applications in combinatorial mathematics. A remarkable and unexpected application is to prove program termination. The unsolvability of the halting problem is of little relevance to software, where programs are generally expected to terminate for trivial reasons. A well-designed program should not resemble an attempt to test an instance of the Collatz Conjecture. In 2004, Podelski and Rybalchenko introduced Transition Invariants, a proof rule based on the transition relation of a given program. It provides a sufficient and useful condition for proving that a given program terminates, and its mathematical justification relies on the infinite form of Ramsey’s theorem.
In his short life, Frank Ramsey made tremendous contributions to logic, mathematics and other fields. The New Yorker has also published an account of his life.