The Paris-Harrington theorem is a strengthening of the finite Ramsey's theorem by requiring that the homogeneous set be large enough so that . Clearly, the statement can be expressed in the
first-order language of arithmetic. It is easily provable in the second-order arithmetic,
but is unprovable in first-order Peano arithmetic
(Paris and Harrington 1977; Borwein and Bailey 2003, p. 34).
The original unprovability proof by Paris and Harrington used a model-theoretic argument. In any model , the Paris-Harrington principle in its nonstandard instances
allows construction of an initial segment which is a model of Peano
arithmetic. It also follows that the function
such that for any colouring of
-tuples of
into
colors there is a subset
of
of size
which is relatively large and such that
eventually dominates every function provably recursive
in Peano arithmetic.
Later, another approach to proving unprovability of the theorem using ordinals was introduced by J. Ketonen and R. Solovay.