Kanamori–McAloon theorem

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

A function ${\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 ${\displaystyle s}$ not containing 0.

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

For every ${\displaystyle n,k\in \mathbb {N} }$, there exists an ${\displaystyle 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)}$.

• Paris–Harrington theorem
• Goodstein's theorem
• Kruskal's tree theorem

• Kanamori, Akihiro; McAloon, Kenneth (1987), "On Gödel incompleteness and finite combinatorics", Annals of Pure and Applied Logic, 33 (1): 23–41, doi:10.1016/0168-0072(87)90074-1, ISSN 0168-0072, MR 0870685