Canonical L-hulls are elementary and small

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.