Gödel's completeness theorem
Encyclopedia
Gödel's completeness theorem is a fundamental theorem in mathematical logic
that establishes a correspondence between semantic truth and syntactic provability
in first-order logic
. It was first proved by Kurt Gödel
in 1929.
A first-order formula is called logically valid if it is true in every structure
for its language. The completeness theorem shows that if a formula is logically valid then there is a finite deduction (a formal proof) of the formula. The deduction is a finite object that can be verified by hand or computer. This relationship between truth and provability establishes a close link between model theory
and proof theory
in mathematical logic.
An important consequence of the completeness theorem is that it is possible to enumerate the logical consequences of any effective first-order theory, by enumerating all the correct deductions using axioms from the theory.
Gödel's incompleteness theorem, referring to a different meaning of completeness, shows that if any sufficiently strong effective theory of arithmetic is consistent then there is a formula (depending on the theory) which can neither be proven nor disproven within the theory. Nevertheless the completeness theorem applies to these theories, showing that any logical consequence of such a theory is provable from the theory.
s for first-order logic, including systems of natural deduction
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
) of formulas with a specially-designated conclusion. The definition of a deduction is such that it is finite and that it is possible to verify algorithm
ically (by a computer
, for example, or by hand) that a given collection of formulas is indeed a deduction.
A formula is logically valid if it is true in every structure
for the language 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.
it is the conclusion of a formal deduction.
A more general version of Gödel's completeness theorem holds. It says that for any first-order theory T and any sentence S in the language of the theory, there is a formal deduction of S from T if and only if S is satisfied by every model of T. 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.
The branch of mathematical logic that deals with what is true in different models is called model theory
. The branch called proof theory
studies what can be formally proved in particular formal system
s. The completeness theorem establishes a fundamental connection between these two branches, giving a link between semantics
and syntax
. The completeness theorem should not, however, be misinterpreted as obliterating the difference between these two concepts; in fact Gödel's incompleteness theorem, another celebrated result, shows that there are inherent limitations in what can be achieved with formal proofs in mathematics. The name for the incompleteness theorem refers to another meaning of complete (see model theory - Using the compactness and completeness theorems). In particular, Gödel's completeness theorem deals with formulas that are logical consequences of a first-order theory, while the incompleteness theorem constructs formulas that are not logical consequences of certain theories.
An important consequence of the completeness theorem is that the set of logical consequences of an effective first-order theory is an enumerable set. The definition of logical consequence quantifies over all structures in a particular language, and thus does not give an immediate method for algorithmically testing whether a formula is logically valid. Moreover, a consequence of Gödel's incompleteness theorem is that the set of logically valid formulas is not decidable. But the completeness theorem implies that the set of consequences of an effective theory is enumerable; the algorithm is to first construct an enumeration of all formal deductions from the theory, and use this to produce an enumeration of their conclusions. The finitary, syntactic nature of formal deductions makes it possible to enumerate them.
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 deduction 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
. 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 RCA0 (a second-order variant of Peano arithmetic restricted to induction over Σ01 formulas). Weak König's lemma is provable in ZF, the system of Zermelo–Fraenkel set theory
, 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 known as the 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 same cardinality, knowing that on countable sets, the ultrafilter lemma becomes equivalent to weak König's lemma. Also, although every consistent, countable first-order theory has a finite or countable model (as a consequence of the completeness theorem and the Löwenheim-Skolem theorem), it is known there are effective consistent first-order theories that do not have computable models.
that does not hold for all logics. Second-order logic
, for example, does not have a completeness theorem for its standard semantics (but does have the completeness property for Henkin
semantics), and 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. The set of logically-valid formulas in second-order logic is not enumerable.
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 for modal logic
or intuitionistic logic
with respect to Kripke semantics
.
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 for any consistent first-order theory. James Margetson (2004) developed a computerized formal proof using the Isabelle theorem prover. http://afp.sourceforge.net/entries/Completeness-paper.pdf Other proofs are also known.
Mathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
that establishes a correspondence between semantic truth and syntactic provability
Provability logic
Provability logic is a modal logic, in which the box operator is interpreted as 'it is provable that'. The point is to capture the notion of a proof predicate of a reasonably rich formal theory, such as Peano arithmetic....
in first-order logic
First-order logic
First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic...
. It was first proved by Kurt Gödel
Kurt Gödel
Kurt Friedrich Gödel was an Austrian logician, mathematician and philosopher. Later in his life he emigrated to the United States to escape the effects of World War II. One of the most significant logicians of all time, Gödel made an immense impact upon scientific and philosophical thinking in the...
in 1929.
A first-order formula is called logically valid if it is true in every structure
Structure (mathematical logic)
In universal algebra and in model theory, a structure consists of a set along with a collection of finitary operations and relations which are defined on it....
for its language. The completeness theorem shows that if a formula is logically valid then there is a finite deduction (a formal proof) of the formula. The deduction is a finite object that can be verified by hand or computer. This relationship between truth and provability establishes a close link between model theory
Model theory
In mathematics, model theory is the study of mathematical structures using tools from mathematical logic....
and proof theory
Proof theory
Proof theory is a branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as plain lists, boxed lists, or trees, which are constructed...
in mathematical logic.
An important consequence of the completeness theorem is that it is possible to enumerate the logical consequences of any effective first-order theory, by enumerating all the correct deductions using axioms from the theory.
Gödel's incompleteness theorem, referring to a different meaning of completeness, shows that if any sufficiently strong effective theory of arithmetic is consistent then there is a formula (depending on the theory) which can neither be proven nor disproven within the theory. Nevertheless the completeness theorem applies to these theories, showing that any logical consequence of such a theory is provable from the theory.
Background
There are numerous deductive systemDeductive system
A deductive system consists of the axioms and rules of inference that can be used to derive the theorems of the system....
s for first-order logic, including systems of natural deduction
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...
and Hilbert-style systems
Hilbert-style deduction system
In logic, especially mathematical logic, a Hilbert system, sometimes called Hilbert calculus or Hilbert–Ackermann system, is a type of system of formal deduction attributed to Gottlob Frege and David Hilbert...
. Common to all deductive systems is the notion of a formal deduction. This is a sequence (or, in some cases, a finite tree
Tree structure
A tree structure is a way of representing the hierarchical nature of a structure in a graphical form. It is named a "tree structure" because the classic representation resembles a tree, even though the chart is generally upside down compared to an actual tree, with the "root" at the top and the...
) of formulas with a specially-designated conclusion. The definition of a deduction is such that it is finite and that it is possible to verify algorithm
Algorithm
In mathematics and computer science, an algorithm is an effective method expressed as a finite list of well-defined instructions for calculating a function. Algorithms are used for calculation, data processing, and automated reasoning...
ically (by a computer
Computer
A computer is a programmable machine designed to sequentially and automatically carry out a sequence of arithmetic or logical operations. The particular sequence of operations can be changed readily, allowing the computer to solve more than one kind of problem...
, for example, or by hand) that a given collection of formulas is indeed a deduction.
A formula is logically valid if it is true in every structure
Structure (mathematical logic)
In universal algebra and in model theory, a structure consists of a set along with a collection of finitary operations and relations which are defined on it....
for the language 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.
Statement and consequences
Gödel's completeness theorem says that a deductive system of first-order predicate calculus is "complete" in the sense that no additional inference rules are required to prove all the logically valid formulas. A converse to completeness is soundness, the fact that only logically valid formulas are provable in the deductive system. Taken together, these theorems imply that a formula is logically valid if and only ifIf and only if
In logic and related fields such as mathematics and philosophy, if and only if is a biconditional logical connective between statements....
it is the conclusion of a formal deduction.
A more general version of Gödel's completeness theorem holds. It says that for any first-order theory T and any sentence S in the language of the theory, there is a formal deduction of S from T if and only if S is satisfied by every model of T. This more general theorem is used implicitly, for example, when a sentence is shown to be provable from the axioms of group theory
Group theory
In mathematics and abstract algebra, group theory studies the algebraic structures known as groups.The concept of a group is central to abstract algebra: other well-known algebraic structures, such as rings, fields, and vector spaces can all be seen as groups endowed with additional operations and...
by considering an arbitrary group and showing that the sentence is satisfied by that group.
The branch of mathematical logic that deals with what is true in different models is called model theory
Model theory
In mathematics, model theory is the study of mathematical structures using tools from mathematical logic....
. The branch called proof theory
Proof theory
Proof theory is a branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as plain lists, boxed lists, or trees, which are constructed...
studies what can be formally proved in particular formal system
Formal system
In formal logic, a formal system consists of a formal language and a set of inference rules, used to derive an expression from one or more other premises that are antecedently supposed or derived . The axioms and rules may be called a deductive apparatus...
s. The completeness theorem establishes a fundamental connection between these two branches, giving a link between semantics
Semantics
Semantics is the study of meaning. It focuses on the relation between signifiers, such as words, phrases, signs and symbols, and what they stand for, their denotata....
and syntax
Syntax
In linguistics, syntax is the study of the principles and rules for constructing phrases and sentences in natural languages....
. The completeness theorem should not, however, be misinterpreted as obliterating the difference between these two concepts; in fact Gödel's incompleteness theorem, another celebrated result, shows that there are inherent limitations in what can be achieved with formal proofs in mathematics. The name for the incompleteness theorem refers to another meaning of complete (see model theory - Using the compactness and completeness theorems). In particular, Gödel's completeness theorem deals with formulas that are logical consequences of a first-order theory, while the incompleteness theorem constructs formulas that are not logical consequences of certain theories.
An important consequence of the completeness theorem is that the set of logical consequences of an effective first-order theory is an enumerable set. The definition of logical consequence quantifies over all structures in a particular language, and thus does not give an immediate method for algorithmically testing whether a formula is logically valid. Moreover, a consequence of Gödel's incompleteness theorem is that the set of logically valid formulas is not decidable. But the completeness theorem implies that the set of consequences of an effective theory is enumerable; the algorithm is to first construct an enumeration of all formal deductions from the theory, and use this to produce an enumeration of their conclusions. The finitary, syntactic nature of formal deductions makes it possible to enumerate them.
Relationship to the compactness theorem
The completeness theorem and the compactness theoremCompactness 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...
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 deduction 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
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 contrast to the ordinary mathematical practice of...
. 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 RCA0 (a second-order variant of Peano arithmetic restricted to induction over Σ01 formulas). Weak König's lemma is provable in ZF, the system of Zermelo–Fraenkel set theory
Zermelo–Fraenkel set theory
In mathematics, Zermelo–Fraenkel set theory with the axiom of choice, named after mathematicians Ernst Zermelo and Abraham Fraenkel and commonly abbreviated ZFC, is one of several axiomatic systems that were proposed in the early twentieth century to formulate a theory of sets without the paradoxes...
, 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 known as the 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 same cardinality, knowing that on countable sets, the ultrafilter lemma becomes equivalent to weak König's lemma. Also, although every consistent, countable first-order theory has a finite or countable model (as a consequence of the completeness theorem and the Löwenheim-Skolem theorem), it is known there are effective consistent first-order theories that do not have computable models.
Completeness in other logics
The completeness theorem is a central property of first-order logicFirst-order logic
First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic...
that does not hold for all logics. Second-order logic
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....
, for example, does not have a completeness theorem for its standard semantics (but does have the completeness property for Henkin
Leon Henkin
Leon Albert Henkin was a logician at the University of California, Berkeley. He was principally known for the "Henkin's completeness proof": his version of the proof of the semantic completeness of standard systems of first-order logic.-The completeness proof:Henkin's result was not novel; it had...
semantics), and 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. The set of logically-valid formulas in second-order logic is not enumerable.
Lindström's theorem
Lindström's theorem
In mathematical logic, Lindström's theorem states that first-order logic is the strongest logic In mathematical logic, Lindström's theorem (named after Swedish logician Per Lindström) states that first-order logic is the strongest logic In mathematical logic, Lindström's theorem (named after...
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
Modal logic is a type of formal logic that extends classical propositional and predicate logic to include operators expressing modality. Modals — words that express modalities — qualify a statement. For example, the statement "John is happy" might be qualified by saying that John is...
or intuitionistic logic
Intuitionistic logic
Intuitionistic logic, or constructive logic, is a symbolic logic system differing from classical logic in its definition of the meaning of a statement being true. In classical logic, all well-formed statements are assumed to be either true or false, even if we do not have a proof of either...
with respect to Kripke semantics
Kripke semantics
Kripke semantics is a formal semantics for non-classical logic systems created in the late 1950s and early 1960s by Saul Kripke. It was first made for modal logics, and later adapted to intuitionistic logic and other non-classical systems...
.
Proofs
Gödel's original proof of the theoremOriginal proof of Gödel's completeness theorem
The proof of Gödel's completeness theorem given by Kurt Gödel in his doctoral dissertation of 1929 is not easy to read today; it uses concepts and formalism that are outdated and terminology that is often obscure...
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
Leon Henkin
Leon Albert Henkin was a logician at the University of California, Berkeley. He was principally known for the "Henkin's completeness proof": his version of the proof of the semantic completeness of standard systems of first-order logic.-The completeness proof:Henkin's result was not novel; it had...
's proof, rather than with Gödel's original proof. Henkin's proof directly constructs a term model for any consistent first-order theory. James Margetson (2004) developed a computerized formal proof using the Isabelle theorem prover. http://afp.sourceforge.net/entries/Completeness-paper.pdf Other proofs are also known.
See also
- Gödel's incompleteness theoremsGödel's incompleteness theoremsGödel's incompleteness theorems are two theorems of mathematical logic that establish inherent limitations of all but the most trivial axiomatic systems capable of doing arithmetic. The theorems, proven by Kurt Gödel in 1931, are important both in mathematical logic and in the philosophy of...
- Original proof of Gödel's completeness theoremOriginal proof of Gödel's completeness theoremThe proof of Gödel's completeness theorem given by Kurt Gödel in his doctoral dissertation of 1929 is not easy to read today; it uses concepts and formalism that are outdated and terminology that is often obscure...
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.External links
- Stanford Encyclopedia of PhilosophyStanford Encyclopedia of PhilosophyThe Stanford Encyclopedia of Philosophy is a freely-accessible online encyclopedia of philosophy maintained by Stanford University. Each entry is written and maintained by an expert in the field, including professors from over 65 academic institutions worldwide...
: "Kurt Gödel" -- by Juliette Kennedy. - MacTutor biography: Kurt Gödel.
- Detlovs, Vilnis, and Podnieks, Karlis, "Introduction to mathematical logic."