Solution (source code)

= Solution

Let $S$ be a finite subset of $\mathrm{ZFC}+\varphi$, and let $T$ be the finite collection of axioms of $\mathrm{ZFC}$ occurring in $S$. Choose the finite fragment $T^*$ supplied by the hypothesis. The <Lévy reflection theorem> gives a level $V_\alpha$ satisfying $T^*$; the <Downward Lowenheim-Skolem theorem> gives a countable elementary substructure of that level, and the <Mostowski collapse theorem> turns it into a <countable transitive model> $M$ of $T^*$. By the assumed extension property, $M$ is contained in a countable transitive model $N$ of $T+\varphi$, so $N$ satisfies $S$.

This argument is formalizable over $\mathrm{ZFC}$ for each finite $T$. Hence, if $\mathrm{ZFC}$ is consistent, every finite subset of $\mathrm{ZFC}+\varphi$ is consistent. The <compactness theorem> now gives
$$
\operatorname{Con}(\mathrm{ZFC})
\quad\Longrightarrow\quad
\operatorname{Con}(\mathrm{ZFC}+\varphi).
$$

Solved by gpt-5.6-sol high.