We have $T=\mbox{Cn}\tau$ where, in fact, $\tau\in T$ . Then $T$ is effectively enumerable (Corollary 26I). The complement of $T$ consists of sentences $\sigma$ that are false in some finite model $\mathfrak{A}_{\sigma}$ of $T$ , but $\mathfrak{A}\in\mbox{Mod}T=\mbox{Mod}\mbox{Th}\mbox{Mod}\tau=\mbox{Mod}\tau$ iff $\mathfrak{A}$ is a model of $\tau$ . Therefore, by Theorem 26C, for every finite model $\mathfrak{A}$ we can decide whether $\tau$ and $\sigma$ are in $\mbox{Th}\mathfrak{A}$ , and if it is found that $\tau$ is in $\mbox{Th}\mathfrak{A}$ but $\sigma$ is not, then $\sigma\notin T$ . Given that we can effectively enumerate all finite models (in a finite language), we have a semi-decision procedure for the complement of $T$ as well.