Gödel's completeness theorem
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.
(This does not contradict 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.[1]) The completeness theorem makes a close link between model theory, which deals with what is true in different models, and proof theory, which studies what can be formally proven in particular formal systems.
It was then simplified when Leon Henkin observed in his Ph.D. thesis that the hard part of the proof can be presented as the Model Existence Theorem (published in 1949).
This is a sequence (or, in some cases, a finite tree) of formulae with a specially designated conclusion.
To formally state, and then prove, the completeness theorem, it is necessary to also define a deductive system.
A converse to completeness is soundness, the fact that only logically valid formulas are provable in the deductive system.
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, 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.
The theorem can be expressed more generally in terms of logical consequence.
Gödel's original formulation is deduced by taking the particular case of a theory without any axiom.
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 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.)
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.
Gödel's incompleteness theorems show that there are inherent limitations to what can be proven within any given first-order theory in mathematics.
which is consistent, effective and contains Robinson arithmetic ("Q") must be incomplete in this sense, by explicitly constructing a sentence
; but the incompleteness theorem showed this to be impossible, so the counterexample must not be a standard number, and thus any model of
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.
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.
The ineffectiveness of the completeness theorem can be measured along the lines of reverse mathematics.
Weak Kőnig's lemma is provable in ZF, the system of Zermelo–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 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 the same cardinality.
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.
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.
