Finite Ramsey Theorem via many-sorted logic compactness + infinite Ramsey theorem

Question

Here you will find the relevant definitions, statements of Ramsey's theorems, and how propositional compactness + infinite Ramsey Theorem ($\mathrm{IRT}$) can be used to prove the finite Ramsey theorem ($\mathrm{FRT}$). Here first-order compactness is used instead of propositional compactness.

I am learning the basic concepts of many-sorted logic, and I thought it would be good practice to show that that $\mathrm{FRT}$ follows from $\mathrm{IRT}$ via many-sorted logic compactness.

The idea is using many-sorted logic 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 many-sorted 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 compactness. This will yield a model in which $\mathrm{IRT}$ fails.

The language $L$ consists of:

1. Two sorts $\{s_{1},s_{2}\}$. Intuitively, the two sorts will serve to encode the idea of $p$-element subsets of $\mathbb{N}$ and $k_{0}$-element subsets of $\mathbb{N}$, i.e. elements of $[\mathbb{N}]^{p}$ and $[\mathbb{N}]^{k_{0}}$, respectively.
2. $1$-ary predicates $C^{1},\ldots,C^{r}$ of sort $(s_{1})$. Intuitively, $C^{i}x$ expresses that the $p$-element subset $x$ is assigned color $i$.
3. A $2$-ary predicate $D$ of sort $(s_{1},s_{2})$. Intuitively, $Dxy$ expresses that $x$ is a $p$-element subset of $y$.
4. Equality symbols $=_{1}$ and $=_{2}$ for the sorts.
5. Variables $x_{1},x_{2},\ldots$ of sort $(s_{1})$ and $y_{1},y_{2},\ldots$ of sort $(s_{2})$

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

1. $\varphi_{n}:=\displaystyle\exists_{1} x_{1}\ldots\exists_{1} x_{n}\,\left(\bigwedge_{1\leq u<v\leq p}\neg(x_{u}=_{1} x_{v})\right)$ for all $n\in\mathbb{N}$
2. $\psi_{n}:=\displaystyle\exists_{2} y_{1}\ldots\exists_{2} y_{n}\,\left(\bigwedge_{1\leq u<v\leq p}\neg(y_{u}=_{2} y_{v})\right)$ for all $n\in\mathbb{N}$.

1 and 2 express that there are infinitely many elements in our two sorted domains.

3. $\displaystyle\forall_{1}x\,\bigvee_{1\leq i\leq r}C^{i}x$ for all $1\leq i\leq r$. Each $p$-element subset is assigned at least one color.
4. $\displaystyle\forall_{1}x\;\neg(C^{i}x\wedge C^{j}x)$ for all $1\leq i<j\leq r$. Each $p$-element subset is assigned at most one color.
5. $\displaystyle\forall_{2}y\hspace{1mm}\exists_{1}x\hspace{1mm}\left(Dxy\wedge\left(\bigvee_{1\leq i\leq r}\neg C^{i}x\right)\right)$. Every $k_{0}$-element subset has at least one $p$-element subset which is not colored by $i$, i.e. every $k_{0}$-element subset has at least one $p$-element subset for at least two different colors.

5 expresses that there will not be a homogeneous subset of size $k_{0}$ for the $r$-coloring.

6. Equality axioms for $=_1$ and $=_2$.

Question: Did I define $L$ and $S_{k_{0}}$ correctly? How does one show finite satisfiability in the context of many-sorted compactness?

Answer 1

In order to remove the question from the unanswered list, I will post the edit to the original question as an answer.

Based on the language $L$ and set $S_{k_{0}}$ of $L$-sentences, a model $M$ has the form $(\{U_{1},U_{2}\}, C_{M}^{i}:1\leq i\leq r, D_{M}, =_{1}^{M}, =_{2}^{M})$, where $U_{1}$ and $U_{2}$ are our domains, one for each sort. $C_{M}\subseteq U_{1}$, and $D_{M}\subseteq U_{1}\times U_{2}$. Finite satisfiability is then proven similarly to how it is done in single-sorted logic. Indeed, since $\Delta$ is finite there are largest $n_{0},n_{1}\in\mathbb{N}$ for which $\varphi_{n_{0}}$ and $\psi_{n_{1}}$ occur in $\delta$. Let $N>\max\{n_{0},n_{1}\}$, and and recall that since $\neg\mathrm{FRT}$ for $k_{0}$, there is an $r$-coloring $c_{N}:[N]^{p}\to[r]$ having no homoegeous subset of size $k_{0}$. We define de model $M$ as follows:

1. $U_{1}:=[N]^{p}$ is the domain of sort $s_{1}$ and $U_{2}:=[N]^{k_{0}}$ is the domain of sort $s_{2}$.
2. $C^{i}_{M}:=\{a\in U_{1}^{M}:c_{N}(a) = i\}$ for $1\leq i\leq r$.
3. $D_{M}:=\{(a,b)\in U_{1}\times U_{2}:a\in[b]^{p}\}$.
4. $=_{1}^{M}$ and $=_{2}^{M}$ are the obvious interpretations of $=_{1}$ and $=_{2}$.

If I have not made mistakes, it should be straightforward to check that $M$ indeed satisfies $\Delta$. Briefly: Axioms 1 and 2 are satisfies because the domains have cardinalities $N^{p}$ and $N^{k_{0}}$, respectively. Both are greater than $N$ (recall that $p,k_{0}\in\mathbb{N}^{+}$). Axioms 3 and 4 are satisfied because $c_{N}$ is an $r$-coloring. Axiom 6 is satisfied because $c_{N}$ does not have a homogeneous subset of size $k_{0}$. Finally, axiom 6 is clearly satisfied.