Relative consistency of no free ultrafilters on any set over ZF

By F2, the hypothesis gives $\mathrm{Con}(\mathrm{Z}\mathrm{F}\mathrm{C}+\mathrm{G}\mathrm{C}\mathrm{H})$. Suppose for contradiction that the target theory $T=\mathrm{Z}\mathrm{F}+\text{"every ultrafilter on every set is principal"}$ is inconsistent. One formal refutation is a finite sequence and therefore uses only a finite list $\mathrm{\Delta }$ of ZF axiom instances together with the displayed extra sentence.

Apply F1 to this exact external $\mathrm{\Delta }$. The finite ZFC source isolated there, and hence ZFC+GCH, proves that a set structure satisfies every sentence used in the alleged refutation. The fixed first-order soundness induction for that finite derivation would then make ZFC+GCH prove that the structure satisfies a contradiction; equality logic proves that no structure does. This contradicts step 1.1.

Consequently $T$ is consistent. The empty-proof and zero-axiom cases cannot be refutations because no last contradiction line is present; a one-line alleged refutation is covered by the same soundness check. The argument uses only the finite support of one hypothetical proof. It invokes neither semantic completeness nor a countable transitive model of full ZF, and it concludes only conditional syntactic consistency.