Canonical Skolem hulls in constructible levels

Work in ZF. Fix a nonzero limit ordinal $\alpha$, put $S=L_{\alpha }$, and let $A\subseteq S$. The levels are those of The constructible hierarchy and constructible rank. Fix an enumeration $({\phi }_i(y,v_0,\dots ,v_{k_i-1}){)}_{i<\omega }$ of all membership formulas with a distinguished witness variable, allowing unused parameter variables and $k_i=0$. Satisfaction refers to the set structure $(S,\in )$, as constructed in Existence and uniqueness of set satisfaction; it is never truth in the class $L$.

Let ${<}_L$ be the fixed order in The canonical definable global well-order of L. For $a\in S^{k_i}$ let $f_i(a)$ be the ${<}_L$-least $b\in S$ satisfying ${\phi }_i(b,a)$ if a witness exists, and the ${<}_L$-least member of $S$ otherwise. This default is available because $\alpha \mathrm{\ne }0$ implies $\mathrm{\varnothing }\in S$. Define

$H_0=A,H_{n+1}=H_n\cup \{f_i(a):i<\omega ,a\in H_n^{k_i}\},{\mathrm{Hull}}^{L_{\alpha }}(A)={\bigcup }_{n<\omega }{H}_n\mathrm{.}$

In particular, $H_n^0$ contains the empty tuple even when $H_n$ is empty: parameter-free witnesses enter at stage one. The enumeration, default and least-witness rule are fixed; no family of arbitrary choices is implicit. Canonical L-hulls are elementary and small ↗ supplies set existence, elementarity and size. The finite-tuple convention agrees with Finite-tuple satisfaction is absolute when its transitive-ZF-model hypothesis holds; that hypothesis is not being asserted of $S$.