Gödel's completeness theorem is a fundamental theorem in mathematical logic that establishes a correspondence between semantic truth and syntactic provability in firstorder logic.
The completeness theorem applies to any firstorder theory: 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 (firstorder) proof of φ using the statements of T as axioms. One sometimes says this as "anything universally true is provable". This does not contradict Gödel's incompleteness theorem, which shows that some formula φ_{u} is unprovable although true in the natural numbers, which are a particular model of a firstorder theory describing them — φ_{u} is just false in some other model of the firstorder theory being considered (such as a nonstandard model of arithmetic for Peano arithmetic). This kind of failure of consistency between a standard and nonstandard model is also called Omega Inconsistency.^{[1]}
It makes a close link between model theory that deals with what is true in different models, and proof theory that studies what can be formally proven in particular formal systems.
It was first proved by Kurt Gödel in 1929. 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).^{[2]} Henkin's proof was simplified by Gisbert Hasenjaeger in 1953.^{[3]}
YouTube Encyclopedic

1/5Views:2 882 2432 004 249168 79450722 394 773

The paradox at the heart of mathematics: Gödel's Incompleteness Theorem  Marcus du Sautoy

Gödel's Incompleteness Theorem  Numberphile

Math's Existential Crisis (Gödel's Incompleteness Theorems)

Mathematical Logic, Lecture 7 (Proof of Gödel's Completeness Theorem)

Math's Fundamental Flaw
Transcription
Preliminaries
There are numerous deductive systems for firstorder logic, including systems of natural deduction and Hilbertstyle 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 formulae with a specially designated conclusion. The definition of a deduction is such that it is finite and that it is possible to verify algorithmically (by a computer, for example, or by hand) that a given sequence (or tree) of formulae is indeed a deduction.
A firstorder formula is called logically valid if it is true in every structure 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, the fact that only logically valid formulas are provable in the deductive system.
If some specific deductive system of firstorder 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 firstorder predicate calculus, choosing any of the wellknown equivalent systems. Gödel's original proof assumed the HilbertAckermann 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, 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 , 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 of T. The completeness theorem then says that for any firstorder theory T with a wellorderable language, and any sentence s in the language of T,
Since the converse (soundness) also holds, it follows that if and only if , and thus that syntactic and semantic consequence are equivalent for firstorder 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 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 firstorder theory T with a wellorderable language,
Another version, with connections to the Löwenheim–Skolem theorem, 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. Precisely, we can systematically define a model of any consistent effective firstorder 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 firstorder 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 show that there are inherent limitations to what can be proven within any given firstorder 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, effective and contains Robinson arithmetic ("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 nonstandard numbers.
In fact, the model of any theory containing Q obtained by the systematic construction of the arithmetical model existence theorem, is always nonstandard with a nonequivalent provability predicate and a nonequivalent way to interpret its own construction, so that this construction is nonrecursive (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 nonstandard models.
Relationship to the compactness theorem
The completeness theorem and the compactness theorem are two cornerstones of firstorder 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. 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 secondorder variant of Peano arithmetic restricted to induction over Σ^{0}_{1} formulas). 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 same cardinality.
Completeness in other logics
The completeness theorem is a central property of firstorder logic that does not hold for all logics. Secondorder logic, for example, does not have a completeness theorem for its standard semantics (but does have the completeness property for Henkin semantics), and the set of logicallyvalid formulas in secondorder logic is not recursively enumerable. The same is true of all higherorder logics. It is possible to produce sound deductive systems for higherorder logics, but no such system can be complete.
Lindström's theorem states that firstorder 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.
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 for any consistent firstorder theory. James Margetson (2004) developed a computerized formal proof using the Isabelle theorem prover.^{[4]} Other proofs are also known.
See also
Further reading
 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 (SpringerVerlag). London: Springer. ISBN 3540058192. ISSN 14314657. Chapter 5: "Gödel's completeness theorem".
 ^ Batzoglou, Serafim (2021). "Gödel's Incompleteness Theorem". arXiv:2112.06641. (p.17). Accessed 20221201.
 ^ Leon Henkin (Sep 1949). "The completeness of the firstorder functional calculus". The Journal of Symbolic Logic. 14 (3): 159–166. doi:10.2307/2267044. JSTOR 2267044. S2CID 28935946.
 ^ Gisbert F. R. Hasenjaeger (Mar 1953). "Eine Bemerkung zu Henkin's Beweis für die Vollständigkeit des Prädikatenkalküls der Ersten Stufe". The Journal of Symbolic Logic. 18 (1): 42–48. doi:10.2307/2266326. JSTOR 2266326. S2CID 45705695.
 ^ James Margetson (Sep 2004). Proving the Completeness Theorem within Isabelle/HOL (PDF) (Technical Report). Archived (PDF) from the original on 20060222.
External links
 Stanford Encyclopedia of Philosophy: "Kurt Gödel"—by Juliette Kennedy.
 MacTutor biography: Kurt Gödel. Archived 20051013 at the Wayback Machine
 Detlovs, Vilnis, and Podnieks, Karlis, "Introduction to mathematical logic."