Godel's Completeness Theorem

The Gödel completeness theorem (named after Kurt Gödel ) is the law of mathematical logic . It shows the correctness and completeness of the Hilbert calculus (a formal system of first-order predicate logic ) : every sentence that semantically follows from a set of formulas can be derived from the set of formulas using the inference rules of the system , and vice versa. For the logic of the first level, syntactic and semantic inference are therefore synonymous.

Basic concepts

Formulas : First, a number of constant, function and relation symbols must be specified. In addition to these symbols, propositional joiners , the quantifiers , the equal sign and variables for the formula structure are available.

Semantics : A structure is a non-empty set in which the constant, function and relation symbols are interpreted by elements, functions and relations. An interpretation also includes assignment of the variables with values from the structure. A formula is universal if it is true in every interpretation. An interpretation that makes every formula from a set of formulastrue is called a model of. A formulais a semantic inference from(in characters) whenis truein each model. ${\ displaystyle \ Gamma \}$ ${\ displaystyle \ Gamma \}$ ${\ displaystyle \ varphi}$ ${\ displaystyle \ Gamma \}$ ${\ displaystyle \ Gamma \ vDash \ varphi}$ ${\ displaystyle \ varphi}$ ${\ displaystyle \ Gamma \}$

Derivations : A Hilbert calculus is given by axioms and rules of inference. The most important final rule is the modus ponens : From the formulasandone is allowed topass over. A formulacan be derived from a set of formulas(in signs) if there is a finitesequence of formulas that ends with, where for each term of the sequence the following applies: it is an axiom or an element ofor it is derived from earlier terms of the Sequence formed. ${\ displaystyle \ varphi}$ ${\ displaystyle \ varphi \ rightarrow \ psi}$ ${\ displaystyle \ psi \}$ ${\ displaystyle \ varphi}$ ${\ displaystyle \ Gamma \}$ ${\ displaystyle \ Gamma \ vdash \ varphi}$ ${\ displaystyle \ varphi}$ ${\ displaystyle \ Gamma \}$

The sentence

In 1929 Kurt Gödel proved the completeness theorem essentially in the following form:

There is a calculus of first-order predicate logic such that for every set of formulas and for every formula : ${\ displaystyle \ Gamma}$ ${\ displaystyle \ varphi}$

${\ displaystyle \ varphi}$ follows from if and only if in the calculus can be derived from . ${\ displaystyle \ Gamma}$ ${\ displaystyle \ varphi}$ ${\ displaystyle \ Gamma}$

If one uses as a sign for the semantic inference and for the deducibility in the calculus, the short formulation results: ${\ displaystyle \ vDash}$ ${\ displaystyle \ vdash}$

{\ displaystyle (\ Gamma \ vDash \ varphi) \ Longleftrightarrow (\ Gamma \ vdash \ varphi)}

The conclusion from right to left means the correctness of the calculus: Everything that can be derived with the calculus from given assumptions really follows logically from these assumptions. Every meaningful logic calculus must meet this requirement.

The conclusion from left to right is the actual completeness: It is claimed that for every proposition that logically follows from a set of given assumptions, there actually exists a proof from these assumptions in the calculus.

A weakened version of the completeness clause is often formulated as follows:

There is a calculus of first order predicate logic such that for every formula : ${\ displaystyle \ varphi}$

${\ displaystyle \ varphi}$ is generally valid if and only can be proven in the calculus. ${\ displaystyle \ varphi}$

In characters this version reads briefly:

{\ displaystyle (\ vDash \ varphi) \ Longleftrightarrow \ (\ vdash \ varphi)}

It is a special case of the above statement, where the formula set is empty. ${\ displaystyle \ Gamma}$

It is important to remember that completeness is a quality of calculus. The symbol for the deducibility is actually an abbreviation for , where denotes the calculus. A concrete calculus must be given to prove the theorem. Gödel did this with a Hilbert calculus consisting of axioms and rules of inference. The sequence calculus introduced by Gerhard Gentzen , for example, is also complete . ${\ displaystyle \ vdash}$ ${\ displaystyle \ vdash _ {K}}$ ${\ displaystyle K}$

Proof idea

Godel originally proved the theorem by reducing the problem to completeness for a restricted class of formulas, for which completeness can then be reduced to the completeness of propositional logic . Today a proof published by Leon Henkin in 1949 is mostly used. To this end, the following theorem is proven first:

Every consistent set of formulas has a model.

Consistency is a syntactic term and means for a set of formulas that no contradiction in the calculus can be derived from it (formally: there is no formula with and ). ${\ displaystyle \ Gamma \}$ ${\ displaystyle \ varphi}$ ${\ displaystyle \ Gamma \ vdash \ varphi}$ ${\ displaystyle \ Gamma \ vdash \ neg \ varphi}$

The existence of the model is proven by using Lindenbaum's theorem to expand a given consistent formula set to a so-called maximally consistent set that does not have a consistent proper superset. Then, the speech is by so-called Henkinkonstanten expanded, thus expanding the set of formulas that for each formula of the form and ( c a Henkinkonstante) is included. Then, according to Henkin's theorem, there is a term interpretation whose basic set consists of the terms of language and which satisfies all elements of the resulting set of formulas, and thus also the original, consistent set of formulas . ${\ displaystyle \ Gamma \}$ ${\ displaystyle \ exists x \ varphi (x)}$ ${\ displaystyle \ varphi (c)}$ ${\ displaystyle \ Gamma \}$

Then the completeness can easily be shown: Assuming it is true , but not . The calculus has the property that the negation of a formula that cannot be derived from a consistent set of formulas can be added to the set of formulas, and the consistency is retained. In the present case is therefore consistent and has a model according to Henkin's theorem. In this model, however, is now false, in contradiction to the assumption that in all models of is true. ${\ displaystyle \ Gamma \ vDash \ varphi}$ ${\ displaystyle \ Gamma \ vdash \ varphi}$ ${\ displaystyle \ Gamma \ cup \ {\ neg \ varphi \}}$ ${\ displaystyle \ varphi}$ ${\ displaystyle \ varphi}$ ${\ displaystyle \ Gamma \}$

meaning

The fact that the content-related logical inference can be completely mapped through derivations in a recursive calculus is an outstanding property of first-level predicate logic. This completeness does not apply to many other logics, for example not to the higher-level predicate logic .

The compactness theorem , a central theorem of model theory , results as a corollary from the completeness theorem.

In the context of the Hilbert program (to create a consistent and complete calculus for mathematics) the sentence initially seemed to be a step towards the goal. The program failed, however, because Gödel was able to show with his incompleteness theorem that a sufficiently expressive theory cannot prove every true sentence. (Note that the incompleteness clause refers to a different type of completeness than the completeness clause presented here.)

Position in set theory

For countable (or more generally: well-ordered) sets of symbols, the completeness theorem from the axioms of the Zermelo-Fraenkel set theory can be proven without the axiom of choice. The proof for any set of symbols can be carried out with the axiom of choice, but the theorem is not equivalent to the axiom of choice, but (relative to the axioms of set theory without the axiom of choice) u. a. to:

literature

Hans Dieter Ebbinghaus, Jörg Flum, Wolfgang Thomas: Introduction to mathematical logic . Spektrum Akademischer Verlag, Heidelberg 2007, ISBN 3-8274-1691-4 .
K Gödel : About the completeness of the logic calculus . In: University Of Vienna. (Ed.): Dissertation . 1929.
K Gödel : The completeness of the axioms of the logical function calculus . In: Monthly books for mathematics . 37, No. 1, 1930, pp. 349-360. doi : 10.1007 / BF01696781 .
Leon Henkin: The Completeness of the First-Order Functional Calculus . In: Journal of Symbolic Logic , 14, 1949, pp. 159-166
Wolfgang Rautenberg : Introduction to Mathematical Logic . 3. Edition. Vieweg + Teubner, Wiesbaden 2008, ISBN 978-3-8348-0578-2 .