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.