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

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.