Editing Gödel's completeness theorem (section)

===Model existence theorem===

The completeness theorem can also be understood in terms of [[consistency]], as a consequence of Henkin's [[Consistency#Henkin's theorem|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,

{{block indent|if <math>T</math> is syntactically consistent, then <math>T</math> has a model.}}

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

{{block indent|Every syntactically consistent, [[countable]] first-order theory has a finite or countable model.}}

Given Henkin's theorem, the completeness theorem can be proved as follows: If <math>T \models s</math>, then <math>T\cup\lnot s</math> does not have models. By the contrapositive of Henkin's theorem, then <math>T\cup\lnot s</math> is syntactically inconsistent. So a contradiction (<math>\bot</math>) is provable from <math>T\cup\lnot s</math> in the deductive system. Hence <math>(T\cup\lnot s) \vdash \bot</math>, and then by the properties of the deductive system, <math>T\vdash s</math>.