Consistency strength of assuming the existence of countable transitive model of $\mathsf{ZFC}$

102 Views Asked by At

In order to do forcing, it is convenient to assume the existence of countable transitive model of $\mathsf{ZFC}$. Add a constant symbol $M$ to the language and let the theory $\mathsf{CTM}$ consist of the statements "$M$ is countable", "$M$ is transitive", and all the relativizations of $\mathsf{ZFC}$ to $M$. The book "Forcing For Mathematicians" by Nik Weaver claims that $$\mathrm{Con}(\mathsf{ZFC}) \rightarrow \mathrm{Con}(\mathsf{ZFC} + \mathsf{CTM})$$ but by Gödel's incompleteness theorem, $$\mathrm{Con}(\mathsf{ZFC}) \nrightarrow \mathrm{Con}(\mathsf{ZFC} + \mathrm{Con}(\mathsf{ZFC}))$$ I was wondering why this is possible, and came to a conclusion. We can not internalize $\mathsf{CTM}$ completely in $\mathsf{ZFC}$ to prove $\mathrm{Con}(\mathsf{ZFC})$ since we are not using infinitary logic. Then I have another question. Following the reasoning, to show that $$\mathsf{ZFC} \vdash \kappa \text{ is inaccessible} \rightarrow (V_\kappa, \in) \text{ is a model of } \mathsf{ZFC}$$ we should not only merely prove that all the relativizations of $\mathsf{ZFC}$ to $V_\kappa$ holds, but also completely internalize the proof in $\mathsf{ZFC}$. Is this right?