Is adding all sentences true of terms in skolemized theory conservative?

Question

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.

Answer 1

So I can mark this answered (when I can tmw) I'm posting Emil Jeřábek's 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.