Kanamori–McAloon theorem

In mathematical logic, the Kanamori–McAloon theorem, due to Kanamori & McAloon (1987), gives an example of an incompleteness in Peano arithmetic, similar to that of the Paris–Harrington theorem. They showed that a certain finitistic theorem in Ramsey theory is not provable in Peano arithmetic (PA).
Statement

Given a set \( {\displaystyle s\subseteq \mathbb {N} } \) of non-negative integers, \( {\displaystyle \min(s)} \) denote the minimum element of s s. Let \( {\displaystyle [X]^{n}} \) denote the set of all n-element subsets of X.

A function f\( {\displaystyle f:[X]^{n}\rightarrow \mathbb {N} } \) where \( {\displaystyle X\subseteq \mathbb {N} } \) is said to be regressive if \( {\displaystyle f(s)<\min(s)} \) for all s s not containing 0.

The Kanamori–McAloon theorem states that the following proposition, denoted by ( ∗ ) (*) in the original reference, is not provable in PA:

For every \( {\displaystyle n,k\in \mathbb {N} } \) , there exists an \( m\in \mathbb {N} \) such that for all regressive \( {\displaystyle f:[\{0,1,\ldots ,m-1\}]^{n}\rightarrow \mathbb {N} } \), there exists a set \( {\displaystyle H\in [\{0,1,\ldots ,m-1\}]^{k}} \) such that for all \( {\displaystyle s,t\in [H]^{n}} \) with \( {\displaystyle \min(s)=\min(t)} \), we have \( {\displaystyle f(s)=f(t)} \).