Finite-stage L histories and weak limit-level absoluteness

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.