Editing Gödel's completeness theorem (section)

==Statement==

We first fix a deductive system of first-order predicate calculus, choosing any of the well-known equivalent systems.  Gödel's original proof assumed the Hilbert-Ackermann proof system.

===Gödel's original formulation===

The completeness theorem says that if a formula is logically valid then there is a finite deduction (a formal proof) of the formula.

Thus, the deductive system is "complete" in the sense that no additional inference rules are required to prove all the logically valid formulae. A converse to completeness is ''[[soundness theorem|soundness]]'', the fact that only logically valid formulae are provable in the deductive system. Together with soundness (whose verification is easy), this theorem implies that a formula is logically valid [[if and only if]] it is the conclusion of a formal deduction.

===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.

===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>.

===As a theorem of arithmetic===

The model existence theorem and its proof can be formalized in the framework of [[Peano arithmetic]]. Precisely, we can systematically define a model of any consistent effective first-order theory ''T'' in Peano arithmetic by interpreting each symbol of ''T'' by an arithmetical formula whose free variables are the arguments of the symbol. (In many cases, we will need to assume, as a hypothesis of the construction, that ''T'' is consistent, since Peano arithmetic may not prove that fact.) However, the definition expressed by this formula is not recursive (but is, in general, [[arithmetical hierarchy#The arithmetical hierarchy of sets of natural numbers|Δ<sub>2</sub>]]).