Solution (source code)

= Solution

The <partition relation> $\lambda\to(\mu)^r_\nu$ says that every <colouring> of the $r$-element <subsets> of a <set> of <cardinality> $\lambda$ into $\nu$ colours has a <homogeneous set> of <cardinality> $\mu$. Define the <beth numbers> over an infinite <cardinal> $\kappa$ by $\beth_0(\kappa)=\kappa$ and $\beth_{n+1}(\kappa)=2^{\beth_n(\kappa)}$. The <Erdős-Rado theorem for finite arities> gives the precise bound
$$
\boxed{\beth_n(\kappa)^+\longrightarrow(\kappa^+)^{n+1}_\kappa\qquad(n<\omega).}
$$
Thus any fixed finite arity and any fixed infinite number of colours admit arbitrarily large infinite <monochromatic sets> once the starting <cardinal> is sufficiently large. For pairs, the especially useful case is $(2^\kappa)^+\to(\kappa^+)^2_\kappa$. The successor in this bound matters: a binary first-difference colouring on a suitably ordered <set> of binary <sequences> supplies the familiar obstruction at $2^\kappa$. Also, a theorem for every fixed finite arity is not a theorem homogenizing all arities simultaneously.

The mechanism is to build an <end-homogeneous routing tree>: each new vertex is routed according to its colours to earlier vertices on its branch. A long branch is end-homogeneous, meaning the colour from a fixed earlier vertex is independent of the later vertex. There are at most $\kappa^\alpha\leq2^\kappa$ routes of length $\alpha<\kappa^+$, and the whole collection of short routes has size at most $2^\kappa$. Inserting $(2^\kappa)^+$ vertices therefore forces a branch of length $\kappa^+$. One colour occurs at $\kappa^+$ earlier vertices on that branch, giving the pair theorem. Iterating the higher-arity version of this routing construction explains the successive powers in the <Erdős-Rado theorem for finite arities>.

A <weakly compact cardinal> is an uncountable <strongly inaccessible cardinal> $\kappa$ with
$$
\kappa\longrightarrow(\kappa)^2_2.
$$
Equivalent formulations include the <tree property> at the inaccessible <cardinal> and compactness for theories of size at most $\kappa$ in the infinitary language $L_{\kappa,\kappa}$: if every subtheory of size $<\kappa$ has a <first-order model>, so does the theory.

A <measurable cardinal> is an uncountable $\kappa$ carrying a <nonprincipal ultrafilter> <closed> under intersections of fewer than $\kappa$ members. Such an <ultrafilter> contains no <set> of size $<\kappa$, since all singletons have complements in it and it is <kappa-complete>. Consequently a cofinal <sequence> of length $<\kappa$ would partition $\kappa$ into too few small pieces, so $\kappa$ is <regular cardinal>. If $\lambda<\kappa$ and $\kappa$ distinct <subsets> of $\lambda$ existed, choose, for each coordinate of $\lambda$, the bit selected by the <ultrafilter>. <Kappa-completeness> would make all those bits simultaneously constant on a large <set> of indices; only one distinct <subset> could have that bit pattern, a contradiction. Hence $2^\lambda<\kappa$: $\kappa$ is also a <strong limit cardinal>.

A <supercompact cardinal> $\kappa$ has, for every $\lambda\geq\kappa$, a <fine ultrafilter> that is a <normal ultrafilter on small subsets> and is <kappa-complete> on
$$
P_\kappa(\lambda)=\{x\subseteq\lambda:|x|<\kappa\}.
$$
Fine means $\{x:\alpha\in x\}$ is large for every $\alpha<\lambda$. Normal means that a <function> $f$ with $f(x)\in x$ on a large <set> is constant on some large <set>. Equivalently, for every such $\lambda$ there is an <elementary embedding> $j:V\to M$ with <critical point> $\kappa$, $j(\kappa)>\lambda$, and $M$ <closed> under $\lambda$-sequences from the universe.

These notions form the implication chain \b[supercompact $\Rightarrow$ measurable $\Rightarrow$ weakly compact]. For the first implication, an embedding as above gives the measure $U=\{X\subseteq\kappa:\kappa\in j(X)\}$. For the second, use a <normal ultrafilter on a cardinal> obtained by normalizing its measure. Indeed the <ultrapower embedding> gives the measure $U=\{X\subseteq\kappa:\kappa\in j(X)\}$; for a regressive $f$, $j(f)(\kappa)<\kappa$ is a fixed <ordinal>, yielding the required constant large fibre. Given a pair-colouring, select for each $\alpha$ the measure-one colour on the tail above $\alpha$. One selected colour occurs on a measure-one <set> of $\alpha$'s. Normality makes the diagonal intersection of their selected tails measure one; any two members of that intersection have the selected colour. This gives the required <partition relation>, and the preceding regularity and strong-limit argument gives inaccessibility.