Kruskal's tree theorem and $\Pi_1$ sentences of linear orderings with finitely many constants

Question

In their paper "Theories with recursive models" [1] Lerman and Schmerl used a version of Kruskal's tree theorem about finite n-augmented trees.

An n-augmented tree is a tree T together with $n$ unary relation symbols on its universe. The version of Kruskal's theorem is as follows

Theorem 1. Suppose $n<\omega$ and $A_0,A_1,\dots$ is a sequence of finite n-augmented trees. Then there are $i<j<\omega$ such that $A_i$ embeds in $A_j$.

They then used the following fact about $\Pi_1$ sentences in the language of linear orderings with finitely many constants in their proof that any $\Sigma_2$ theory of linear orderings has a recursive model. We denote with $L^F$ the language containing $\leq$ and a constant symbol $c_i$ for every $i\in F$.

Fact. For every finite set of constants $F$ and every set $\Phi$ of $\Pi_1$ sentences in $L^F$ consistent with the theory of linear orderings $LO$, there is finite $\Phi_0\subseteq \Phi$ such that $LO\vdash \Phi_0 \leftrightarrow \Phi$.

They do not give a proof of this fact and say that it follows easily from Theorem 1. I can see intuitively why the above fact should hold but how does this follow from Theorem 1?

[1] Lerman, Manuel, and James H. Schmerl. 1979. “Theories with Recursive Models.” The Journal of Symbolic Logic 44 (1): 59–76. https://doi.org/10.2307/2273704.

Answer 1

Towards a contradiction, suppose not. Then we can find a sequence $\phi_0, \phi_1, \dots$ from $\Phi$ such that for all $i$, $LO, \phi_0, \dots, \phi_i \not \vdash \phi_{i+1}$. So for each $i$, there is an $L^F$-model $M_i$ with $M_i \vDash LO \wedge \phi_0, \dots, \phi_i \wedge \neg \phi_{i+1}$. Since these are finitary $\Pi_1$ sentences, it's not hard to argue that we can take $M_i$ to be finite.

Each $M_i$ is a $|F|$-augmented tree, using a unary relation symbol to pick out each constant, and interpreting a linear order as a non-branching tree. By Theorem 1, there is an $i < j$ with $M_i$ embedding in $M_j$. But $M_j \vDash \phi_{i+1}$, and since this is $\Pi_1$, it must be that $M_i \vDash \phi_{i+1}$, contrary to choice of $M_i$.