Parallel Henkinization for arbitrary set languages

First embed $L$ into a disjoint tagged copy, so that further tags cannot collide with original symbols. Adjoin one distinguished seed constant to get $L_0$. Given $L_n$, introduce a different constant $c_{n,E}$ for each existential $L_n$-sentence $E=\mathrm{\exists }x\varphi$, and put $L_{n+1}=L_n\cup \{c_{n,E}:E\text{ as above}\}$. These are sets since finite strings on a set form a set; tagging by $(n,E)$ is injective. Let $H_n$ be all sentences $E\to \varphi [c_{n,E}\mathrm{/}x]$. Set $L_{\mathrm{\infty }}={\bigcup }_{n<\omega }{L}_n$ and $T_H=T\cup {\bigcup }_{n<\omega }{H}_n$. The stage recursion uses uniquely specified sets, not choices of an enumeration.

Fix a finite subset $K$ of the added axioms, and list it in nondecreasing stage order, ordering each finite same-stage block arbitrarily. Starting from $T$, first use F1 to allow all constants of $L_{\mathrm{\infty }}$ except the finitely many designated witness constants in this list. This is a consistent pure expansion. When adding an axiom at stage $n$, its designated constant occurs neither in $T$, nor in an earlier-stage axiom, nor in the matrix of any other axiom at stage $n$: those matrices are in $L_n$, whereas the new constants were introduced in $L_{n+1}$. It is therefore fresh in the current theory and its matrix. F2 adjoins it with its axiom preserving consistency. After finitely many additions every axiom of $K$ has been added and the language is $L_{\mathrm{\infty }}$. Thus $T\cup K$ is consistent in the union language.

If $T_H$ were inconsistent, F3 would give a finite proof using only finitely many axioms from the sets $H_n$. These form a finite $K$ as in step 2.1, contradicting its consistency. Hence $T_H$ is consistent. Every existential $L_{\mathrm{\infty }}$-sentence uses finitely many symbols, each introduced at some finite stage; the maximum of those finitely many stages places the sentence in some $L_n$. Its witness axiom is then in $H_n\subseteq T_H$. The seed ensures a closed term even when the original language has no constants, and the empty finite set of new axioms is covered by F1. QED.