Can this combinatorics proof be finished using the Compactness Theorem in Logic?

Question

In Alon and Spencer's book The Probabilistic Method, they prove the following theorem:

---

Theorem: Let $m$ and $k$ be two positive integers satisfying $$e(m(m-1)+1)k\left(1-\frac{1}{k}\right)^m \leq 1$$ Then, for any set $S$ of $m$ real numbers there is a $k$-colouring of $\mathbb{R}$ so that each translation $x+S$ (for $x \in\mathbb{R}$) is multicoloured (i.e. contains at least one real of each colour).

---

Their proof proceeds by proving the statement holds for every finite set of translations $X$ (i.e. there is a $k$-colouring so that each translation $x+S$ is multicoloured when $x \in X$) and then they apply an argument which they refer to as "a standard compactness argument", invoking Tychonoff's Theorem to prove the compactness of the space of all functions from $\mathbb{R}$ to $\{1,2,...,k\}$ etc.

I'm slightly less familiar with analysis than you might hope (/expect?) when reading this book and while I understand their argument formally, it definitely doesn't come across as "standard". I therefore wonder whether it is possible to finish the proof instead using the Compactness Theorem in first-order logic (a piece of machinery I'm a little more comfortable with!).

It seems to me that we could formalise the notion of a k-colouring of a set of real numbers in first-order logic and then similarly formalise every sentence of the form "$x+S$ is multicoloured" (for each individual $x \in\mathbb{R}$). We then know from their earlier argumentation that for every finite subset of these sentences, there is a colouring (i.e. a model for these sentences) and therefore there is a model for all the sentences and the theorem is proven.

Question: Is the above reasoning correct? Are there any barriers I have missed to formalising this in first-order logic and using the Compactness Theorem?

Answer 1

Your sketch is essentially correct. Fix a natural number $k$ and a finite set $S \subseteq \mathbb{R}$ so that

$$ e(|S|(|S|-1)+1)k\left(1-\frac{1}{k}\right)^{|S|}\leq 1$$ holds.

Consider the language $\mathcal{L}$ which has

1. a constant symbol $c_r$ for each real number $r \in \mathbb{R}$,
2. a binary function symbol $\oplus$, and
3. a unary function symbol $f$.

Define $K(x)$ to abbreviate $\displaystyle \bigvee_{i \in \{1,\dots,k\}} x = c_i$, and $S(x)$ to abbreviate $\displaystyle \bigvee_{i \in S} x = c_i$.

Now take the theory $T$ over $\mathcal{L}$ consisting of the following axioms:

1. the axiom $c_x \oplus c_y = c_z$ for each element of the set $\{(x,y,z) \in \mathbb{R}^3 \:|\: x+y=z \}$,
2. the axiom $\forall x. K(f(x))$,
3. for each real number constant $c_x$, the axiom $\forall t. K(t) \rightarrow \exists s. S(s) \wedge f(c_x \oplus s) = t$.

The second axiom states that $f$ is a $k$-coloring, and the third axiom schema ensures that each translation $x+S$ has at least one real of each color. So if a coloring with the desired property exists, then $T$ has a model. Vice versa, if the theory $T$ has a model $(M, \oplus, f)$, then $\mathbb{R} \subseteq M$ and $+ \subseteq \oplus$ and one can verify (exercise!) that $(\mathbb{R},+, f_{|\mathbb{R}})$ is also a model of $T$. So the theory $T$ has a model precisely if a desired coloring of the reals exists.

Consider an arbitrary finite fragment $T'$ of $T$. Such a fragment contains only finitely many instances of the third axiom schema. Consider the finite set $X=\{x \in \mathbb{R} \:|\: c_x\text{ occurs in an instance of the third schema in }T'\}$. By the result of Alon and Spencer, one can find a $k$-coloring $f'$ so that each translation $x+S$ is multicolored when $x \in X$, so $T'$ has the model $(\mathbb{R}, + ,f')$. Since every finite fragment $T'$ of $T$ has a model, the compactness theorem yields that $T$ itself has a model. It follows that a desired coloring of the reals exists.

Remark: Regarding minimalistic interest: indeed, the fact that "the product of an indexed family of finite topological spaces is compact" is already equivalent to the ultrafilter lemma (and hence to compactness) over ZF Set Theory. There's a proof in Levy's Basic Set Theory (Theorem 2.21 in the 2002 edition). Not entirely coincidentally, Nelson's Internal Set Theory (the Choice-free fragment) provides a convenient setting for results proved using compactness arguments like these (and much more complicated variants too), allowing one to sidestep having to define ad-hoc theories, or proving ad-hoc product spaces compact.