Suppose I have a (incomplete) theory $T$ (e.g. PA) which I skolemize to get a theory $T\_S$ in the expanded language. I now build $T'$ by adding to $T\_S$ any sentence $(\forall x)\phi(x)$ where I can prove (say using ZFC as my background set theory) that for all terms $t$ in my skolemized language $ T\_S \vdash\phi(t)$


In some sense $T'$ is kinda what you get if you assume that all objects are constructed via skolem functions.


Is $T'$ in general a conservative extension of $T$? When $T$ is PA?


Obviously, $T'$ has to be consistent as it's true of the model one gets via the standard Skolem construction over $T$ but I have no idea if it's conservative. Since this is a pretty natural idea I presume this has been studied before and I'd love any pointer to where I can read more about the properties that $T'$ or further iterates ($T''$ etc..) would have.



Is adding all sentences true of terms in skolemized theory conservative?
So I can mark this answered (when I can tmw) I'm posting [Emil Jeřábek's](https://mathoverflow.net/users/12705/emil-je%c5%99%c3%a1bek) comment as an answer but they deserve all the credit.


Suppose that $(\forall x)\phi(x)$ is in $T' - T\_S$. That means we've proved that $T\_S \vdash \phi(t)$ for each term $t$ in our skolemized language. Now define


$$\theta(y) = \left(\lnot\phi(y) \lor (\forall x)\phi(x)\right)$$


$(\exists y)\theta(y)$ is a tautology so it's in $T$ and when we skolemize we introduce a constant $c$ and place $\theta(c)$ into $T\_S$. By above (and assuming background theory doesn't prove false claims) $T\_S \vdash \phi(c)$. Hence, as $\theta(c) \land \phi(c) \implies (\forall x)\phi(x)$ we have that $T\_S \vdash (\forall x)\phi(x)$. Hence, $T'=T\_S$


As $T\_S$ was itself conservative over $T$ this answers the question.


