Solution (source code)

= Solution

Suppose first that $M\models T$. By the <soundness theorem for first-order logic>, every theorem of $T$ is true in $M$. A contradiction cannot be true in a structure, so $T$ is consistent.

Conversely, the <Godel completeness theorem> says that every semantically valid consequence is derivable. Its equivalent model-existence form says directly that every consistent first-order theory has a model. Hence
$$
\boxed{T\text{ is consistent}\quad\Longleftrightarrow\quad T\text{ has a model}.}
$$