Can a theory prove (schematically) its axioms relativized to a set? In $\mathsf{ZFC}$, a somewhat cheating way to buy "transitive models" without cost in consistency is to add to the language a constant symbol $M$ and add to $\mathsf{ZFC}$ the axioms stating that $M$ is countable transitive, and for each axiom of $\mathsf{ZFC}$, add its relativization to $M$. This allows us to "pretend" that we have a transitive model of $\mathsf{ZFC}$ (the catch is that this is a theorem schema).
I wonder if adding a constant symbol is necessary. In other words, can there be some theory $T$ (extending $\mathsf{ZFC}$) in the language $\{\in\}$, such that T can prove there is a set $M$, and $T$ proves each of its own axioms relativized to $M$?
 A: $\mathsf{ZFC}$ already has this property. Specifically:

*

*The reflection theorem shows that every model of $\mathsf{ZFC}$ - even of $\mathsf{ZFC+\neg Con(ZFC)}$ - contains a model of $\mathsf{ZFC}$. (This model might not internally be a model of $\mathsf{ZFC}$, which is why this isn't an obvious absurdity.)


*The fact that satisfiability is absolute to $L$ then lets us pick out a specific model, via the $L$-ordering.
The details are as follows:
Working in $\mathsf{ZFC}$, fix some standard enumeration of the $\mathsf{ZFC}$ axioms and let $T_0$ be the largest initial segment of that enumeration which is consistent. Classically of course we have (under the usual assumptions) that $T_0=\mathsf{ZFC}$; meanwhile, note that $\mathsf{ZFC}$ proves  "$T_0$ is consistent" (trivially) as well as "$\varphi\in T_0$" for each $\varphi\in\mathsf{ZFC}$ (by the reflection theorem).
Now since $\mathsf{ZFC}$ proves that $T_0$ is consistent, we can - in $\mathsf{ZFC}$ - consider $M=$ the least constructible set model of $T_0$, where "least" refers to the standard ordering on $L$. This is provably in $\mathsf{ZFC}$ a model of $T_0$, and so for each $\mathsf{ZFC}$-axiom $\varphi$ we have $\mathsf{ZFC}\vdash M\models\varphi$ as desired.
