Compactness for explicitly countable languages

If $M\models T$, the same $M$ satisfies every subset, in particular every finite subset. Conversely suppose each finite subset of $T$ has a model. Any proof of bottom from $T$ would have finite support $T_0$ by F2; its model would contradict F3. Thus $T$ is consistent and F1 supplies an at most countable nonempty model. This also handles $T=\mathrm{\varnothing }$: the finite-subset hypothesis then concerns that empty theory itself.

If $T\models \sigma$, F1 gives a finite proof $T⊢\sigma$. F2 supplies its finite assumption set $T_0\subseteq T$, with $T_0⊢\sigma$. F3 then gives $T_0\models \sigma$. The support can be empty when $\sigma$ is logically provable. No selection of models for all finite subsets was needed in step 1.1: a single alleged proof would call for only one model.