Skolem witness closure on a cardinal

Include in $\mathcal{H}$ every language function and constant, and the constant zero. For each formula $\mathrm{\exists }x\phi (x,\vec{y})$ with a specified finite list containing its other free variables, include $h_{\phi }(\vec{a})$ equal to the least ordinal witness in $M$ if one exists, and zero otherwise. The local structural recursion and satisfaction theorem make each displayed witness selector a set function.

Put $\mu =\max (\omega ,\mathrm{\mid }L\mathrm{\mid })<\kappa$. Finite strings over the alphabet of symbols, countably many variables and punctuation number at most $\mu$: induction from ${\mu }^2=\mu$ bounds each finite length, and recursion collects all finite lengths; the countable disjoint union has size at most $\omega \times \mu \le {\mu }^2=\mu$. Thus the formula/list pairs and the functions just included form a family of size at most $\mu$. Ambient AC suffices for these cardinal identifications.

Let nonzero alpha be closed under this family. Closure under language functions and constants makes it a substructure. Terms evaluated on parameters below alpha agree in both structures, by induction on terms. Equality and relation atoms therefore agree; induction on formulas preserves agreement under negation and conjunction. If M satisfies $\mathrm{\exists }x\phi (x,\vec{a})$, its selected witness is below alpha, and the induction hypothesis for $\phi$ proves truth in the restriction. Conversely a witness below alpha transfers to M by the same induction hypothesis. Thus every formula agrees.

The same induction proves the general witness criterion used below: any nonempty substructure in which every existential formula true in M with parameters in the substructure has some witness there is elementary. Conversely an elementary substructure has that witness property by the semantics of existential quantification.