Finite-fragment interpretation in L with GCH

Fix the promised presentation explicitly. Expand $D(x)$ from the usual finite-formula definition of $L$: a witness is a set-sized ordinal hierarchy history beginning with the empty set, taking definable subsets at successors and unions at limits, and containing $x$ in one of its values. Expand ordered pairs, functions, ordinals, formula words and finite satisfaction tables into the primitive membership syntax. Use the least fresh variable at every renaming. Add to the F5 certificates tag $3$ for the selected well-ordering form of AC and tag $4$ for the selected GCH sentence saying that, for each infinite initial ordinal $\kappa$, the power set of $\kappa$ is bijective with its next initial ordinal. These are finite formulas, so formula recognition, certificate checking and raw $D$-relativization are primitive recursive and have literal, rather than merely alpha-equivalent, output codes.

We construct a proof-producing map on accepted target-axiom certificates. For each of the six fixed ZF tags, expand the corresponding finite derivation from F1 in the fixed calculus and store its code. Do the same for the fixed AC and GCH derivations from F2; the AC block includes the finite equivalence from the selected well-ordering sentence to the choice formulation used there, and the GCH block includes the finite expansion of initial ordinals, successor cardinals and bijections. Substitution and alpha-renaming append the required domain guards and give the exact raw-relativization endpoints. There are only eight such blocks, so they are constants of a primitive-recursive dispatcher, not an appeal to a truth predicate or to a model of ZF.

For a Separation certificate with matrix $\varphi (z,\bar{p})$, recurse through the parse tree of $\varphi$ and compile the usual satisfaction-relativization equivalence for every subformula. Compile the finite witness-rank iteration for that subformula closure above a level containing $a,\bar{p}$; its terminal level $L_{\beta }$ reflects every member of the closure. Ambient Separation then forms $b=\{z\in a:(L_{\beta },\in )\models \varphi [z,\bar{p}]\}$, and the finite Decode/Def block puts $b$ in $L_{\beta +1}$. The compiled equivalence identifies this with $\{z\in a:{\varphi }^L(z,\bar{p})\}$. Universal generalization over the parameters, followed by the fixed propositional rearrangements, ends at the literal $D$-relativization of the F5 Separation sentence. Empty $a$ and an empty defined subset use the same block and require no witness choice.

For a Replacement certificate with matrix $\varphi (z,w,\bar{p})$, first use ambient Replacement on the functional formula $D(w)\wedge {\varphi }^L(z,w,\bar{p})$ to form its image $Y$. A second ambient Replacement on constructible ranks, followed by Union and successor, produces $\beta$ with $Y\subseteq L_{\beta }$ and with $a,\bar{p}\in L_{\beta }$. Invoke the constructor of step 2.2 on the original image matrix $\mathrm{\exists }z(z\in a\wedge \varphi (z,w,\bar{p}))$, not on an already relativized formula. Its $L$-Separation block cuts exactly $Y$ out of $L_{\beta }$; internal functionality gives both directions of the required image biconditional. This also covers $a=\mathrm{\varnothing }$. The rank-bound, uniqueness, Separation and final universal-closure templates are fixed Hilbert proof schemata, while the only varying pieces are capture-free substitutions of the parsed matrix. Consequently their expansion ends at the exact F5 Replacement relativization.

The constructions in steps 2.1–3.1 use only finite list operations, structural recursion on a checked formula parse, capture-free substitution, and concatenation or index-shifting of finite derivations. Induction on the subformula schedule proves that every generated line is either one of the six logical schemes of the fixed calculus, an axiom carrying its F5 certificate, or one of its three rules applied to earlier lines. PA formalizes this bounded induction and the line-prefix induction of the proof checker. It therefore proves that the dispatcher is total and that every accepted target-axiom certificate is sent to a ZF proof whose conclusion is its literal $D$-relativization. On malformed input the dispatcher returns a fixed proof of a tautology; correctness is asserted only under the accepted-certificate antecedent. The large concrete endpoint codes and executable regression checks are useful finite checks of the selection, but are not being identified with this PA derivation.

Now fix finite $\mathrm{\Delta }$. Apply the dispatcher to its finitely many members. From the resulting translated-axiom proofs and the finitely many fixed interpretation-obligation proofs, extract every nonlogical ZF axiom sentence that actually occurs, and let $\mathrm{\Gamma }$ be the union of those finite supports. Proof codes themselves are not members of $\mathrm{\Gamma }$. Every member of $\mathrm{\Gamma }$ therefore has an F5 axiom certificate, so $\mathrm{\Gamma }$ is a finite fragment of ZF, and weakening makes every translated-axiom and interpretation-obligation derivation a $\mathrm{\Gamma }$-proof. For empty $\mathrm{\Delta }$, only the ZF axiom occurrences in the fixed interpretation-obligation derivations remain.

Give the finite source theory $\mathrm{\Delta }$ the restricted target certificates and the interpretation of step 1.1. The lookup in its finite list of translated axiom proofs is effective. F4 therefore translates every finite $\mathrm{\Delta }$-derivation into a $\mathrm{\Gamma }$-derivation of its guarded $L$-translation. More generally, dispatching axiom lines as in step 4.1 and logical lines by F4 yields one PA-verified primitive-recursive translator for arbitrary certified $\mathrm{Z}\mathrm{F}\mathrm{C}+\mathrm{G}\mathrm{C}\mathrm{H}$ proofs. This proves both the stated finite-fragment result and the uniform formalized clause, without a transitive-model assumption.