Gödel's completeness theorem is a fundamental theorem inmathematical logic that establishes a correspondence betweensemantic truth and syntacticprovability infirst-order logic.

The completeness theorem applies to any first-ordertheory: IfT is such a theory, and φ is a sentence (in the same language) and every model ofT is a model of φ, then there is a (first-order) proof of φ using the statements ofT as axioms. One sometimes says this as "anything true in all models is provable". (This does not contradictGödel's incompleteness theorem, which is about a formula φ_u that is unprovable in a certain theoryT but true in the "standard" model of the natural numbers: φ_u is false in some other, "non-standard" models ofT.^[1])

The completeness theorem makes a close link betweenmodel theory, which deals with what is true in different models, andproof theory, which studies what can be formally proven in particularformal systems.

It was first proved byKurt Gödel in 1929. It was then simplified whenLeon Henkin observed in hisPh.D. thesis that the hard part of the proof can be presented as the Model Existence Theorem (published in 1949).^[2] Henkin's proof was simplified byGisbert Hasenjaeger in 1953.^[3]

There are numerousdeductive systems for first-order logic, including systems ofnatural deduction andHilbert-style systems. Common to all deductive systems is the notion of aformal deduction. This is a sequence (or, in some cases, a finitetree) of formulae with a specially designatedconclusion. The definition of a deduction is such that it is finite and that it is possible to verifyalgorithmically (by acomputer, for example, or by hand) that a given sequence (or tree) of formulae is indeed a deduction.

A first-order formula is calledlogically valid if it is true in everystructure for the language of the formula (i.e. for any assignment of values to the variables of the formula). To formally state, and then prove, the completeness theorem, it is necessary to also define a deductive system. A deductive system is calledcomplete if every logically valid formula is the conclusion of some formal deduction, and the completeness theorem for a particular deductive system is the theorem that it is complete in this sense. Thus, in a sense, there is a different completeness theorem for each deductive system. A converse to completeness issoundness, the fact that only logically valid formulas are provable in the deductive system.

If some specific deductive system of first-order logic is sound and complete, then it is "perfect" (a formula is provable if and only if it is logically valid), thus equivalent to any other deductive system with the same quality (any proof in one system can be converted into the other).^{[citation needed]}

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.

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 issoundness, 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 validif and only if it is the conclusion of a formal deduction.

The theorem can be expressed more generally in terms oflogical consequence. We say that a sentences is asyntactic consequence of a theoryT, denoted${\displaystyle T⊢s}$, ifs is provable fromT in our deductive system. We say thats is asemantic consequence ofT, denoted${\displaystyle T\models s}$, ifs holds in everymodel ofT. The completeness theorem then says that for any first-order theoryT with awell-orderable language, and any sentences in the language ofT,

if${\displaystyle T\models s}$, then${\displaystyle T⊢s}$.

Since the converse (soundness) also holds, it follows that${\displaystyle T\models s}$if and only if${\displaystyle T⊢s}$, 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 ofgroup 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.

The completeness theorem can also be understood in terms ofconsistency, as a consequence of Henkin'smodel existence theorem. We say that a theoryT issyntactically consistent if there is no sentences such that boths and its negation ¬s are provable fromT in our deductive system. The model existence theorem says that for any first-order theoryT with a well-orderable language,

if${\displaystyle T}$ is syntactically consistent, then${\displaystyle T}$ has a model.

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

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

The model existence theorem and its proof can be formalized in the framework ofPeano arithmetic. Precisely, we can systematically define a model of any consistent effective first-order theoryT in Peano arithmetic by interpreting each symbol ofT 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, thatT is consistent, since Peano arithmetic may not prove that fact.) However, the definition expressed by this formula is not recursive (but is, in general,Δ₂).

An important consequence of the completeness theorem is that it is possible torecursively enumerate the semantic consequences of anyeffective first-order theory, by enumerating all the possible formal deductions from the axioms of the theory, and use this to produce an enumeration of their conclusions.

This comes in contrast with the direct meaning of the notion of semantic consequence, that quantifies over all structures in a particular language, which is clearly not a recursive definition.

Also, it makes the concept of "provability", and thus of "theorem", a clear concept that only depends on the chosen system of axioms of the theory, and not on the choice of a proof system.

Gödel's incompleteness theorems show that there are inherent limitations to what can be proven within any given first-order theory in mathematics. The "incompleteness" in their name refers to another meaning ofcomplete (seemodel theory – Using the compactness and completeness theorems): A theory${\displaystyle T}$ is complete (or decidable) if every sentence${\displaystyle S}$ in the language of${\displaystyle T}$ is either provable (${\displaystyle T⊢S}$) or disprovable (${\displaystyle T⊢\mathrm{\neg }S}$).

The first incompleteness theorem states that any${\displaystyle T}$ which isconsistent,effective and containsRobinson arithmetic ("Q") must be incomplete in this sense, by explicitly constructing a sentence${\displaystyle S_T}$ which is demonstrably neither provable nor disprovable within${\displaystyle T}$. The second incompleteness theorem extends this result by showing that${\displaystyle S_T}$ can be chosen so that it expresses the consistency of${\displaystyle T}$ itself.

Since${\displaystyle S_T}$ cannot be proven in${\displaystyle T}$, the completeness theorem implies the existence of a model of${\displaystyle T}$ in which${\displaystyle S_T}$ is false. In fact,${\displaystyle S_T}$ is aΠ₁ sentence, i.e. it states that some finitistic property is true of all natural numbers; so if it is false, then some natural number is a counterexample. If this counterexample existed within the standard natural numbers, its existence would disprove${\displaystyle S_T}$ within${\displaystyle T}$; but the incompleteness theorem showed this to be impossible, so the counterexample must not be a standard number, and thus any model of${\displaystyle T}$ in which${\displaystyle S_T}$ is false must includenon-standard numbers.

In fact, the model ofany theory containingQ obtained by the systematic construction of the arithmetical model existence theorem, isalways non-standard with a non-equivalent provability predicate and a non-equivalent way to interpret its own construction, so that this construction is non-recursive (as recursive definitions would be unambiguous).

Also, if${\displaystyle T}$ is at least slightly stronger thanQ (e.g. if it includes induction for bounded existential formulas), thenTennenbaum's theorem shows that it has no recursive non-standard models.

The completeness theorem and thecompactness theorem are two cornerstones of first-order logic. While neither of these theorems can be proven in a completelyeffective manner, each one can be effectively obtained from the other.

The compactness theorem says that if a formula φ is a logical consequence of a (possibly infinite) set of formulas Γ then it is a logical consequence of a finite subset of Γ. This is an immediate consequence of the completeness theorem, because only a finite number of axioms from Γ can be mentioned in a formal deduction of φ, and the soundness of the deductive system then implies φ is a logical consequence of this finite set. This proof of the compactness theorem is originally due to Gödel.

Conversely, for many deductive systems, it is possible to prove the completeness theorem as an effective consequence of the compactness theorem.

The ineffectiveness of the completeness theorem can be measured along the lines ofreverse mathematics. When considered over a countable language, the completeness and compactness theorems are equivalent to each other and equivalent to a weak form of choice known asweak Kőnig's lemma, with the equivalence provable in RCA₀ (a second-order variant ofPeano arithmetic restricted to induction over Σ⁰₁ formulas). Weak Kőnig's lemma is provable in ZF, the system ofZermelo–Fraenkel set theory without axiom of choice, and thus the completeness and compactness theorems for countable languages are provable in ZF. However the situation is different when the language is of arbitrary large cardinality since then, though the completeness and compactness theorems remain provably equivalent to each other in ZF, they are also provably equivalent to a weak form of theaxiom of choice known asthe ultrafilter lemma. In particular, no theory extending ZF can prove either the completeness or compactness theorems over arbitrary (possibly uncountable) languages without also proving the ultrafilter lemma on a set of the same cardinality.

The completeness theorem is a central property offirst-order logic that does not hold for all logics.Second-order logic, for example, does not have a completeness theorem for its standard semantics (though does have the completeness property forHenkin semantics), and the set of logically valid formulas in second-order logic is not recursively enumerable. The same is true of all higher-order logics. It is possible to produce sound deductive systems for higher-order logics, but no such system can be complete.

Lindström's theorem states that first-order logic is the strongest (subject to certain constraints) logic satisfying both compactness and completeness.

A completeness theorem can be proved formodal logic orintuitionistic logic with respect toKripke semantics.

Gödel'soriginal proof of the theorem proceeded by reducing the problem to a special case for formulas in a certain syntactic form, and then handling this form with anad hoc argument.

In modern logic texts, Gödel's completeness theorem is usually proved withHenkin's proof, rather than with Gödel's original proof. Henkin's proof directly constructs aterm model for any consistent first-order theory. James Margetson (2004) developed a computerized formal proof using theIsabelle theorem prover.^[4] Other proofs are also known.

• Original proof of Gödel's completeness theorem
• Trakhtenbrot's theorem

• Gödel, K (1929).Über die Vollständigkeit des Logikkalküls (Thesis). Doctoral dissertation. University Of Vienna. The first proof of the completeness theorem.
• Gödel, K (1930). "Die Vollständigkeit der Axiome des logischen Funktionenkalküls".Monatshefte für Mathematik (in German).37 (1):349–360.doi:10.1007/BF01696781.JFM 56.0046.04.S2CID 123343522. The same material as the dissertation, except with briefer proofs, more succinct explanations, and omitting the lengthy introduction.
• Hans Hermes (1973).Introduction to Mathematical Logic. Hochschultext (Springer-Verlag). London: Springer.ISBN 3540058192.ISSN 1431-4657. Chapter 5:"Gödel's completeness theorem".

• Stanford Encyclopedia of Philosophy: "Kurt Gödel"—byJuliette Kennedy.
• MacTutor biography:Kurt Gödel.Archived 2005-10-13 at theWayback Machine
• Detlovs, Vilnis, and Podnieks, Karlis, "Introduction to mathematical logic."

• Theorems in the foundations of mathematics
• Metatheorems
• Model theory
• Proof theory
• Works by Kurt Gödel

• Articles with short description
• Short description matches Wikidata
• All articles with unsourced statements
• Articles with unsourced statements from December 2024
• CS1 German-language sources (de)
• Webarchive template wayback links