Condensation, GCH, and Diamond in L

Each $f_i$ is a set function: its graph is obtained by Separation from $L_{\alpha }^{k_i}\times L_{\alpha }$, using the set satisfaction relation and the set well-order in F1. The joint evaluation relation is a set as well, since the formula indices and finite tuples form a set. Replacement therefore forms the successor closure of any subset of $L_{\alpha }$. F2 on $\omega$ gives the unique stage sequence; Union gives $H\subseteq L_{\alpha }$.

Every finite tuple from $H$ belongs to some common $H_n$: take the maximum of the finitely many first-entry stages. Thus its image under any $f_i$ lies in $H_{n+1}$. The zero-arity case puts a witness for $y=y$ in $H_1$ even if $A=\mathrm{\varnothing }$. Hence $H$ is nonempty and closed under all the specified functions.

Every element of H is the value of a finite term formed from the operation symbols $f_i$ and constants naming members of A. Indeed constants give $H_0$, and an element entering $H_{n+1}$ is an operation on finitely many earlier terms; conversely every term has finite depth and its value is in that stage of the closure. Nullary symbols are terms without seed constants.

Prove agreement of satisfaction by induction on formulas. Atoms agree since H carries the restricted membership relation. Negation and conjunction preserve agreement. If $L_{\alpha }\models \mathrm{\exists }y\psi (y,a)$ with $a$ in H, the corresponding function gives $b\in H$ with $L_{\alpha }\models \psi (b,a)$; the induction hypothesis makes this true in H. Conversely a witness in H satisfies the same subformula in $L_{\alpha }$ by that hypothesis. These two directions complete the existential step, hence prove elementarity for all formulas.

If A is infinite and well-orderable, fix one bijection between A and its cardinal $\kappa$ from F3. If A is finite fix a finite enumeration and put $\kappa =\omega$. In either case the alphabet consisting of parentheses, countably many operation symbols and seed labels injects into $\kappa$. Fix one bijection $\kappa \times \kappa \to \kappa$ using F4. Its iterates encode finite strings of each length; encoding the length together with the iterated value encodes all finite strings in $\kappa$. This uses one fixed bijection and ordinary recursion, not countably many choices. The set of valid terms therefore injects into $\kappa$.

Assign to $x\in H$ the least code of a term evaluating to x. Such a code exists by step 2.2, and distinct values have distinct least codes. This injects H into $\kappa$ and gives a well-order of H. For infinite A the inclusion $A\subseteq H$ supplies the opposite cardinal bound, so $\mathrm{\mid }H\mathrm{\mid }=\mathrm{\mid }A\mathrm{\mid }$. For finite A, step 3.1 implies H contains every natural number: zero is the unique empty set in the transitive level, and from n its unique ordinal successor in that level is obtained by the successor-defining formula. All finite ordinals belong to every nonzero limit L level. Thus $\omega \subseteq H$, and the upper bound makes H countably infinite. No AC is used in either case.

Fix the sentinel numerical coding from F1. Let the total external enumeration $\nu (e)$ first unpair $e$ as $(f,n)$, deterministically decode $f$ to a finite word $w$, and accept it exactly when the finite parse trace ends in a formula and its free-variable set is contained in $\{0,\dots ,n\}$. On an invalid input return the fixed pair $(v_0=v_0,0)$. The formula $\mathrm{Enum}(e,w,n)$ says that the finite unpairing, decoding, parse and free-variable trace has that output. Induction over the trace proves existence, uniqueness, soundness and completeness. Every trace and every competing trace is hereditarily finite, so the same induction proves absoluteness in each transitive domain containing all hereditarily finite sets.

Suppose $A\mathrm{\ne }\mathrm{\varnothing }$. Choose a finite assignment length $m$ strictly above $n$ and every variable index occurring in $w$. Let $U$ be exactly the set of graph-coded functions $m\to A$. On the distinct subformulas in the canonical closing-order parse trace, form a graph $T$ of truth subsets of $U$: equality and membership read coordinates, negation takes complement in $U$, conjunction takes intersection, and an existential in coordinate $i$ uses assignments obtained by replacing exactly coordinate $i$. Induction in the finite child-before-parent order proves that any such table is unique and agrees with satisfaction. It also proves coincidence: changing coordinates not free in a subformula does not change its truth row. Thus shifting the tuple $a\in A^n$ to coordinates $1,\dots ,n$, reserving coordinate zero for $x$, and existentially padding the remaining coordinates defines a unique $b=\{x\in A:(A,\in )\models w[x,a]\}$.

Define $\mathrm{Decode}$ by exactly two disjoint branches. If $A=\mathrm{\varnothing }$, require the designated empty code, the empty tuple and the empty output. If $A\mathrm{\ne }\mathrm{\varnothing }$, require $\mathrm{Enum}(e,w,n)$ and the construction of step 1.2. Enum uniqueness, table uniqueness and coincidence make this relation single-valued. In the nonempty branch its range consists of exactly the definitions in F4, since every allowed formula/arity pair has a numerical code and unused parameters are permitted. The empty branch gives exactly the special value in F4; it is not inferred from satisfaction on an empty structure.

The formulas checking the finite parse, assignment and table graphs are fixed pure-membership formulas. If $A\in L_{\eta }$ and $\eta$ is infinite, an $m$-assignment into $A$ belongs to $L_{\eta +3}$: its Kuratowski-pair entries cost two successor stages and the finite graph one. The exact assignment set is definable over that level and lies in $L_{\eta +4}$. For each fixed subformula its truth row is defined directly over the same containing level by the relativization in F3, rather than one Def step per syntactic node. Pairing the finitely many words with their rows and collecting the table costs at most three more stages. All parse and Enum traces are hereditarily finite, so they add no stage above an infinite base. Hence every needed certificate and decoded subset appears after a fixed finite overhead.

For finite $r$, induction gives $L_r=V_r$: every subset of the finite set $V_r$ is finite and is definable using its members as parameters. Therefore $L_{\omega }=V_{\omega }$. Every particular syntax trace, finite assignment table, decoded subset and finite initial history is hereditarily finite, so all of them belong to $L_{\omega }$ even though no one stage contains codes of every finite size. An inductive set would contain every finite ordinal and hence would not be hereditarily finite; therefore $L_{\omega }$ does not satisfy Infinity.

Let $W$ be the fixed finite sentence asserting Empty Set, Pairing and Union, the Enum trace clauses, the existence and exactness of the assignment and truth tables for every nonempty carrier, and both branches of Decode. For a nonzero limit $\lambda >\omega$, any finite tuple of parameters lies in some infinite $L_{\eta }$ with $\eta <\lambda$; step 2.2 places the witnesses below $\lambda$. Step 3.1 handles $\lambda =\omega$. Thus every nonzero limit $L_{\lambda }$ satisfies $W$. If a transitive $N$ satisfies $W$, all its accepted finite traces are actual by step 1.1, all actual finite assignments occur in its exact $U$, and induction through the accepted table proves its Decode relation is the external one. Consequently whenever $N$ recognizes a supplied $B$ as the decoded range over $A$, $B=\mathrm{Def}(A)$ externally.

Let $\mathrm{Hist}(h,\gamma )$ say that $h$ is a function on $\gamma +1$, starts with the empty set, takes the decoded range at successors, and at limits takes the union of its earlier values. In any transitive model of $W$, external induction on the supplied history identifies its value at $\delta$ with the actual $L_{\delta }$; this uses step 4.1 at successors and bounded membership at limits. It assumes no internal recursion theorem.

Prove $H_{\gamma }\in L_{\gamma +8}$ by external induction. At finite $\gamma$ it is hereditarily finite by step 3.1. If $\gamma =\delta +1$, the inductive $H_{\delta }$ is in $L_{\delta +8}$, while $⟨\delta +1,L_{\delta +1}⟩$ is in $L_{\delta +4}$; one definition over $L_{\delta +8}$ appends it and gives $H_{\gamma }$ in $L_{\delta +9}=L_{\gamma +8}$. At an infinite limit $\lambda$, define the strict prefix over $L_{\lambda }$ by the existence of an accepted shorter history with the displayed terminal value. All true shorter histories already belong to $L_{\lambda }$, and step 5.1 excludes false ones. The prefix lies in $L_{\lambda +1}$; pairing and appending $⟨\lambda ,L_{\lambda }⟩$ puts $H_{\lambda }$ in $L_{\lambda +4}$.

Augment histories by relations. At a successor retain the earlier order, place every old member before every new one, and order new members by their least Decode code: first the same numerical $e$ from Enum, then the parameter tuples lexicographically at the fixed allowed arity. Step 2.1 gives the exact decoding fibres, including unused parameters and the designated empty case; F6 gives their unique least elements. At limits take unions. Simultaneous external induction proves every accepted augmented history has the actual levels and exactly this actual relation. By F7 it is the published ${<}_L$, not merely an isomorphic well-order.

Let $C$ conjoin $W$ with: every ordinal has its ordinal successor; every ordinal has a Hist witness; and every set belongs to a value on such a history. Step 6.1 and level exhaustion show that every nonzero limit $L_{\lambda }$ satisfies $C$. Conversely let nonempty transitive $N$ satisfy $C$ and put $\beta =N\cap \mathrm{Ord}$. Empty-set existence makes $\beta$ nonzero, and successor closure makes it a limit. Steps 4.1 and 5.1 show that every internal history is actual, so $L_{\delta }\in N$ for every $\delta <\beta$ and hence $L_{\beta }\subseteq N$. Exhaustion gives the reverse inclusion. Therefore $N=L_{\beta }$.

For finite $\gamma$, the order and history are hereditarily finite. At an infinite successor, define $R_{\delta +1}$ over $L_{\delta +32}$ from $R_{\delta }$ and the two levels. Step 2.2 places every relevant finite table far below this bound, and step 6.2 makes minimization exact, so $R_{\delta +1}\in L_{\delta +33}$. The two nested pairs in the new augmented history entry lie below $L_{\delta +40}$; one definition appends them, giving $K_{\delta +1}\in L_{\delta +41}$. At an infinite limit, define the strict augmented prefix over $L_{\lambda }$ from accepted shorter histories; step 6.2 excludes false witnesses. Its union order is in $L_{\lambda +1}$ and finite pairing places the appended history below $L_{\lambda +6}$. Thus the stated $+32$ and $+40$ bounds hold.

Define $\chi (x,y)$ to mean that some accepted augmented history contains $⟨x,y⟩$ in its terminal order. Steps 6.2 and 7.2 show in ambient ZF that this is exactly $x{<}_{L}y$. In a nonzero limit $L_{\lambda }$, every required shorter augmented history is present by step 7.2; conversely its transitivity, $W$, and step 6.2 make every internally accepted history actual. Therefore the interpretation of this very formula $\chi$ in $L_{\lambda }$ is precisely ${<}_L\upharpoonright L_{\lambda }$. This proves agreement of least codes as well as agreement on already selected elements, without applying full-ZF absoluteness to the weak level.

Expand the proof used in F1 into the fixed first-order formulas named in the Given. Its induction says simultaneously that, for every internal ordinal $\alpha$, the internally constructed history through $\alpha$ is the actual history and hence $(L_{\alpha }{)}^M=L_{\alpha }$. At a successor, finite satisfaction over the transitive set $L_{\beta }$ is absolute, so the two definable-subset operations agree. At a limit, transitivity gives exactly the actual earlier indices and union gives exactly their union. The proof uses only finitely many instances of Separation, Replacement and Foundation, together with finitely many of the remaining ZF axioms. By F2, let $K_0$ be the exact finite set of ZF axiom sentences occurring in this expanded derivation. Thus the comparison holds for every transitive $K_0$-model; no occurrence of the hypothesis "model of ZF" remains unexpanded.

Add to $K_0$ the finitely many axiom occurrences in the fixed proofs that Infinity supplies an internal nonzero limit ordinal, that the ordinals of a nonempty transitive set form an ordinal with no largest member, and that the fixed formula $x\in L$ is equivalent internally to membership in some level of its hierarchy. Call the resulting finite fragment $K_L$. If $M$ is a transitive $K_L$-model and ${\delta }_M=\mathrm{Ord}\cap M$, these fixed proofs make ${\delta }_M$ a nonzero limit ordinal and give $L^M={\bigcup }_{\alpha <{\delta }_M}(L_{\alpha }{)}^M$. By step 1.1 every summand is the actual $L_{\alpha }$. Each such level is an element of $M$, and transitivity puts all of its elements in $M$. Therefore $L^M=L_{{\delta }_M}\subseteq M$.

Suppose $M\subseteq N$ are transitive $K_L$-models with the same ordinals. Then ${\delta }_M={\delta }_N$, so step 2.1 gives $L^M=L_{{\delta }_M}=L_{{\delta }_N}=L^N\subseteq M$.

If $x\in N\setminus M$, step 3.1 gives $x\mathrm{\notin }{L}^N$. Since $x$ is an element of the universe of $N$ but is not internally constructible there, $N\models V\mathrm{\ne }L$. This last implication uses the fixed internal formula for $x\in L$ and does not compare $L^N$ with constructible levels above the common ordinal height.

By F1, $(L_{\alpha },\in )\models C$. Since $X\prec L_{\alpha }$, also $(X,\in )\models C$. F2 makes $\pi$ an isomorphism from $(X,\in )$ to the transitive set $(M,\in )$, so $M\models C$. In particular $M$ is nonempty; no assertion that $L_{\alpha }$ or $M$ satisfies Infinity, Power Set, Replacement, Separation, or Choice has been used.

Put $\beta =M\cap \mathrm{Ord}$. The converse direction of F1 applies directly to the nonempty transitive set $M$ satisfying $C$ and yields $M=L_{\beta }$. This includes the boundary $\alpha =\omega$: the supplier proves $L_{\omega }=V_{\omega }$, verifies $C$ there by finite certificates, and explicitly does not infer Infinity.

F3 applied to this collapse fixes each transitive $A\subseteq X$ pointwise. It also gives $\pi (\xi )=\mathrm{otp}(X\cap \xi )$ for every actual ordinal $\xi \in X$, and gives $\pi (\xi )=X\cap \xi$ when that intersection is transitive. These conclusions do not require $X$ itself to be transitive, and the empty transitive part is fixed vacuously.

The order from F2 restricts to a well-order of $L_{\alpha }$. F5 gives the injection $\alpha \hookrightarrow L_{\alpha }$ by inclusion. Thus both cardinals exist and $\mathrm{\mid }\alpha \mathrm{\mid }\le \mathrm{\mid }{L}_{\alpha }\mathrm{\mid }$.

Encode descriptions by finite rooted ordered trees. A node carries a label $(\gamma ,i)$ with $\gamma <\alpha$ and i the code of a formula defining a subset of $L_{\gamma }$; its ordered children describe the finite tuple of parameters. A valid tree evaluates its children first and then takes the subset defined by that formula over the indicated level. Empty-level descriptions use the prescribed $\mathrm{Def}(\mathrm{\varnothing })=\{\mathrm{\varnothing }\}$. Each valid tree has at most one value, by uniqueness of satisfaction and of its recursively evaluated parameters.

Every $x\in L_{\alpha }$ has a valid finite description. Induct on ${\rho }_L(x)$. Choose one definition of x over $L_{\gamma }$, where $\gamma ={\rho }_L(x)<\alpha$. Each parameter has smaller constructible rank by F1 and nesting. By the induction hypothesis it has a finite description; finitely many existential choices of descriptions are provable in ZF by induction on the tuple length. Joining those finitely many finite trees under the root $(\gamma ,i)$ gives a finite description of x. The zero-parameter case is a single node, covering the first stage. This induction proves existence, without choosing definitions simultaneously for all x.

Put $\kappa =\mathrm{\mid }\alpha \mathrm{\mid }$. Fix one bijection $\alpha \to \kappa$ from F3 and one pairing bijection on $\kappa$ from F4. Encode node labels and finitely many punctuation symbols in $\kappa$. Iterating this fixed pairing and including the string length injects all finite strings, hence all the described finite trees, into $\kappa$. For a nonempty fibre of the tree-evaluation map take its least ordinal code. Step 1.2 ensures different values have disjoint fibres; step 2.1 ensures every x has a nonempty fibre. Least codes therefore give an injection $L_{\alpha }\to \kappa$.

The upper bound in step 3.1 and the lower bound in step 1.1 imply $\mathrm{\mid }{L}_{\alpha }\mathrm{\mid }=\mathrm{\mid }\alpha \mathrm{\mid }$. In particular at $\alpha =\omega$ the finite-tree codes are natural-number codes and the lower bound consists of the finite ordinals. The same code alphabet works at successor and limit ordinals alike; no family of levelwise bijections, and no AC, was used.

Put $\kappa =\mathrm{\mid }\alpha \mathrm{\mid }$ and fix a bijection from $L_{\alpha }$ to $\kappa$ using F2. Iterate one pairing bijection from F4 and encode lengths to inject all formula/finite-tuple pairs into $\kappa$. Each definable subset has a code by F1. Its least code exists; assigning that code gives an injection $\mathrm{Def}(L_{\alpha })\to \kappa$, hence a well-order and an upper bound by F3. Empty parameter tuples are among these codes.

For every $a\in L_{\alpha }$, transitivity from F5 gives $a\subseteq L_{\alpha }$; the formula $x\in a$ with the single parameter a defines exactly a over $L_{\alpha }$. Thus $L_{\alpha }\subseteq \mathrm{Def}(L_{\alpha })$, providing a lower bound of $\kappa$ by F2.

Both sets are well-orderable by step 1.1 and F2. The upper and lower bounds therefore give $\mathrm{\mid }\mathrm{Def}(L_{\alpha })\mathrm{\mid }=\kappa =\mathrm{\mid }\alpha \mathrm{\mid }$. The only selections in the proof were one bijection for the already well-orderable level and one cardinal pairing; least codes supply all subset representatives without AC.

Choose a nonzero limit $\theta$ large enough that $x,\kappa ,L_{\kappa }$ and the relevant finite seed belong to $L_{\theta }$; this is possible because $x$ is constructible and the $L$-levels are nested and exhaustive for $L$. For the first clause set $A=\kappa \cup \{\kappa ,x\}$, and for the second set $A=L_{\kappa }\cup \{L_{\kappa },\kappa ,x\}$. Each seed is a subset of $L_{\theta }$. In the first case $\mathrm{\mid }A\mathrm{\mid }=\kappa$ because $\kappa$ is infinite; in the second F4 gives the same conclusion. Both seeds are well-orderable.

Let $H={\mathrm{Hull}}^{L_{\theta }}(A)$. By F1, $H\prec L_{\theta }$ and $H$ is well-orderable with $\mathrm{\mid }H\mathrm{\mid }=\kappa$. Collapse $H$ to $M$. By F2 there is an ordinal $\beta$ with $M=L_{\beta }$. Since $\beta =\mathrm{Ord}\cap M\subseteq M$ and the collapse bijects $H$ with $M$, there is an injection $\beta \to \kappa$; F5 therefore gives $\beta <{\kappa }^{+}$.

In the first case, $\kappa \subseteq A\subseteq H$, so F3 fixes every ordinal below $\kappa$. Since $x\in H$ and $x\subseteq \kappa$, the recursive collapse equation gives $\pi (x)=\{\pi (\xi ):\xi \in x\}=x$. Thus $x\in M=L_{\beta }$. In the second case, $L_{\kappa }\subseteq H$ is transitive by F6, so F3 fixes it pointwise; again $x\in H$ and $x\subseteq L_{\kappa }$ imply $\pi (x)=x$, whence $x\in L_{\beta }$.

We have proved the general clause with $\beta <{\kappa }^{+}$. For the first clause, nesting gives $L_{\beta }\subseteq L_{{\kappa }^{+}}$, so $x\in L_{{\kappa }^{+}}$. The case $x=\mathrm{\varnothing }$ is included, and no selection from a family of sets occurred: the hull is canonical and the cardinal bound uses only the Hartogs successor.

Work inside $L$. By F1 it satisfies ZF and thinks $V=L$; by F2 it also satisfies A1. Fix an infinite internal cardinal $\kappa$, and write $\lambda =({\kappa }^{+}{)}^L$. Every $p\in {\mathcal{P}}^L(\kappa )$ is internally constructible, so the internal instance of F3 gives $p\in L_{\lambda }$. Thus inclusion is an injection ${\mathcal{P}}^L(\kappa )\hookrightarrow L_{\lambda }$.

Since $\lambda$ is an infinite ordinal, internal F4 gives $\mathrm{\mid }{L}_{\lambda }{\mathrm{\mid }}^L=\mathrm{\mid }\lambda {\mathrm{\mid }}^L=\lambda$. Hence $(2^{\kappa }{)}^L=\mathrm{\mid }{\mathcal{P}}^L(\kappa ){\mathrm{\mid }}^L\le \lambda$. On the other hand F5, applied under internal AC, gives $\kappa <(2^{\kappa }{)}^L$. By the defining minimality of the successor cardinal $\lambda$, this implies $\lambda \le (2^{\kappa }{)}^L$. Therefore $(2^{\kappa }{)}^L=\lambda =({\kappa }^{+}{)}^L$.

The argument applies to every infinite cardinal of $L$, so $L\models \mathrm{G}\mathrm{C}\mathrm{H}$, while F2 also gives $L\models \mathrm{A}\mathrm{C}$. If $V=L$, internal and ambient sets, cardinals, power sets, and successors coincide, yielding $\mathrm{A}\mathrm{C}+\mathrm{G}\mathrm{C}\mathrm{H}$ in $V$. No claim that ambient ZF alone well-orders arbitrary ambient power sets was used.

Define $(S_{\alpha }{)}_{\alpha <{\omega }_1}$ by F6. Having defined the earlier guesses, call $(B,D)$ bad at $\alpha$ when $B\subseteq \alpha$, $D\subseteq \alpha$ is club in $\alpha$, and $S_{\xi }\mathrm{\ne }B\cap \xi$ for every $\xi \in D$. If a bad pair exists, take the $\chi$-least ordered pair and set $S_{\alpha }=B$; otherwise set $S_{\alpha }=\mathrm{\varnothing }$. F2 makes the choice unique and F1 makes this one fixed first-order recursion; $S_0=\mathrm{\varnothing }$, and always $S_{\alpha }\subseteq \alpha$.

Assume for contradiction that this sequence is not diamond. By F7 there are $A\subseteq {\omega }_1$ and a club $C\subseteq {\omega }_1$ such that $S_{\alpha }\mathrm{\ne }A\cap \alpha$ for every $\alpha \in C$. Among all such global failure pairs choose the $\chi$-least $(A,C)$, possible because $V=L$ and F2 well-orders $L$.

Choose a nonzero limit $\theta$ such that $L_{\theta }$ contains $S,A,C,{\omega }_1$. Because $L_{\theta }$ is a ${<}_L$-initial segment and the badness predicate has only bounded quantifiers once these parameters are fixed, it sees that $(A,C)$ is the least failure pair. Let $X$ be the canonical hull of this finite seed. F3 gives $X\prec L_{\theta }$ and makes $X$ countably infinite. Put $\delta =X\cap {\omega }_1$. Elementarity makes $X\cap {\omega }_1$ an ordinal, hence transitive, and countability gives $\delta <{\omega }_1$. For every $\xi <\delta$, elementarity applied to the unbounded set $C$ produces $c\in C\cap X$ above $\xi$; hence $C\cap \delta$ is unbounded in $\delta$. It follows that $\delta$ is a nonzero countable limit, and closure of $C$ gives $\delta \in C$.

Collapse $X$ by $\pi$ to $M=L_{\gamma }$ using F4. By F5, $\pi ({\omega }_1)=\delta$. Since every $\xi <\delta$ lies in $X$, evaluation of the function $S\in X$ puts $S_{\xi }\in X$; as $S_{\xi }\subseteq \xi$, F5 fixes it. The collapse equations therefore give $\pi (S)=S\upharpoonright \delta$, $\pi (A)=A\cap \delta$, and $\pi (C)=C\cap \delta$.

By elementarity and isomorphism, $M$ regards $(A\cap \delta ,C\cap \delta )$ as its $\chi$-least failure pair for the sequence $S\upharpoonright \delta$ on its first uncountable ordinal $\delta$. The predicates “subset of $\delta$,” “club in $\delta$,” and “fails at every member” are bounded here and are absolute between the transitive $M$ and the universe for these fixed parameters. F1 says that $M$ and the universe use the same $\chi$-order on $M$, and that $M=L_{\gamma }$ is an initial segment of that order. Therefore no ambient bad pair at $\delta$ can precede $(A\cap \delta ,C\cap \delta )$: any preceding pair would belong to $M$ and contradict internal leastness. Thus step 1.1 sets $S_{\delta }=A\cap \delta$.

But step 3.1 gives $\delta \in C$, while step 2.1 says $S_{\delta }\mathrm{\ne }A\cap \delta$ at every member of $C$. This contradicts step 5.1. Hence the sequence is diamond, and its correct-guess set meets every club for every target subset of ${\omega }_1$.

By F1, $V=L$ supplies a diamond sequence on ${\omega }_1$. By F2 and the equality $V=L$, A1 holds in the ambient universe. This explicit use of Choice is essential to the cited tree proof: it supplies its countable-union, maximal-antichain, and deterministic well-ordering steps.

Apply F3 with the diamond sequence and AC from step 1.1. The resulting tree is normal and splitting, has underlying set ${\omega }_1$, has countable levels, and has neither an uncountable antichain nor a cofinal branch; hence it is a Suslin tree. No tree is asserted at the degenerate heights zero or one, and no weakening from stationary guessing to merely unbounded guessing is made.

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.

Write the fixed target contradiction as $\mathrm{\perp }=\mathrm{\exists }{v}_0\mathrm{\neg }(v_0=v_0)$. In F1's specialized raw $D$-relativization, its guarded $L$-translation is $\mathrm{\top }\to \mathrm{\exists }{v}_0(D(v_0)\wedge \mathrm{\neg }(v_0=v_0))$, where $\mathrm{\top }$ is the fixed empty guard. Let $A(v_0)$ denote the exact fixed translation of the equality atom if a term-graph presentation is used instead; its graph witnesses express that both occurrences of $v_0$ have value $v_0$ and that those values are equal. Under $D(v_0)$, equality reflexivity and existential introduction prove $A(v_0)$, so either presentation admits the same fixed refutation block. Fix once and for all a finite ZF block which proves $\mathrm{\top }$, applies the translated conclusion, derives the negation of its existential matrix from this equality instance and quantified Boolean reasoning, and concludes the selected ZF contradiction by explosion. Such a block exists by F3 and the reflexivity axiom after the fixed formula $D$ and abbreviations are expanded. Define $r(p)$ by appending this block, with shifted line references, to the translator output of F1. List append, addition of the input proof length to finitely many fixed references, and the malformed-input default are primitive recursive. PA checks each of the finitely many new line templates and combines those checks with F1's uniform checker-acceptance proof. Hence PA proves totality and $\mathrm{\forall }p({\mathrm{Prf}}_{\mathrm{Z}\mathrm{F}\mathrm{C}+\mathrm{G}\mathrm{C}\mathrm{H}}(p,<mi\; mathvariant="normal">⌜</mi>\mathrm{\perp }<mi\; mathvariant="normal">⌝</mi>)\to {\mathrm{Prf}}_{\mathrm{Z}\mathrm{F}}(r(p),<mi\; mathvariant="normal">⌜</mi>\mathrm{\perp }<mi\; mathvariant="normal">⌝</mi>))$. This is one assertion about all proof codes, not an external selection of a new finite fragment after entering PA.

Apply F2 with $T=\mathrm{Z}\mathrm{F}$ and $U=\mathrm{Z}\mathrm{F}\mathrm{C}+\mathrm{G}\mathrm{C}\mathrm{H}$ to the map $r$. It yields $\mathrm{P}\mathrm{A}⊢\mathrm{Con}(\mathrm{Z}\mathrm{F})⟶\mathrm{Con}(\mathrm{Z}\mathrm{F}\mathrm{C}+\mathrm{G}\mathrm{C}\mathrm{H})$. Only numerical proof codes occur in this argument. In particular, neither step constructs nor assumes a set model, a well-founded model, or a transitive model of ZF.

There is a fixed finite $\mathrm{Z}\mathrm{F}\mathrm{C}+\mathrm{G}\mathrm{C}\mathrm{H}$ proof of CH: instantiate GCH at the first infinite initial ordinal and expand the selected cardinal notation. Hence appending this proof and replacing uses of the CH axiom gives a primitive-recursive map from any $\mathrm{Z}\mathrm{F}\mathrm{C}+\mathrm{C}\mathrm{H}$ refutation to a $\mathrm{Z}\mathrm{F}\mathrm{C}+\mathrm{G}\mathrm{C}\mathrm{H}$ refutation, and PA verifies the map by its finite line-prefix check. Therefore $\mathrm{Con}(\mathrm{Z}\mathrm{F}\mathrm{C}+\mathrm{G}\mathrm{C}\mathrm{H})$ implies $\mathrm{Con}(\mathrm{Z}\mathrm{F}\mathrm{C}+\mathrm{C}\mathrm{H})$.

Combining step 1.1 with F1 gives both implications from $\mathrm{Con}(\mathrm{Z}\mathrm{F})$. Separately, the inclusion of every certified ZF axiom in ZFC gives an identity-on-lines primitive-recursive map from ZF refutations to ZFC refutations. Thus PA proves $\mathrm{Con}(\mathrm{Z}\mathrm{F}\mathrm{C})\to \mathrm{Con}(\mathrm{Z}\mathrm{F})$. Composing this with the two implications already proved gives both conclusions from $\mathrm{Con}(\mathrm{Z}\mathrm{F}\mathrm{C})$ as claimed.