Are $\Pi_2$ consequences of universal theories witnessed by finitely many terms?

Question

Here is a question in model theory I need help. Suppose $T$ be a set of universal sentences and $T\models\forall x\exists y\:P(x,y)$. Prove that there exists terms $t_1(x),\cdots,t_n(x)$ such that $$ T\models\forall x \bigvee^n_{k=1}P(x,t_k) $$ Intuitively, it is obvious true but I need a rigorous proof which should involve the compactness theorem.

Answer 1

The desired result turns out to be a form of Herbrand's Theorem. The statement given in the question is virtually identical to one appearing in the paper "On Herbrand's Theorem" by Samuel R. Buss, as shown here:

That paper appears In "Logic and Computational Complexity, Lecture Notes in Computer Science #960", 1995, Springer-Verlag, pp. 195-209 and is available online. Buss's proof however is proof-theoretic, and so is the proof sketch on the Wikipedia page for the theorem.

This question as posed here however is for a proof in model theory. There is a model-theoretic proof in Joseph Shoenfield's classic text "Mathematical Logic" (1967), and you can find Shoenfield's exposition revisited in detail in a bachelor's thesis by E. J. Gerritse, available online at https://www.cs.ru.nl/bachelors-theses/2015/Emma_Gerritse___4248120___Herbrands_theorem.pdf.

It seems inappropriate to recap the rather lengthy model-theoretic proof in an answer here, so please refer to one of these high-quality sources.

In spite of the request for a proof that uses compactness and the alleged application of compactness in another answer, I do not believe there is any appeal to compactness in these model-theoretic proofs. It would be interesting to see if compactness can play a role.

Answer 2

I assume that $P$ is supposed to be quantifier-free; otherwise, as discussed in the comments, the result is false.

First, note that since $T$ consists of universal sentences, if $M$ is any model of $T$, then any substructure of $M$ is also a model of $T$. In particular, given $a\in M$, the substructure $N$ generated by $a$ consists of elements represented by terms in $a$, and $N\models\exists y P(a,y)$. Thus, there is a term $t(a)$ such that $N\models P(a,t(a))$, and hence $M\models P(a,t(a))$ as well since $P$ is quantifier-free.

So, for any $a$ in any model of $T$, there is some term $t(a)$ such that $P(a,t(a))$ is true. In other words, adding a constant symbol $c$ to the language, the infinite disjunction $\bigvee_i P(c,t_i(c))$ is true in every model of $T$, where $t_i$ ranges over all possible terms. By compactness, there must be finitely many $t_1,\dots,t_n$ such that $T\models\bigvee_{k=1}^n P(c,t_k(c))$, and so $T\models \forall x \bigvee_{k=1}^n P(x,t_k(x))$