Well-ordered language completeness with a size bound

Use A1 and F6 to fix a well-order of the original alphabet and enough coding bijections. An alphabet of size at most $\kappa$ has at most $\kappa$ finite words: for each positive finite $r$, iterate $\kappa \cdot \kappa =\kappa$ from F7 to bound words of length $r$, include the one empty word, then use $\omega \cdot \kappa =\kappa$ from F7 for their union. One can fix one pairing bijection of ${\kappa }^2$ with $\kappa$ and iterate it, with a length tag, so all these bounds are uniform. The countable variables and finite punctuation are absorbed as well. Reserve constants $c_{\ast }$ and $c_{n,\alpha }$ for $n<\omega$, $\alpha <\kappa$. Their total set has size at most $\kappa$ by F7 and is disjoint from $L$.

Begin with the seed expansion and $T_0=T$. For round $n$, let $L_n$ contain $L$, the seed and the earlier constant layers. Use the fixed word codes to enumerate its sentences in a $\kappa$-sequence: at a code that is not a sentence use the fixed sentence $\mathrm{\exists }x(x=x)$. Every sentence occurs. In $L_{n+1}$ start with $U_0=T_n$; at each $\alpha <\kappa$ decide the enumerated ${\sigma }_{\alpha }$ by F2, then, if it is existential, add its implication witness axiom with $c_{n,\alpha }$. The constant is absent from the current assumptions: all decisions are in $L_n$ and earlier witness axioms use only earlier indices. F1 and F8 preserve consistency in the full $L_{n+1}$. At each nonzero limit $\lambda \le \kappa$ take the union of the earlier theories; F3 gives consistency. Set $T_{n+1}=U_{\kappa }$.

Each successor decision is determined by the predicate of syntactic consistency on a set of proof codes, and each limit is a specified union. F5 therefore supplies the inner $\kappa$-recursion, and then the outer $\omega$-recursion. These are definable operations; extend them arbitrarily on invalid histories to make a total recursion rule. Every language and theory is a set of words in the fixed potential alphabet of step 1.1, so the required set bounds hold. No regularity of $\kappa$ is required: a finite proof at any limit draws its support from one earlier stage of that increasing chain.

Let $U={\bigcup }_n{T}_n$ in $L_{\mathrm{\infty }}={\bigcup }_n{L}_n$. By F8 each earlier theory is consistent in this final constant expansion; F3 therefore gives consistency of $U$. Every final sentence lies in some $L_n$, since it uses finitely many constant layers, and is decided in that round. Every final existential sentence likewise has its witness axiom there. Take all sentence consequences of $U$ as $H$. If $H$ proved bottom, F3 would replace the finitely many used sentence consequences by their $U$-proofs, contradicting consistency. The same argument proves deductive closure. Thus $H$ has all the hypotheses of F4, and its quotient satisfies $H$ and hence, on reduct, $T$.

All closed terms inject into the word-code set of size $\kappa$. Assign each quotient class its least ordinal term code; this is defined for every nonempty class and is injective, just as equal least codes identify the same term. Thus the model has size at most $\kappa$ and is nonempty by the seed. Finally, finite satisfiability rules out a finite-support proof of bottom by F9; hence it gives consistency and the preceding construction applies. AC was assumed in step 1.1 to fix well-orders/coding data, and is retained as an explicit hypothesis of the theorem; this does not assert an arbitrary-language compactness theorem over ZF alone.