structural:scholar_edition, stylistic:style_transfer
Model existence theorem

The completeness theorem can also be understood in terms of consistency, as a consequence of Henkin's model existence theorem. We say that a theory T is syntactically consistent if there is no sentence s such that both s and its negation ¬ s are provable from T in our deductive system. The model existence theorem says that for any first-order theory T with a well-orderable language,

Another version, with connections to the Löwenheim–Skolem theorem, says:

Given Henkin's theorem, the completeness theorem can be proved as follows: If T ⊨ s {\displaystyle T\models s}, then T ∪ ¬ s {\displaystyle T\cup \lnot s} does not have models. By the contrapositive of Henkin's theorem, then T ∪ ¬ s {\displaystyle T\cup \lnot s} is syntactically inconsistent. So a contradiction (⊥ {\displaystyle \bot }) is provable from T ∪ ¬ s {\displaystyle T\cup \lnot s} in the deductive system. Hence (T ∪ ¬ s) ⊢ ⊥ {\displaystyle (T\cup \lnot s)\vdash \bot }, and then by the properties of the deductive system, T ⊢ s {\displaystyle T\vdash s}.