Formalising Ramsey theory, II
[Isabelle Paul Erdős Ramsey's theorem ordinal partitions formalised mathematics Unlike the natural sciences, which are confined to what actually exists in the universe, mathematics is limited only by our imagination. Some branches, such as number theory, attract much attention, while other topics languish in the fringes. One fringe topic is Ramsey theory, and if anybody has heard of it, it’s probably because it captured the attention of one of mathematics’ few celebrities: Paul Erdős. A previous post introduced Ramsey’s theorem itself. It’s reasonably well known and has significant applications. Things get more obscure when we move into the transfinite. In the sequel, you need to be familiar with ordinals, including ordinal arithmetic and order types.
A brief introduction to ordinal partitions
As previously mentioned, the infinite version of Ramsey’s theorem states that if $n$ is a positive integer and we partition the $n$-element subsets of a given infinite set $X$ into two parts, then there is an infinite subset $Y\subseteq X$ such that every $n$-subset of $Y$ is in the same part. Often $n=2$, when we can use the more intuitive terminology of graphs. If the edges of the complete graph on $X$—an infinite set of vertices—are coloured black or white, then there is an infinite subset $Y\subseteq X$ such that all edges between elements of $Y$ have the same colour: are monochromatic.
The partition notation of Erdős and Rado, written $\alpha\longrightarrow (\beta_0, \ldots,\beta_{k-1})$, means that for every partition of the set $[\alpha]^2$ (the ediges of the complete graph on $\alpha$) into $k$ colours $C_0$, $\ldots$, $C_{k-1}$, there exists $i<k$ and a subset $B\subseteq\alpha$ of order type $\beta_i$ such that $[B]^2\subseteq C_i$. In particular, the infinite version of Ramsey’s theorem can be expressed by $\omega\longrightarrow (\omega ,\omega)$. The negation of $\alpha\longrightarrow (\beta, \gamma)$ is written $\alpha \not\mkern-3mu\longrightarrow (\beta, \gamma)$.
One key result is negative: for any ordinal $\alpha$ we have $\alpha\not\mkern-3mu\longrightarrow (|\alpha|+1, \omega)$. The proof involves an elementary construction that we’ll formalise below.
In 1987, Erdős offered a thousand-dollar prize to anyone who could characterise the set of all countable ordinals $\alpha$ such that $\alpha\longrightarrow(\alpha,3)$. Progress has been slow. My colleagues and I have formalised the proof important result, $\omega^\omega\longrightarrow(\omega^\omega, m)$. Unfortunately, such proofs tend to be gruesomely technical and all I can offer today is the elementary negative result mentioned above.
Ordinal partitions in Isabelle/HOL
Our formalisation relies on the Isabelle/HOL library for ZFC set theory.
We use ordinary HOL sets to represent relations and HOL sets, while the list of order types is a V list, combining ZF set theory with HOL lists.
Although we could encode lists directly as ZF sets, such combinations of the set theory and Isabelle/HOL libraries are the easiest way to accomplish what we want.
We begin by defining the Erdős–Rado partition notation. In its most general form, it accepts as an argument the relation to be used in the determination of order types. In many cases however, we’ll specialise it to the standard ordering on set-theoretic ordinals (which is simply the membership relation);
we’ll then write the order type of H as tp H.
definition partn_lst :: "[('a × 'a) set, 'a set, V list, nat] ⇒ bool" where "partn_lst r B α n ≡ ∀f ∈ [B]⇗n⇖ → {..<length α}. ∃i < length α. ∃H. H ⊆ B ∧ ordertype H r = (α!i) ∧ f ` (nsets H n) ⊆ {i}"
This definition uses a lot of Isabelle/HOL syntax. Essentially it says that for every $f$ mapping $n$-element subsets of $B$ to natural numbers less than length$(\alpha)$, there exists some $i$ and $H$ where $H$ has order type $\alpha_i$. The final inclusion, using the image operator, states that $f$ maps all $n$-element subsets of $H$ to $i$.
Here’s a small example: proving the infinite version of Ramsey’s theorem as $\omega\longrightarrow (\omega ,\omega)$, given a different formulation of that theorem. So all that’s happening in the proof below is the unpacking of the Erdős–Rado partition notation (in the ordinal version just mentioned) followed by an application of Ramsey’s theorem and delivering the result in the required form.
lemma Ramsey_partn: "partn_lst_VWF ω [ω,ω] 2" proof (clarsimp simp: partn_lst_def) fix f assume "f ∈ [elts ω]⇗2⇖ → {..<Suc (Suc 0)}" then have *: "∀x∈elts ω. ∀y∈elts ω. x ≠ y ⟶ f {x, y} < 2" by (auto simp: nsets_def eval_nat_numeral) obtain H i where H: "H ⊆ elts ω" and "infinite H" and t: "i < Suc (Suc 0)" and teq: "∀x∈H. ∀y∈H. x ≠ y ⟶ f {x, y} = i" using Ramsey2 [OF infinite_ω *] by (auto simp: eval_nat_numeral) then have "tp H = [ω, ω] ! i" using less_2_cases eval_nat_numeral ordertype_infinite_ω by force moreover have "f ` {N. N ⊆ H ∧ finite N ∧ card N = 2} ⊆ {i}" by (force simp: teq card_2_iff) ultimately have "f ` [H]⇗2⇖ ⊆ {i}" by (metis (no_types) nsets_def numeral_2_eq_2) then show "∃i<Suc (Suc 0). ∃H⊆elts ω. tp H = [ω,ω] ! i ∧ f ` [H]⇗2⇖ ⊆ {i}" using H ‹tp H = [ω, ω] ! i› t by blast qed
The form of the supplied version of Ramsey’s theorem (Ramsey2, since it’s for the $n=2$ case) should be evident from the obtain line.
A negative result
To prove $\alpha\not\mkern-3mu\longrightarrow (|\alpha|+1, \omega)$ for any ordinal $\alpha$, we construct a counterexample to the Ramsey property. The proof is simple enough to present in full. We begin by stating the claim.
proposition omega_basic_counterexample: assumes "Ord α" shows "¬ partn_lst_VWF α [succ (vcard α), ω] 2" proof -
The first step of the construction is to obtain an injective map $\pi: \alpha\to |\alpha|$, which exists because there is a bijection between any set and its cardinality. Since all cardinals are ordinals and all ordinals are sets, $\pi$ is simply a map from sets to sets.
obtain π where funπ: "π ∈ elts α → elts (vcard α)" and injπ: "inj_on π (elts α)" using inj_into_vcard by auto have Ordπ: "Ord (π x)" if "x ∈ elts α" for x using Ord_in_Ord funπ that by fastforce
The counterexample will be a colouring of the edges between elements of $\alpha$ such that there exists no monochromatic subset of $\alpha$ of order type $|\alpha|+1$ or $\omega$, respectively. We define $f$ on pairs of ordinals such that
\[f \{x,y\} = \begin{cases}0 & \text{if } x<y \land \pi(x)<\pi(y)\\ 1 & \text{if } x<y \land \pi(x)>\pi(y) \end{cases}\]The one-line definition is followed by a proof that $f$ belongs to the right “type” (function space), mapping 2-element subsets of $\alpha$ to the set $\{0,1\}$.
define f where "f A ≡ @i::nat. ∃x y. A = {x,y} ∧ x < y ∧ (π x < π y ∧ i=0 ∨ π y < π x ∧ i=1)" for A have f_Pi: "f ∈ [elts α]⇗2⇖ → {..<Suc (Suc 0)}" proof fix A assume "A ∈ [elts α]⇗2⇖" then obtain x y where xy: "x ∈ elts α" "y ∈ elts α" "x < y" and A: "A = {x,y}" apply (clarsimp simp: nsets_2_eq) by (metis Ord_in_Ord Ord_linear_lt assms insert_commute) consider "π x < π y" | "π y < π x" by (metis Ordπ Ord_linear_lt injπ inj_onD less_imp_not_eq2 xy) then show "f A ∈ {..<Suc (Suc 0)}" by (metis A One_nat_def lessI lessThan_iff zero_less_Suc ‹x < y› A exE_some [OF _ f_def]) qed
Next comes a proof that there exists no 0-monochromatic subset $H\subseteq\alpha$ having order type $|\alpha|+1$. Those assumptions lead to the contradiction $|\alpha|+1 \le |\alpha|$. The calculation starts halfway down, starting with ”tp H = tp (π ` H)”.
have False if eq: "tp H = succ (vcard α)" and H: "H ⊆ elts α" and 0: "⋀A. A ∈ [H]⇗2⇖ ⟹ f A = 0" for H proof - have [simp]: "small H" using H down by auto have OH: "Ord x" if "x ∈ H" for x using H Ord_in_Ord ‹Ord α› that by blast have π: "π x < π y" if "x∈H" "y∈H" "x<y" for x y using 0 [of "{x,y}"] that H fiff by (fastforce simp: nsets_2_eq) have sub_vcard: "π ` H ⊆ elts (vcard α)" using H funπ by auto have "tp H = tp (π ` H)" proof (rule ordertype_VWF_inc_eq [symmetric]) show "π ` H ⊆ ON" using H Ordπ by blast qed (auto simp: π OH subsetI) also have "… ≤ vcard α" by (simp add: H sub_vcard assms ordertype_le_Ord) finally show False by (simp add: eq succ_le_iff) qed
And next comes a proof that there exists no 1-monochromatic subset $H\subseteq\alpha$ having order type $\omega$. Those assumptions lead to an infinitely descending chain of ordinals.
moreover have False if eq: "tp H = ω" and H: "H ⊆ elts α" and 1: "⋀A. A ∈ [H]⇗2⇖ ⟹ f A = Suc 0" for H proof - have [simp]: "small H" using H down by auto define η where "η ≡ inv_into H (ordermap H VWF) ∘ ord_of_nat" have bij: "bij_betw (ordermap H VWF) H (elts ω)" by (metis ordermap_bij ‹small H› eq total_on_VWF wf_VWF) then have "bij_betw (inv_into H (ordermap H VWF)) (elts ω) H" by (simp add: bij_betw_inv_into) then have η: "bij_betw η UNIV H" unfolding η_def by (metis ω_def bij_betw_comp_iff2 bij_betw_def elts_of_set inf inj_ord_of_nat order_refl) moreover have Ordη: "Ord (η k)" for k by (meson H Ord_in_Ord UNIV_I η assms bij_betw_apply subsetD) moreover obtain k where k: "(π (η(Suc k)), π (η k)) ∉ VWF" by (meson wf_VWF wf_iff_no_infinite_down_chain) moreover have π: "π y < π x" if "x∈H" "y∈H" "x<y" for x y using 1 [of "{x,y}"] that H fiff by (fastforce simp: nsets_2_eq) ultimately have "η (Suc k) ≤ η k" by (metis H Ordπ Ord_linear2 VWF_iff_Ord_less bij_betw_def rangeI subset_iff) then have "(η (Suc k), η k) ∈ VWF ∨ η (Suc k) = η k" using Ordη Ord_mem_iff_lt by auto then have "ordermap H VWF (η (Suc k)) ≤ ordermap H VWF (η k)" by (metis η ‹small H› bij_betw_imp_surj_on ordermap_mono_le rangeI trans_VWF wf_VWF) moreover have "ordermap H VWF (η (Suc k)) = succ (ord_of_nat k)" unfolding η_def using bij bij_betw_inv_into_right by force moreover have "ordermap H VWF (η k) = ord_of_nat k" using η_def bij bij_betw_inv_into_right by force ultimately show False by (simp add: less_eq_V_def) qed
The two results above, combined using moreover and delivered using ultimately, yield the desired claim.
ultimately show ?thesis apply (simp add: partn_lst_def image_subset_iff) by (metis f_Pi less_2_cases nth_Cons_0 nth_Cons_Suc numeral_2_eq_2) qed
I wish such proofs were easier. You can find much more of this online in the AFP. If anyone wants to see more on this topic here, please let me know.