Finite-fragment compiler for the PFA iteration

Fix the source and target proof predicates. Let $\mathrm{Good}(P)$ be the fixed source formula saying that some supercompact $\kappa$ and Laver function $\mathrm{\ell }$ witness that $P$ is the recursively defined Laver-guided iteration. The stored formalization of F1 proves $\mathrm{\exists }P\mathrm{Good}(P)$ and proves from $\mathrm{Good}(P)$ the nonemptiness and forcing conclusions of F1. Define by recursion on a parsed membership formula $\phi$ the code ${\mathrm{Forc}}_P(\phi )$ of “$1_P$ forces $\phi$,” leaving $P$ as the one displayed free parameter. Atomic clauses insert the two fixed forcing-relation formulas; Boolean connectives and quantifiers insert the corresponding fixed clauses with fresh variables. F4 supplies parsing and capture-free substitution; fresh indices are obtained by a bounded scan above the largest parsed index, and F5 supplies the bounded syntax-tree traversal and output-list recursion. Alongside the formula code, the recursion emits the fixed logical derivations showing that forcing respects each logical axiom and inference rule. Invalid formula codes return the fixed tautology proof.

Define the target-axiom constructor $A$ from the certified templates in Given. For each of the finitely many nonschematic ZFC axioms it returns the corresponding stored forcing proof. On a certified Separation instance for $\phi$, it substitutes ${\mathrm{Forc}}_P(\rho \in \sigma \wedge \phi )$ into the supplied name-and-Separation template; on a Replacement instance it substitutes into the supplied least-witness-rank template and its bounding name. The Power Set branch inserts the stored subname construction, and the Choice branch inserts the stored ground-well-order and least-fibre construction. The PFA tag returns the one stored formalization of F1, including the forced-proper name normalization, image factor, lifted-embedding formula, image-generated filter, and elementarity reflection. Each branch is weakened by the antecedent $\mathrm{Good}(P)$ and finishes with the supplied checker-certified derivation of $\mathrm{Good}(P)\to {\mathrm{Forc}}_P(\delta )$ for its input axiom $\delta$. F4 verifies the displayed substitutions and certificate tags, while F5 supplies the finite template and list assembly. No truth evaluator, proof search, or uniformity inference from F2 occurs.

Traverse a certified finite fragment $\mathrm{\Delta }$, apply $A$ to each entry, rename bound and proof-line variables above the current maxima, concatenate the blocks, and collect the nonlogical source-axiom certificates actually appearing. The resulting finite list $\mathrm{\Gamma }(\mathrm{\Delta })$ contains the supercompact axiom because this compiler uniformly uses the PFA iteration, and it contains exactly the finitely many ZFC schema instances used by the emitted derivations. It also contains the parameter, preorder, forcing-recursion, proper-iteration, factorization, master-condition, and forcing-truth instances occurring in that fixed block, together with the fixed proof of $\mathrm{\exists }P\mathrm{Good}(P)$. Thus the output proves every finite ground fact and every conditional $\mathrm{Good}(P)\to {\mathrm{Forc}}_P(\delta )$ for $\delta \in \mathrm{\Delta }$, not merely a citation to the semantic theorem. For each particular output fragment, F2 identifies these finite proof roles; it does not construct the traversal.

Every loop in steps 1.1–3.1 is bounded by a decoded formula, proof, or fragment length; every update is one of F4's primitive-recursive syntax operations or F5's primitive-recursive list recursions. Hence their composition is primitive recursive. PA proves the following simultaneous invariant by induction first on formula-tree size and then on the fragment position: every returned line reference is earlier than its use, every substitution passes the free-for test, each source axiom line carries its supplied certificate, and the last line of the block is the advertised forcing formula. Constant branches reduce to checking fixed finite numerals; the two schematic branches use the constructor tags and annotations that F4's checker recomputes. F6 supplies PA-provably total single-valued graphs for the composite functions. This verifies totality and checker acceptance rather than inferring either from F1 or F2.

Now define $R$ on a proposed target proof $p$. If F4 rejects $p$ or its conclusion is not the fixed contradiction, put $R(p)=0$. Otherwise scan its lines. For a target-axiom line append the block supplied by $A$. For a logical-axiom line append the corresponding forcing-logic block from step 1.1, weakened by $\mathrm{Good}(P)$. For modus ponens, generalization, or existential elimination, append the fixed block deriving $\mathrm{Good}(P)\to {\mathrm{Forc}}_P(\phi )$ for the conclusion $\phi$ from the already emitted conditional translations of the cited earlier lines, after renumbering its references. Maintain the table sending each input line to its output concluding line. The final target contradiction therefore yields $\mathrm{Good}(P)\to 1_P⊩\mathrm{\perp }$. Append the fixed derivation that nonemptiness of $P$ implies $1_P⊮\mathrm{\perp }$; since $\mathrm{Good}(P)$ includes nonemptiness, obtain $\mathrm{\forall }P\mathrm{\neg }\mathrm{Good}(P)$. Combining this with F1's stored source proof of $\mathrm{\exists }P\mathrm{Good}(P)$ gives an $S$-refutation without adding a witness constant to the source language.

PA induction on the decoded line number proves the precise loop invariant $\text{if the first }i\text{ target lines check, the output prefix checks and ends each line block with its forcing translation.}$ The axiom, logical, and inference cases are exactly the branches in step 5.1, and malformed references take only the rejected-input branch. F4 checks the input and every emitted annotation; F5 supplies the bounded output-list and table recursions, and F6 proves the composite functions total. PA therefore verifies $\mathrm{\forall }p({\mathrm{Prf}}_T(p,<mi\; mathvariant="normal">⌜</mi>\mathrm{\perp }<mi\; mathvariant="normal">⌝</mi>)⟶{\mathrm{Prf}}_S(R(p),<mi\; mathvariant="normal">⌜</mi>\mathrm{\perp }<mi\; mathvariant="normal">⌝</mi>))\mathrm{.}$ This supplies all constructor verifications demanded by F3, including the zero-occurrence case in which no PFA block is emitted.

Steps 1.1–4.1 give the promised compiler on every finite target fragment, and steps 5.1–6.1 give its verified refutation-reduction form. The construction manipulates finite codes only. F2 is used only after an output is fixed, to identify the finite semantic proof roles that output must realize; the uniform templates and their PA correctness derivations are the explicit certified data in Given. F1 supplies the one fixed object-theoretic PFA block. No step asserts that consistency creates a generic extension or a countable transitive model of full $S$ or full $T$.