Editing Gödel's completeness theorem (section)

===More general form===

The theorem can be expressed more generally in terms of [[logical consequence]].  We say that a sentence ''s'' is a ''syntactic consequence'' of a theory ''T'', denoted <math>T\vdash s</math>, if ''s'' is provable from ''T'' in our deductive system.  We say that ''s'' is a ''semantic consequence'' of ''T'', denoted <math>T\models s</math>, if ''s'' holds in every [[model (mathematical logic)|model]] of ''T''.  The completeness theorem then says that for any first-order theory ''T'' with a [[well-order]]able language, and any sentence ''s'' in the language of ''T'',

{{block indent|if <math>T\models s</math>, then <math>T\vdash s</math>.}}

Since the converse (soundness) also holds, it follows that <math>T\models s</math> [[if and only if]] <math>T\vdash s</math>, and thus that syntactic and semantic consequence are equivalent for first-order logic.

This more general theorem is used implicitly, for example, when a sentence is shown to be provable from the axioms of [[group theory]] by considering an arbitrary group and showing that the sentence is satisfied by that group.

Gödel's original formulation is deduced by taking the particular case of a theory without any axiom.