Wetzel's problem and the continuum hypothesis
[ZFC_in_HOL Paul Erdős set theory Proofs from THE BOOK David Hilbert formalised mathematics The continuum hypothesis (CH) dates from the 19th century and became the first of David Hilbert’s famous unsolved problems. Gödel proved it to be consistent with the axioms of set theory (ZFC), while Cohen exhibited models of ZFC in which CH failed. New axioms would be needed to settle the question. Despite decades of intensive research, the status of CH remains open. However recondite it may be, CH cannot be ignored: ordinary-looking mathematical questions occasionally bump into it.
What is the continuum hypothesis anyway?
CH can be expressed by the mysterious formula $2^{\aleph_0}=\aleph_1$, and yet it is a simple question. A set is countable if its elements can be written in a series. (So finite sets are also countable.) The concept of countability was readily accepted by 19th century mathematicians, who by assuming facts such as “a countable union of countable sets is countable” found themselves depending on the axiom of choice (AC) before it had even been promulgated.
Cantor had proved that the algebraic numbers were countable and that the real numbers were not. He proved that the finite interval $[0,1]$ could be put into bijection with any $\mathbb{R}^n$, and called this “cardinality of the continuum” $\frak{c}$. He then asked whether some intermediate set $X$ of real numbers existed, itself uncountable but of smaller cardinality than $\mathbb{R}$. And that simply depended on the existence (or not) of a bijection between $X$ and $\mathbb{R}$: it need not involve the cardinal numbers or AC.
The story of Wetzel’s problem
I first learned of Wetzel’s problem from Proofs from THE BOOK by Aigner and Ziegler, a compendium of beautiful proofs, many somehow connected with the legendary Hungarian mathematician, Paul Erdős. It involves some complex analysis, fortunately only a tiny bit, because that’s all I know myself. Wetzel asked
If $\{f_\alpha\}$ is a family of distinct analytic functions (on some fixed domain) such that for each $z$ the set of values $\{f_\alpha(z)\}$ is countable, is the family itself countable?
Erdős stumbled upon this question in a problem book and in 1964 published a solution: Wetzel’s question is equivalent to the negation of CH. It is therefore independent of the generally accepted axioms of set theory!
Erdős first assumes ¬CH. He then shows that for any family of analytic functions $\{f_\alpha\}$ of size $\aleph_1$ there exists a complex number $z$ such that all $\aleph_1$ values $\{f_\alpha(z)\}$ are distinct and therefore this set is uncountable. If on the other hand CH holds, Erdős shows how, by transfinite induction, one can construct a family $\{f_\alpha\}$ of cardinality $\aleph_1$ such that $\{f_\alpha(z)\}$ is countable for all $z$.
Garcia and Shoemaker have written a brief history of the problem and its origins.
Wetzel’s problem in Isabelle/HOL
Let’s begin by defining the predicate Wetzel on sets of complex-valued functions. It holds if every element of the given set $F$ is analytic on the complex plane and if every set of the form $\{f(z) \mid f\in F\}$ (for any $z$) is countable.
definition Wetzel :: "(complex ⇒ complex) set ⇒ bool" where "Wetzel ≡ λF. (∀f∈F. f analytic_on UNIV) ∧ (∀z. countable((λf. f z) ` F))"
Because the proof refers to ordinals, cardinals and transfinite induction, it’s natural to base it on the theory of ZFC_in_HOL, which was described in a previous post. The easier case is when ¬CH, i.e., when $\aleph_0 < \aleph_1 < 2^{\aleph_0}=\frak{c}$. The formal proof is compact enough to insert in full, and it’s legible enough to reveal the main proof ideas. It begins with a lemma to exhibit some $z_0$ such that the cardinality of $\{f(z_0) \mid f\in F\}$ is at least $\aleph_1$, under the assumption that $F$ is uncountable. Skipping down to the very bottom of the proof, we see that the result quickly follows from this lemma and the Wetzel assumption.
Now for the proof of the lemma. We are given that $F$ is uncountable, which guarantees the existence of some $F’ \subseteq F$ having cardinality $\aleph_1$, from which we obtain a bijection $\phi$ between the ordinals below $\aleph_1$ and $F’$.
Now for ordinals $\alpha$, $\beta < \omega_1$ we define $S\alpha\beta = \{z. \phi\alpha z = \phi\beta z\}$. (Note: $\omega_1$ is nothing but $\aleph_1$, regarded as an ordinal.)
Lemma co_S tells us that $S\alpha\beta$ is countable if $\alpha<\beta$. Its proof relies on the fact holomorphic_countable_equal_UNIV: since $\phi\alpha$ and $\phi\beta$ must be different functions, and they are holomorphic, they can agree on only countably many points. (And that’s the sum total of the complex analysis required here.)
Next, we define $SS = \bigcup_{\alpha<\beta<\aleph_1}\, S\alpha\beta$.
It takes a dozen lines of calculations to show $|SS|\leq \aleph_1$.
By ¬CH we have $\aleph_1 < \frak{c}$ and trivially obtain some complex number $z_0\not\in SS$.
By the definition of $SS$, since $\phi\alpha z_0 \not= \phi\beta z_0$ for all $\alpha<\beta<\omega_1$,
we find that $|\{f(z_0) \mid f\in F’\}| = \aleph_1$, from which the lemma follows.
proposition Erdos_Wetzel_nonCH: assumes W: "Wetzel F" and NCH: "C_continuum > ℵ1" and "small F" shows "countable F" proof - have "∃z0. gcard ((λf. f z0) ` F) ≥ ℵ1" if "uncountable F" proof - have "gcard F ≥ ℵ1" using ‹small F› that uncountable_gcard_ge by blast then obtain F' where "F' ⊆ F" and F': "gcard F' = ℵ1" by (meson Card_Aleph Ord_1 subset_smaller_gcard ‹small F›) then obtain φ where φ: "bij_betw φ (elts ω1) F'" by (metis TC_small eqpoll_def gcard_eqpoll) define S where "S ≡ λα β. {z. φ α z = φ β z}" have co_S: "gcard (S α β) ≤ ℵ0" if "α ∈ elts β" "β ∈ elts ω1" for α β proof - have "φ α holomorphic_on UNIV" "φ β holomorphic_on UNIV" using W ‹F' ⊆ F› unfolding Wetzel_def by (meson Ord_ω1 Ord_trans φ analytic_imp_holomorphic bij_betwE subsetD that)+ moreover have "φ α ≠ φ β" by (metis Ord_ω1 Ord_in_Ord Ord_trans OrdmemD φ bij_betw_imp_inj_on inj_on_def less_V_def that) ultimately have "countable (S α β)" using holomorphic_countable_equal_UNIV unfolding S_def by blast then show ?thesis using countable_imp_g_le_Aleph0 by blast qed define SS where "SS ≡ ⨆((λβ. ⨆((λα. S α β) ` elts β)) ` elts(ℵ1))" have F'_eq: "F' = φ ` elts ω1" using φ bij_betw_imp_surj_on by auto have §: "⋀β. β ∈ elts ω1 ⟹ gcard (⋃α∈elts β. S α β) ≤ ω" by (metis Aleph_0 TC_small co_S countable_UN countable_iff_g_le_Aleph0 less_ω1_imp_countable) have "gcard SS ≤ gcard ((λβ. ⋃α∈elts β. S α β) ` elts ω1) ⊗ ℵ0" apply (simp add: SS_def) by (metis (no_types, lifting) "§" TC_small gcard_Union_le_cmult imageE) also have "… ≤ ℵ1" proof (rule cmult_InfCard_le) show "gcard ((λβ. ⋃α∈elts β. S α β) ` elts ω1) ≤ ω1" using gcard_image_le by fastforce qed auto finally have "gcard SS ≤ ℵ1" . with NCH obtain z0 where "z0 ∉ SS" by (metis Complex_gcard UNIV_eq_I less_le_not_le) then have "inj_on (λx. φ x z0) (elts ω1)" apply (simp add: SS_def S_def inj_on_def) by (metis Ord_ω1 Ord_in_Ord Ord_linear) then have "gcard ((λf. f z0) ` F') = ℵ1" by (smt (verit) F' F'_eq gcard_image imageE inj_on_def) then show ?thesis by (metis TC_small ‹F' ⊆ F› image_mono subset_imp_gcard_le) qed with W show ?thesis unfolding Wetzel_def by (meson countable uncountable_gcard_ge) qed
Wetzel’s problem, assuming the continuum hypothesis
The case when the continuum hypothesis holds is much more difficult, even setting aside the hardest part of the proof. We must construct an uncountable family of analytic functions that makes the Wetzel property fail.
proposition Erdos_Wetzel_CH: assumes CH: "C_continuum = ℵ1" obtains F where "Wetzel F" and "uncountable F"
Consider the set $D\subseteq\mathbb{C}$ of “rational” complex numbers, i.e. \(\begin{align*} D = \{p+iq\mid p,q\in\mathbb{Q}\}. \end{align*}\) By CH we can write $\mathbb{C} = \{z_\alpha : \alpha < \omega_1 \}$ and it will suffice to construct $\{f_\beta : \beta < \omega_1 \}$ such that \(\begin{align*} f_\beta (z_\alpha) \in D \end{align*}\) if $\alpha<\beta$. Since the set $D$ is countable and the $z_\alpha$ for $\alpha < \omega_1$ include all complex numbers, the desired result follows.
The formal proof begins with a self-evident definition of $D$. It’s easily shown to be countable, and with somewhat unexpected difficulty, infinite. That $D$ is dense in $\mathbb{C}$ requires an explicit proof that any complex $z$ can be approximated arbitrarily closely by some element $w$ of $D$. Note that “closure D = UNIV” expresses that the closure of $D$ equals the universal set of complex numbers, i.e. the entire complex plane.
proof - define D where "D ≡ {z. Re z ∈ ℚ ∧ Im z ∈ ℚ}" have Deq: "D = (⋃x∈ℚ. ⋃y∈ℚ. {Complex x y})" using complex.collapse by (force simp: D_def) with countable_rat have "countable D" by blast have "infinite D" unfolding Deq by (intro infinite_disjoint_family_imp_infinite_UNION Rats_infinite) (auto simp: disjoint_family_on_def) have "∃w. Re w ∈ ℚ ∧ Im w ∈ ℚ ∧ norm (w - z) < e" if "e > 0" for z and e::real proof - obtain x y where "x∈ℚ" "y∈ℚ" and xy: "dist (x,y) (Re z, Im z) < e" using ‹e > 0› Rats_closure_real2 by (force simp: closure_approachable) moreover have "dist (x,y) (Re z, Im z) = norm (Complex x y - z)" by (simp add: norm_complex_def norm_prod_def dist_norm) ultimately show "∃w. Re w ∈ ℚ ∧ Im w ∈ ℚ ∧ norm (w - z) < e" by (metis complex.sel) qed then have cloD: "closure D = UNIV" by (auto simp: D_def closure_approachable dist_complex_def)
In the formal proof, the transfinite enumeration $\{\zeta_\alpha : \alpha < \omega_1 \}$ of the complex plane is called $\zeta$. Next come some technical definitions: inD for functions whose range for certain arguments lies within $D$ and $\Phi$ for further constraints on the family f of analytic functions being defined transfinitely.
obtain ζ where ζ: "bij_betw ζ (elts ω1) (UNIV::complex set)" by (metis Complex_gcard TC_small assms eqpoll_def gcard_eqpoll) define inD where "inD ≡ λβ f. (∀α ∈ elts β. f (ζ α) ∈ D)" define Φ where "Φ ≡ λβ f. f β analytic_on UNIV ∧ inD β (f β) ∧ inj_on f (elts (succ β))"
The lemma called * will be the induction step, claiming the existence of the next member of the family, h, given that f is already defined below the ordinal $\gamma$.
This ordinal is countable, but could be either finite or infinite. The finite case is easier, since the function we have to construct will simply be a polynomial, and trivially analytic. That is the case shown below, including induction on the finite ordinal $\gamma$. The infinite case requires serious trickery, so it has been elided. I hope one day to write a paper to explain the full details.
have *: "∃h. Φ γ ((restrict f (elts γ))(γ:=h))" if γ: "γ ∈ elts ω1" and "∀β ∈ elts γ. Φ β f" for γ f proof - have f: "∀β ∈ elts γ. f β analytic_on UNIV ∧ inD β (f β)" using that by (auto simp: Φ_def) have inj: "inj_on f (elts γ)" using that by (simp add: Φ_def inj_on_def) (meson Ord_ω1 Ord_in_Ord Ord_linear) obtain h where "h analytic_on UNIV" "inD γ h" "(∀β ∈ elts γ. h ≠ f β)" proof (cases "finite (elts γ)") case True then obtain η where η: "bij_betw η {..<card (elts γ)} (elts γ)" using bij_betw_from_nat_into_finite by blast define g where "g ≡ f o η" define w where "w ≡ ζ o η" have gf: "∀i<card (elts γ). h ≠ g i ⟹ ∀β∈elts γ. h ≠ f β" for h using η by (auto simp: bij_betw_iff_bijections g_def) have **: "∃h. h analytic_on UNIV ∧ (∀i<n. h (w i) ∈ D ∧ h (w i) ≠ g i (w i))" if "n ≤ card (elts γ)" for n using that proof (induction n) case 0 then show ?case using analytic_on_const by blast next case (Suc n) then obtain h where "h analytic_on UNIV" and hg: "∀i<n. h (w i) ∈ D ∧ h (w i) ≠ g i (w i)" using Suc_leD by blast define p where "p ≡ λz. ∏i<n. z - w i" have p0: "p z = 0 ⟷ (∃i<n. z = w i)" for z unfolding p_def by force obtain d where d: "d ∈ D - {g n (w n)}" using ‹infinite D› by (metis ex_in_conv finite.emptyI infinite_remove) define h' where "h' ≡ λz. h z + p z * (d - h (w n)) / p (w n)" have h'_eq: "h' (w i) = h (w i)" if "i<n" for i using that by (force simp: h'_def p0) show ?case proof (intro exI strip conjI) have nless: "n < card (elts γ)" using Suc.prems Suc_le_eq by blast with η have "η n ≠ η i" if "i<n" for i using that unfolding bij_betw_iff_bijections by (metis lessThan_iff less_not_refl order_less_trans) with ζ η γ have pwn_nonzero: "p (w n) ≠ 0" apply (clarsimp simp: p0 w_def bij_betw_iff_bijections) by (metis Ord_ω1 Ord_trans nless lessThan_iff order_less_trans) then show "h' analytic_on UNIV" unfolding h'_def p_def by (intro analytic_intros ‹h analytic_on UNIV›) fix i assume "i < Suc n" then have §: "i < n ∨ i = n" by linarith then show "h' (w i) ∈ D" using h'_eq hg d h'_def pwn_nonzero by force show "h' (w i) ≠ g i (w i)" using § h'_eq hg h'_def d pwn_nonzero by fastforce qed qed show ?thesis using ** [OF order_refl] η that gf by (simp add: w_def bij_betw_iff_bijections inD_def) metis next case False show ?thesis ... qed qed with f show ?thesis using inj by (rule_tac x="h" in exI) (auto simp: Φ_def inj_on_def) qed
The next part of the proof is pure annoyance. We have just shown the main argument of the transfinite construction, yet the following chunk of text seems to be necessary in order to define the family of functions f and to perform the transfinite induction itself (the relevant induction rule is called eps_induct, for $\epsilon$-induction).
Having done this, we obtain the crucial properties of f: the functions are analytic and satisfy $f_\beta (z_\alpha) \in D$ if $\alpha<\beta$; moreover, the enumeration f is injective and therefore repetition-free.
define G where "G ≡ λf γ. @h. Φ γ ((restrict f (elts γ))(γ:=h))" have nxt: "Φ γ ((restrict f (elts γ))(γ:= G f γ))" if "γ ∈ elts ω1" "∀β ∈ elts γ. Φ β f" for f γ unfolding G_def using * [OF that] by (metis someI) have G_restr: "G (restrict f (elts γ)) γ = G f γ" if "γ ∈ elts ω1" for f γ by (auto simp: G_def) define f where "f ≡ transrec G" have Φf: "Φ β f" if "β ∈ elts ω1" for β using that proof (induction β rule: eps_induct) case (step γ) then have *: "∀β∈elts γ. Φ β f" using Ord_ω1 Ord_trans by blast have [simp]: "inj_on (λβ. G (restrict f (elts β)) β) (elts γ) ⟷ inj_on f (elts γ)" by (metis (no_types, lifting) f_def transrec inj_on_cong) have "f γ = G f γ" by (metis G_restr transrec f_def step.prems) with nxt [OF step.prems] * show ?case by (metis Φ_def elts_succ fun_upd_same fun_upd_triv inj_on_restrict_eq restrict_upd) qed then have anf: "⋀β. β ∈ elts ω1 ⟹ f β analytic_on UNIV" and inD: "⋀α β. ⟦β ∈ elts ω1; α ∈ elts β⟧ ⟹ f β (ζ α) ∈ D" using Φ_def inD_def by blast+ have injf: "inj_on f (elts ω1)" using Φf unfolding inj_on_def Φ_def by (metis Ord_ω1 Ord_in_Ord Ord_linear_le in_succ_iff)
All that remains is tidying up. We show that the family of functions just constructed returns a countable image for every complex number z, which involves finding the corresponding ordinal $\alpha < \omega_1$ using the properties proved for f. The Wetzel property and uncountability of the family follow straightforwardly.
show ?thesis proof let ?F = "f ` elts ω1" have "countable ((λf. f z) ` f ` elts ω1)" for z proof - obtain α where α: "ζ α = z" "α ∈ elts ω1" "Ord α" by (meson Ord_ω1 Ord_in_Ord UNIV_I ζ bij_betw_iff_bijections) let ?B = "elts ω1 - elts (succ α)" have eq: "elts ω1 = elts (succ α) ∪ ?B" using α by (metis Diff_partition Ord_ω1 OrdmemD less_eq_V_def succ_le_iff) have "(λf. f z) ` f ` ?B ⊆ D" using α inD by clarsimp (meson Ord_ω1 Ord_in_Ord Ord_linear) then have "countable ((λf. f z) ` f ` ?B)" by (meson ‹countable D› countable_subset) moreover have "countable ((λf. f z) ` f ` elts (succ α))" by (simp add: α less_ω1_imp_countable) ultimately show ?thesis using eq by (metis countable_Un_iff image_Un) qed then show "Wetzel ?F" unfolding Wetzel_def by (blast intro: anf) show "uncountable ?F" using Ord_ω1 countable_iff_less_ω1 countable_image_inj_eq injf by blast qed qed
And finally …
The conclusion simply expresses the two cases as a single formula:
theorem Erdos_Wetzel: "C_continuum = ℵ1 ⟷ (∃F. Wetzel F ∧ uncountable F)" by (metis C_continuum_ge Erdos_Wetzel_CH Erdos_Wetzel_nonCH TC_small less_V_def)
The full theory development is online. The project took under three weeks and the most difficult part concerned the material skipped above: the case where $\gamma$ is infinite, involving the careful construction of an infinite series satisfying all the criteria and showing it to be holomorphic (therefore analytic) using a theorem about uniform limits. Well done if you made it this far!
Postscript added 26-09-2022
I presented this work in beautiful Tbilisi at CICM 2022 (part of the Computational Logic Autumn Summit). The full paper, including details about the case where $\gamma$ is infinite, is online with the accompanying slides.