
Gödel's completeness theorem is a fundamental theorem in
mathematical logic
Mathematical logic is the study of Logic#Formal logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory (also known as computability theory). Research in mathematical logic com ...
that establishes a correspondence between
semantic
Semantics is the study of linguistic Meaning (philosophy), meaning. It examines what meaning is, how words get their meaning, and how the meaning of a complex expression depends on its parts. Part of this process involves the distinction betwee ...
truth and syntactic
provability in
first-order logic
First-order logic, also called predicate logic, predicate calculus, or quantificational logic, is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over ...
.
The completeness theorem applies to any first-order
theory
A theory is a systematic and rational form of abstract thinking about a phenomenon, or the conclusions derived from such thinking. It involves contemplative and logical reasoning, often supported by processes such as observation, experimentation, ...
: If ''T'' is such a theory, and φ is a sentence (in the same language) and every model of ''T'' is a model of φ, then there is a (first-order) proof of φ using the statements of ''T'' as axioms. One sometimes says this as "anything true in all models is provable". (This does not contradict
incompleteness theorem">Gödel's incompleteness theorem, which is about a formula φ
u that is unprovable in a certain theory ''T'' but true in the "standard" model of the natural numbers: φ
u is false in some other, "non-standard" models of ''T''.)
The completeness theorem makes a close link between
model theory
In mathematical logic, model theory is the study of the relationship between theory (mathematical logic), formal theories (a collection of Sentence (mathematical logic), sentences in a formal language expressing statements about a Structure (mat ...
, which deals with what is true in different models, and
proof theory
Proof theory is a major branchAccording to , proof theory is one of four domains mathematical logic, together with model theory, axiomatic set theory, and recursion theory. consists of four corresponding parts, with part D being about "Proof The ...
, which studies what can be formally proven in particular
formal system
A formal system is an abstract structure and formalization of an axiomatic system used for deducing, using rules of inference, theorems from axioms.
In 1921, David Hilbert proposed to use formal systems as the foundation of knowledge in ma ...
s.
It was first proved by
Kurt Gödel
Kurt Friedrich Gödel ( ; ; April 28, 1906 – January 14, 1978) was a logician, mathematician, and philosopher. Considered along with Aristotle and Gottlob Frege to be one of the most significant logicians in history, Gödel profoundly ...
in 1929. It was then simplified when
Leon Henkin
Leon Albert Henkin (April 19, 1921, Brooklyn, New York – November 1, 2006, Oakland, California) was an American logician, whose works played a strong role in the development of logic, particularly in the Type theory, theory of types. He was an ...
observed in his
Ph.D. thesis that the hard part of the proof can be presented as the Model Existence Theorem (published in 1949). Henkin's proof was simplified by
Gisbert Hasenjaeger in 1953.
Preliminaries
There are numerous
deductive system
A formal system is an abstract structure and formalization of an axiomatic system used for deducing, using rules of inference, theorems from axioms.
In 1921, David Hilbert proposed to use formal systems as the foundation of knowledge in math ...
s for first-order logic, including systems of
natural deduction
In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning. This contrasts with Hilbert-style systems, which instead use ...
and
Hilbert-style systems. Common to all deductive systems is the notion of a ''formal deduction''. This is a sequence (or, in some cases, a finite
tree
In botany, a tree is a perennial plant with an elongated stem, or trunk, usually supporting branches and leaves. In some usages, the definition of a tree may be narrower, e.g., including only woody plants with secondary growth, only ...
) of formulae with a specially designated ''conclusion''. The definition of a deduction is such that it is finite and that it is possible to verify
algorithm
In mathematics and computer science, an algorithm () is a finite sequence of Rigour#Mathematics, mathematically rigorous instructions, typically used to solve a class of specific Computational problem, problems or to perform a computation. Algo ...
ically (by a
computer
A computer is a machine that can be Computer programming, programmed to automatically Execution (computing), carry out sequences of arithmetic or logical operations (''computation''). Modern digital electronic computers can perform generic set ...
, for example, or by hand) that a given sequence (or tree) of formulae is indeed a deduction.
A first-order formula is called ''
logically valid'' if it is true in every
structure
A structure is an arrangement and organization of interrelated elements in a material object or system, or the object or system so organized. Material structures include man-made objects such as buildings and machines and natural objects such as ...
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 called ''complete'' 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 is ''
soundness
In logic and deductive reasoning, an argument is sound if it is both Validity (logic), valid in form and has no false premises. Soundness has a related meaning in mathematical logic, wherein a Formal system, formal system of logic is sound if and o ...
'', 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).
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
In logic and deductive reasoning, an argument is sound if it is both Validity (logic), valid in form and has no false premises. Soundness has a related meaning in mathematical logic, wherein a Formal system, formal system of logic is sound if and o ...
'', 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
In logic and related fields such as mathematics and philosophy, "if and only if" (often shortened as "iff") is paraphrased by the biconditional, a logical connective between statements. The biconditional is true in two cases, where either bo ...
it is the conclusion of a formal deduction.
More general form
The theorem can be expressed more generally in terms of
logical consequence
Logical consequence (also entailment or logical implication) is a fundamental concept in logic which describes the relationship between statement (logic), statements that hold true when one statement logically ''follows from'' one or more stat ...
. We say that a sentence ''s'' is a ''syntactic consequence'' of a theory ''T'', denoted
, if ''s'' is provable from ''T'' in our deductive system. We say that ''s'' is a ''semantic consequence'' of ''T'', denoted
, if ''s'' holds in every
model
A model is an informative representation of an object, person, or system. The term originally denoted the plans of a building in late 16th-century English, and derived via French and Italian ultimately from Latin , .
Models can be divided in ...
of ''T''. The completeness theorem then says that for any first-order theory ''T'' with a
well-order
In mathematics, a well-order (or well-ordering or well-order relation) on a set is a total ordering on with the property that every non-empty subset of has a least element in this ordering. The set together with the ordering is then calle ...
able language, and any sentence ''s'' in the language of ''T'',
Since the converse (soundness) also holds, it follows that
if and only if
In logic and related fields such as mathematics and philosophy, "if and only if" (often shortened as "iff") is paraphrased by the biconditional, a logical connective between statements. The biconditional is true in two cases, where either bo ...
, 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
In abstract algebra, group theory studies the algebraic structures known as group (mathematics), groups.
The concept of a group is central to abstract algebra: other well-known algebraic structures, such as ring (mathematics), rings, field ( ...
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
In deductive logic, a consistent theory is one that does not lead to a logical contradiction. A theory T is consistent if there is no formula \varphi such that both \varphi and its negation \lnot\varphi are elements of the set of consequences ...
, 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
In mathematical logic, the Löwenheim–Skolem theorem is a theorem on the existence and cardinality of models, named after Leopold Löwenheim and Thoralf Skolem.
The precise formulation is given below. It implies that if a countable first-order ...
, says:
Given Henkin's theorem, the completeness theorem can be proved as follows: If
, then
does not have models. By the contrapositive of Henkin's theorem, then
is syntactically inconsistent. So a contradiction (
) is provable from
in the deductive system. Hence
, and then by the properties of the deductive system,
.
As a theorem of arithmetic
The model existence theorem and its proof can be formalized in the framework of
Peano arithmetic
In mathematical logic, the Peano axioms (, ), also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th-century Italian mathematician Giuseppe Peano. These axioms have been used nea ...
. 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,
Δ2).
Consequences
An important consequence of the completeness theorem is that it is possible to
recursively enumerate the semantic consequences of any
effective 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.
Relationship to the incompleteness theorems
Gödel's incompleteness theorems
Gödel's incompleteness theorems are two theorems of mathematical logic that are concerned with the limits of in formal axiomatic theories. These results, published by Kurt Gödel in 1931, are important both in mathematical logic and in the phi ...
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 of ''complete'' (see
model theory – Using the compactness and completeness theorems): A theory
is complete (or decidable) if every sentence
in the language of
is either provable (
) or disprovable (
).
The first incompleteness theorem states that any
which is
consistent
In deductive logic, a consistent theory is one that does not lead to a logical contradiction. A theory T is consistent if there is no formula \varphi such that both \varphi and its negation \lnot\varphi are elements of the set of consequences ...
,
effective and contains
Robinson arithmetic
In mathematics, Robinson arithmetic is a finitely axiomatized fragment of first-order Peano arithmetic (PA), first set out by Raphael M. Robinson in 1950. It is usually denoted Q.
Q is almost PA without the axiom schema of mathematical inducti ...
("''Q''") must be incomplete in this sense, by explicitly constructing a sentence
which is demonstrably neither provable nor disprovable within
. The second incompleteness theorem extends this result by showing that
can be chosen so that it expresses the consistency of
itself.
Since
cannot be proven in
, the completeness theorem implies the existence of a model of
in which
is false. In fact,
is a
Π1 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
within
; but the incompleteness theorem showed this to be impossible, so the counterexample must not be a standard number, and thus any model of
in which
is false must include
non-standard numbers.
In fact, the model of ''any'' theory containing ''Q'' obtained by the systematic construction of the arithmetical model existence theorem, is ''always'' 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
is at least slightly stronger than ''Q'' (e.g. if it includes induction for bounded existential formulas), then
Tennenbaum's theorem shows that it has no recursive non-standard models.
Relationship to the compactness theorem
The completeness theorem and the
compactness theorem
In mathematical logic, the compactness theorem states that a set of first-order sentences has a model if and only if every finite subset of it has a model. This theorem is an important tool in model theory, as it provides a useful (but generall ...
are two cornerstones of first-order logic. While neither of these theorems can be proven in a completely
effective 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 of
reverse mathematics
Reverse mathematics is a program in mathematical logic that seeks to determine which axioms are required to prove theorems of mathematics. Its defining method can briefly be described as "going backwards from the theorems to the axioms", in cont ...
. 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 as
weak Kőnig's lemma, with the equivalence provable in RCA
0 (a second-order variant of
Peano arithmetic
In mathematical logic, the Peano axioms (, ), also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th-century Italian mathematician Giuseppe Peano. These axioms have been used nea ...
restricted to induction over Σ
01 formulas). Weak Kőnig's lemma is provable in ZF, the system of
Zermelo–Fraenkel set theory
In set theory, Zermelo–Fraenkel set theory, named after mathematicians Ernst Zermelo and Abraham Fraenkel, is an axiomatic system that was proposed in the early twentieth century in order to formulate a theory of sets free of paradoxes suc ...
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 the
axiom of choice
In mathematics, the axiom of choice, abbreviated AC or AoC, is an axiom of set theory. Informally put, the axiom of choice says that given any collection of non-empty sets, it is possible to construct a new set by choosing one element from e ...
known as
the ultrafilter lemma
In the mathematical field of set theory, an ultrafilter on a set X is a ''maximal filter'' on the set X. In other words, it is a collection of subsets of X that satisfies the definition of a filter on X and that is maximal with respect to incl ...
. 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.
Completeness in other logics
The completeness theorem is a central property of
first-order logic
First-order logic, also called predicate logic, predicate calculus, or quantificational logic, is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over ...
that does not hold for all logics.
Second-order logic
In logic and mathematics, second-order logic is an extension of first-order logic, which itself is an extension of propositional logic. Second-order logic is in turn extended by higher-order logic and type theory.
First-order logic quantifies on ...
, for example, does not have a completeness theorem for its standard semantics (though does have the completeness property for
Henkin 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
In mathematical logic, Lindström's theorem (named after Swedish logician Per Lindström, who published it in 1969) states that first-order logic is the '' strongest logic'' (satisfying certain conditions, e.g. closure under classical negation) ...
states that first-order logic is the strongest (subject to certain constraints) logic satisfying both compactness and completeness.
A completeness theorem can be proved for
modal logic
Modal logic is a kind of logic used to represent statements about Modality (natural language), necessity and possibility. In philosophy and related fields
it is used as a tool for understanding concepts such as knowledge, obligation, and causality ...
or
intuitionistic logic
Intuitionistic logic, sometimes more generally called constructive logic, refers to systems of symbolic logic that differ from the systems used for classical logic by more closely mirroring the notion of constructive proof. In particular, systems ...
with respect to
Kripke semantics
Kripke semantics (also known as relational semantics or frame semantics, and often confused with possible world semantics) is a formal semantics for non-classical logic systems created in the late 1950s and early 1960s by Saul Kripke and André ...
.
Proofs
Gödel's
original 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 an ''ad hoc'' argument.
In modern logic texts, Gödel's completeness theorem is usually proved with
Henkin's proof, rather than with Gödel's original proof. Henkin's proof directly constructs a
term model
In first-order logic, a Herbrand structure S is a structure over a vocabulary \sigma (also sometimes called a ''signature'') that is defined solely by the syntactical properties of \sigma. The idea is to take the symbol strings of terms as their ...
for any consistent first-order theory. James Margetson (2004) developed a computerized formal proof using the
Isabelle
Isabel is a female name of Iberian origin. Isabelle is a name that is similar, but it is of French origin. It originates as the medieval Spanish form of '' Elisabeth'' (ultimately Hebrew ''Elisheba''). Arising in the 12th century, it became popul ...
theorem prover.
Other proofs are also known.
See also
*
Original proof of Gödel's completeness theorem
*
Trakhtenbrot's theorem In logic, finite model theory, and computability theory, Trakhtenbrot's theorem (due to Boris Trakhtenbrot) states that the problem of validity in first-order logic on the class of all finite models is undecidable. In fact, the class of valid se ...
References
Further reading
* The first proof of the completeness theorem.
* The same material as the dissertation, except with briefer proofs, more succinct explanations, and omitting the lengthy introduction.
* Chapter 5: ''"Gödel's completeness theorem"''.
External links
*
Stanford Encyclopedia of Philosophy
The ''Stanford Encyclopedia of Philosophy'' (''SEP'') is a freely available online philosophy resource published and maintained by Stanford University, encompassing both an online encyclopedia of philosophy and peer-reviewed original publication ...
:
Kurt Gödel—by
Juliette Kennedy.
* MacTutor biography
Kurt Gödel.
* Detlovs, Vilnis, and Podnieks, Karlis,
Introduction to mathematical logic.
{{DEFAULTSORT:Godels Completeness Theorem
Theorems in the foundations of mathematics
Metatheorems
Model theory
Proof theory
Completeness theorem
Complete may refer to:
Logic
* Completeness (logic)
* Completeness of a theory, the property of a theory that every formula in the theory's language or its negation is provable
Mathematics
* The completeness of the real numbers, which implies ...