Finite Ramsey theorem via first-order compactness + infinite Ramsey theorem

Question

The relevant definitions regarding notation, and the statements of Ramsey's theorems, can be found at the beginning of this question. There, I asked, and later provided an answer (mostly correct, as far as I can tell) to the question of how to prove the finite Ramsey theorem ($\mathrm{FRT}$) from the infinite Ramsey theorem ($\mathrm{IRT}$) via propositional compactness.

When I can manage to do so, and as I am still a novice in the subject, I find it quite helpful trying to prove whatever result I know how to prove using propositional compactness via first-order compactness as well.

The idea is to use first-order compactness to show that if $\mathrm{FRT}$ fails for some $k_{0}\in\mathbb{N}^{+}$ then $\mathrm{IRT}$ also fails. Therefore, we need to define appropriate first-order language $L$ and set of $L$-sentences $S_{k_{0}}$ encoding $\neg\mathrm{IRT}$ for $k_{0}$. Then we will prove finite satisfiability of $S_{k_{0}}$ assuming $\neg\mathrm{FRT}$ for $k_{0}$ and apply first-orer compactness. This will yield an model in which $\mathrm{IRT}$ fails.

Here is is my attempt at defining $L$ and $S_{k_{0}}$ of $L$-sentences.

The language $L$ contains:

1. $p$-ary predicate symbols $C^{1}, C^{2},\ldots,C^{r}$ (intuitively $C^{i}x_{1}\ldots x_{p}$ means $c(\{x_{1},\ldots,x_{p}\})=i$ when true).
2. Equality $=$.

The set $S_{k_{0}}$ consists of the following $L$-sentences:

1. $\forall x_{1}\ldots\forall x_{p}\,(C^{i}x_{1}\ldots x_{p}\Leftrightarrow C^{i}x_{f(1)}\ldots x_{f(p)})$ for all $1\leq i\leq r$ and all permutations $f$ of $[p]$.
2. $\displaystyle\forall x_{1}\ldots\forall x_{p}\,\left(C^{i}x_{1}\ldots x_{p}\Rightarrow\left(\bigwedge_{1\leq u<v\leq p}\neg(x_{u}=x_{v})\right)\right)$ for all $1\leq i\leq r$.

1 and 2 mean that only the $p$-element subsets of our domain may be colored.

3. $\forall x_{1}\ldots\forall x_{p}\,\left(\displaystyle\left(\bigwedge_{1\leq u<v\leq p}\neg(x_{u}=x_{v})\right)\Rightarrow\bigvee_{1\leq i\leq r}C^{i}x_{1}\ldots x_{p}\right)$ (each $p$-element subset is assigned at least one color).
4. $\forall x_{1}\ldots\forall x_{p}\,\neg(C^{i}x_{1}\ldots x_{p}\wedge C^{j}x_{1}\ldots x_{p})$ for all $1\leq i<j\leq r$ (each $p$-element subset is assigned at most one color).
5. $\displaystyle\forall x_{1}\ldots\forall x_{k_{0}}\,\left(\left(\bigwedge_{1\leq u<v\leq k_{0}}\neg(x_{u}=x_{v})\right)\Rightarrow\left(\bigvee_{1\leq i_{1}<\cdots<i_{p}\leq k_{0}}\neg C^{i}x_{i_{1}}\ldots x_{i_{p}}\right)\right)$ for all $1\leq i\leq r$ (every $k_{0}$-element subset of our domain has at least one $p$-element subset which is not colored by $i$).

5 means that there is no homogeneous $k_{0}$-element subset for the $r$-coloring of the set of $p$-element subsets of our domain.

6. $\displaystyle\exists x_{1}\ldots\exists x_{n}\,\left(\bigwedge_{1\leq u<v\leq p}\neg(x_{u}=x_{v})\right)$ for all $n\in\mathbb{N}$ (Our domain has infinitely many elements).
7. The equality $=$ axioms.

Question: Did I define $L$ and $S_{k_{0}}$ correctly? I am having a bit of trouble showing the finite satisfiability of $S_{k_{0}}$

Answer 1

In order to remove the question from the unanswered list, I will provide a proof that $S_{k_{0}}$ is finitely satisfiable assuming $\neg\mathrm{FRT}$ for $k_{0}$.

Indeed, let $\Delta\subset S_{k_{0}}$ be finite. This means there is a largest $m\in\mathbb{N}$ for which a sentence of the from 6 occurs in $\Delta$. Therefore, $\Delta$ says "I will have at least $m$ elements on any model". That is, the domain of any model $M$ satifying $\Delta$ will have at least $m$-elements. Let $N>m$, and recall that since $\neg\mathrm{FRT}$ for $k_{0}$, there is an $r$-coloring $c_{N}:[N]^{p}\rightarrow [r]$ having no homoegeous subset of size $k_{0}$. We define a model $M$ as follows:

1. $U_{M}=[N]$.
2. $C^{i}_{M} = \{(a_{1},\ldots,a_{p})\in U_{M}^{p}: \{a_{1},\ldots,a_{p}\}\in[N]^{p}\text{ and }c_{N}(\{a_{1},\ldots,a_{p}\})=i\}$ for $1\leq i\leq r$ (where $U_{M}^{p}$ denotes the cartesian product of $p$ copies of $U_{M}$).
3. $=_{M}$, i.e. the obvious interpretation of $=$.

Now, let us check that $M=(U_{M},C^{i}_{M}:1\leq i\leq r,=_{M})$ satisfies $\Delta$:

1. $M$ satisfies the sentences of 1 in $\Delta$ becasue $C^{i}a_{1},\ldots,a_{p}$ true iff $\{a_{f(1)},\ldots,a_{f(p)}\}\in[N]^{p}$ for any permutation $f$ of $[p]$ iff $(a_{f(1)},\ldots,a_{f(p)})\in C^{i}_{M}$ for any permutation $f$ of $[p]$ iff $C^{i}a_{f(1)}\ldots a_{f(p)}$ is true.
2. $M$ satisfies the sentences of 2 in $\Delta$, since $C^{i}a_{1}\ldots a_{p}$ true iff $(a_{1},\ldots,a_{p})\in C^{i}_{M}$ iff $\{a_{1},\ldots,a_{p}\}\in[N]^{p}$, which clearly implies the $a_{j}$ are all distinct.
3. $M$ satisfies the sentences of 3 in $\Delta$ because if $\displaystyle\bigwedge_{1\leq u<v\leq p}\neg(a_{u}=a_{v})$ is true, then $\{a_{1},\ldots,a_{p}\}\in[N]^{p}$, which implies that $c_{N}$ assigns a color $i$ to $\{a_{1},\ldots,a_{p}\}$. That is, $(a_{1},\ldots,a_{p})\in C^{i}_{M}$.
4. $M$ satisfies the sentences of 4 in $\Delta$ because $c_{N}$ is a function. Therefore for $1\leq i<j\leq r$, $\neg(C^{i}a_{1}\ldots a_{p}\wedge C^{j}a_{1}\ldots a_{p})$ is true iff for $1\leq i<j\leq r$, $(a_{1},\ldots,a_{p})\not\in C^{i}_{M}\cap C^{j}_{M}$.
5. $M$ satisfies the sentences of 5 in $\Delta$ because $c_{N}$ does not have a homogeneous subset of size $k_{0}$. Therefore if $\displaystyle\bigwedge_{1\leq u<v\leq k_{0}}\neg(a_{u}=a_{v})$ is true, the set $\{a_{1},\ldots,a_{k_{0}}\}$ is not homogeneous for $c_{N}$, which implies that it is colored by at least two colors, which implies that $[\{a_{1},\ldots, a_{k_{0}}\}]^{p}$ it is colored by at least two colors, which implies that for each color $1\leq i\leq r$ there is at least one $p$-element subset of $\{a_{1},\ldots,a_{k_{0}}\}$ which is not colored by $i$; i.e. it imples that $\displaystyle\bigvee_{1\leq i_{1}<\cdots<i_{p}\leq k_{0}}\neg C^{i}a_{i_{1}}\ldots a_{i_{p}}$ is true.
6. Since $N>m$, the domain $U_{M}$ certainly has at least $m$ elements. That is, $\varphi_{n}$ is satisfied for all $0\leq n\leq m$. Therefore, $M$ satisfies the sentences of 6 in $\Delta$.
7. $M$ clearly satisfies the sentences of 7 in $\Delta$.

By first-order compactness, the set $S_{k_{0}}$ has a model $M'$ whose domain $U_{M'}$ is countably infinite. Moreover, since $M'$ satisfies $S_{k_{0}}$, any $r$-coloring $c$ of $[U_{M'}]^{p}$ fails to have a homogeneous subset of size $k_{0}$. That is, $\mathrm{IRT}$ fails for $M'$, as desired (recall that if $\mathrm{IRT}$ holds for $M'$, $c$ would have an infinite homogeneous subset, and therefore homogeneous subsets of size $k$ for all $k\in\mathbb{N}$).