Completeness for explicitly countable set languages

If $T$ is consistent, use F1 and F2 to form a quotient model $M_H\models H\supseteq T$. Its reduct to the original language satisfies $T$ by F6 and has the same nonempty carrier.

Let $q$ be the closed-term injection from F5. For each quotient class $b$, define $j(b)=\min \{q(t):[t]=b\}$. The set minimized is nonempty because $b$ is a class of a closed term. Equal values of $j$ name the same term by injectivity of $q$, hence the same class. Thus $j$ injects the carrier into $\omega$, with no choice of a family of representatives.

If $T\models \sigma$ but $T⊬\sigma$, F3 makes $T\cup \{\mathrm{\neg }\sigma \}$ consistent. Steps 1.1–2.1 supply a model of this theory, which satisfies $T$ and falsifies $\sigma$, a contradiction. Thus semantic consequence implies provability. Conversely F4 gives $T⊢\sigma \Rightarrow T\models \sigma$, even if $T$ has no model.