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

In their paper "Theories with recursive models"  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?

 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.

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$.