Canonical countable Lindenbaum–Henkin construction

Start with $L_0=L\cup \{c_{\ast }\}$ and $T_0=T$, consistent in $L_0$ by F2. For each round $n$, F1 provides a fixed exhaustive sequence $({\sigma }_{n,k}{)}_{k<\omega }$ of $L_n$-sentences. Reserve a distinct constant $c_{n,k}$ for each index $k$, disjoint from $L_n$. Let $L_{n+1}$ include all these constants, and regard $T_n$ in this pure expansion; it remains consistent by F6.

In round $n$ put $U_0=T_n$. At index $k$ put $V_k=U_k\cup \{{\sigma }_{n,k}\}$ if this is consistent, and $V_k=U_k\cup \{\mathrm{\neg }{\sigma }_{n,k}\}$ otherwise. F3 makes $V_k$ consistent. If ${\sigma }_{n,k}=\mathrm{\exists }x\varphi$, put $U_{k+1}=V_k\cup \{\mathrm{\exists }x\varphi \to \varphi [c_{n,k}\mathrm{/}x]\}$; otherwise put $U_{k+1}=V_k$. The new constant occurs in neither $V_k$ nor the matrix, since only earlier indices have been used and every enumerated sentence belongs to $L_n$. F2 gives consistency in the one-constant extension, and F6 gives it in the whole $L_{n+1}$. Thus each $U_k$ is consistent.

The test “has no finite proof of bottom” is a set-theoretic predicate, so the successor rule in step 2.1 is a definable function, even when not computable. Encode its state by the index and the current subset of the potential sentence set; define any unused malformed-state transition to a fixed state. F5 then supplies the inner sequence, and F4 makes $T_{n+1}={\bigcup }_k{U}_k$ consistent. The outer round operation is likewise definable on a set of language/theory states, so F5 supplies all rounds. No arbitrary choice of enumerations or of consistent sides is made.

Put $L_{\mathrm{\infty }}={\bigcup }_n{L}_n$ and $U={\bigcup }_n{T}_n$. Each $T_n$ remains consistent in $L_{\mathrm{\infty }}$ by F6, so F4 gives consistency of $U$. Every finite formula in $L_{\mathrm{\infty }}$ lies in some $L_n$ by F1. Round $n$ therefore decides each such sentence and supplies a witness axiom for every such existential sentence. Repeated enumeration entries do no harm: each index has its own fresh constant.

Let $H=\{\sigma \in \mathrm{Sent}(L_{\mathrm{\infty }}):U⊢\sigma \}$. This is a set by Separation. If $H$ proved bottom, finite support would use finitely many members of $H$; replace them by their finite $U$-proofs using F4 to contradict consistency of $U$. The same composition shows that every sentence consequence of $H$ already belongs to $H$. It contains $U$, all decisions and all witness axioms from step 4.1, and the seed is a closed term. F1 injects the union alphabet and syntax into $\omega$. Thus $H$ has every asserted property in ZF.