Fixed finite-fragment verification for the Cohen countermodels

In ZFC let $\lambda =(2^{{\mathrm{\aleph }}_0}{)}^{+}$ and use $P=\mathrm{Add}(\omega ,\lambda )$. The empty condition witnesses nonemptiness. The finite-partial-function definition gives the preorder and generic-coordinate names as sets. The delta-system ccc argument and the maximal-antichain cardinal-preservation argument in F2 are ZFC proofs; for this fixed $\mathrm{\Delta }$, collect the finitely many axioms and schema instances they use. AC is used for the cardinal successor and the maximal-antichain argument.

For distinct $\xi ,\eta <\lambda$, extending a condition at a fresh bit forces the $\xi$ and $\eta$ coordinate reals to differ. Thus $\lambda$ injects into the reals of the extension. Since $P$ preserves ${\mathrm{\aleph }}_2$, it forces $2^{{\mathrm{\aleph }}_0}\ge {\mathrm{\aleph }}_2$, hence $\mathrm{\neg }\mathrm{C}\mathrm{H}$. GCH implies CH at $\omega$, so the same extension forces $\mathrm{\neg }\mathrm{G}\mathrm{C}\mathrm{H}$. No ground-model CH or equality for the continuum is used.

For the chosen $\mathrm{\Delta }$, include its finitely many ZFC axioms and the finite instances needed to verify the forcing relation, the generic extension, cardinal preservation, and step 2.1. The forcing theorem supplies a formal derivation that every condition forces each target member; the quantified schema instances in $\mathrm{\Delta }$ are handled one at a time as their actual formulas, with their translated forcing instances included in the finite source fragment. F1 now yields a ZFC proof that a model of this fixed $\mathrm{\Delta }$ exists. The choices of proofs and finite support may depend on $\mathrm{\Delta }$; no arithmetic uniformity or PA checker theorem follows.