= Solution
Adjoin to $T$ the <negations> of all closed-term instances of $\theta$. If the resulting <set> had a <first-order model> $\mathcal A$, its <ground-term substructure> $\mathcal B$ from (ii) would still <first-order model> $T$. The assumed existential consequence therefore supplies a <tuple> $\vec b$ in $\mathcal B$ satisfying $\theta$. Each $b_j$ is the value of a <closed term> $t_j$.
Quantifier-free agreement between a <substructure> and its ambient <first-order structure> gives
$$
\mathcal A\models\theta(t_1,\ldots,t_k),
$$
contradicting the adjoined <negation> of this very ground instance. Thus
$$
T\cup\{\neg\theta(t_1,\ldots,t_k):t_1,\ldots,t_k\text{ closed terms}\}
$$
is unsatisfiable. <Compactness theorem> gives a finite unsatisfiable <subset>. Its finitely many ground <negations> imply that, for some finite list of <first-order term> <tuples>,
$$
\boxed{T\models\bigvee_{i=1}^m\theta(t_{i1},\ldots,t_{ik}).}
$$
If the finite <subset> already shows $T$ itself inconsistent and supplies no ground <negations>, choose any one closed-term <tuple> using the available constant; then any <first-order sentence> is a consequence of $T$, so $m=1$ suffices. Otherwise the selected list is nonempty. This also explains why the conclusion contains a finite disjunction rather than necessarily one universal choice of a witness <first-order term>.
Back to article page
