Absoluteness of $ \text{Con}(\mathsf{ZFC}) $ for Transitive Models of $ \mathsf{ZFC} $. Is $ \text{Con}(\mathsf{ZFC}) $ absolute for transitive models of $ \mathsf{ZFC} $? It appears that $ \text{Con}(\mathsf{ZFC}) $ is a statement only about logical syntax. Taking any $ \in $-sentence $ \varphi $, we can write $ \text{Con}(\mathsf{ZFC}) $ as $ \mathsf{ZFC} \nvdash (\varphi \land \neg \varphi) $, which appears to be an arithmetical $ \in $-sentence.
If this is true, then I think one can get a quick proof of
$$
\mathsf{ZFC} + \text{Con}(\mathsf{ZFC}) \nvdash
\langle \text{There exists a transitive model of $ \mathsf{ZFC} $} \rangle,
$$
assuming that $ \mathsf{ZFC} + \text{Con}(\mathsf{ZFC}) $ is consistent.
Proof If
$$
\mathsf{ZFC} + \text{Con}(\mathsf{ZFC}) \vdash
\langle \text{There exists a transitive model of $ \mathsf{ZFC} $} \rangle,
$$
then let $ M $ be such a transitive model. By the absoluteness of $ \text{Con}(\mathsf{ZFC}) $, we see that $ M \models \mathsf{ZFC} + \text{Con}(\mathsf{ZFC}) $. Hence, $ \mathsf{ZFC} + \text{Con}(\mathsf{ZFC}) $ proves the consistency of $ \mathsf{ZFC} + \text{Con}(\mathsf{ZFC}) $. By Gödel’s Second Incompleteness Theorem, $ \mathsf{ZFC} + \text{Con}(\mathsf{ZFC}) $ is therefore inconsistent. Contradiction. $ \blacksquare $

Question: Is $ \text{Con}(\mathsf{ZFC}) $ absolute for transitive models, and is the above proof correct?

Thanks for any clarification.

Yes, $\text{Con}(\mathsf{ZFC})$ is an arithmetic statement ($\Pi^0_1$ in particular, because it says a computer program that looks for an inconsistency will never halt) so it is absolute to transitive models, and your proof is correct.
By the way, there are a couple of ways you can strengthen it.  First, arithmetic statements are absolute to $\omega$-models (models with the standard integers, which may nevertheless have nonstandard ordinals) so $\text{Con}(\mathsf{ZFC})$ does not prove the existence of an $\omega$-model of $\mathsf{ZFC}$.  Second, the existence of an $\omega$-model of $\mathsf{ZFC}$ does not prove the existence of a transitive model of $\mathsf{ZFC}$, because the existence of an $\omega$-model of $\mathsf{ZFC}$ is a $\Sigma^1_1$ statement, and $\Sigma^1_1$ statements are absolte to transitive models.
