Gödel's completeness theorem

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

Basic concepts

Formulas: First, a set of constants, function and relation symbols must be defined. In addition to these symbols then are propositional connectives, quantifiers, the equality sign as well as variables for formula construction available.

Semantics: A structure is a non-empty set, in which the constant, function and relation symbols are interpreted by elements, functions and relations. For an interpretation also implies that assignment to the variables with values ​​from the structure. A formula is generally valid if it is true in every interpretation. An interpretation that makes every formula from a set of formulas true is called a model of. A formula is a semantic consequence of ( in characters) if in every model of is true.

Derivations: A Hilbert calculus is given by axioms and rules of inference. The main rule of inference is the modus ponens: From the formulas and one must to go. A formula is composed of a set of formulas derivable (in characters ) when there is a finite, are with -ending sequence of formulas, where for each term of the sequence is valid: it is an axiom or an element of or is connected to a circuit are from previous members sequence formed.

The set

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

If one uses as a sign for the semantic inference and for derivability in the calculus, there is the short formulation:

The conclusion from right to left means the soundness of the calculus: Everything that can be derived from given assumptions with the calculus, also follows logically from these assumptions really. Every reasonable logical calculus must meet this requirement.

The conclusion from left to right is the actual completeness: It is said that at any rate, the logically follows from a set of predefined assumptions, actual proof of these assumptions exist in the calculus.

A watered-down version of the completeness theorem is often expressed as:

In character this version is short:

It is a special case of the above statement, with the formula set is empty.

It is important to remember that completeness is a property of a calculus. The symbol for the derivability is therefore actually an acronym for, where denotes the calculus. For the proof of the theorem, a concrete calculus must be specified. Gödel has this with a Hilbert calculus consisting of axioms and rules of inference, done. Also completely, for example, introduced by Gerhard Gentzen sequent calculus.

Idea of ​​proof

Gödel proved the sentence originally by reducing the problem to the completeness for a restricted class of formulas for which completeness can then be attributed to the completeness of the propositional logic. Today, most of Leon Henkin in 1949 published a proof is used. For this purpose, first the following proposition is proved:

Consistency is a syntactic term and means for a set of formulas that made ​​her no contradiction in the calculus can be derived (formally: There is no formula with and ).

The existence of the model is proved by a given consistent set of formulas is extended to a so-called maximally consistent set, using the set of linden tree that has no consistent proper superset. Then the language is extended by so-called Henkinkonstanten and the set of formulas extended so that for each formula of the form and ( c Henkinkonstante a ) is included. Then there is, by the theorem of Henkin a term interpretation, the basic amount consists of the terms of the language and satisfies all the elements of the resulting set of formulas, and thus the original consistent set of formulas.

Then can easily show the completeness, suppose it is true, but not. The calculus has the property that it is possible to accept the negation of a non- derivable from a consistent set of formulas formula to the formula amount, and consistency is maintained. In the present case, therefore, is consistent and has, by the theorem of Henkin a model. In this model, but is now false, in contradiction to the assumption that in all models is true.

Importance

The fact that the content of logical reasoning can be completely mapped by derivatives in a recursive calculus, is an outstanding feature of the first-order predicate logic. This completeness is true for many other logics not, not, for example, the predicate logic of a higher level.

The compactness theorem, a central set of model theory, are calculated as a corollary of the completeness theorem.

As part of the Hilbert program ( to create a non-contradictory and complete calculus for mathematics ), the set 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 can not prove any true sentence. (Note that the incompleteness theorem to a different kind of completeness refers to as the completeness theorem presented here. )

Position in set theory

For countable ( or, more generally well-ordered ) sets of symbols can the completeness theorem from the axioms of Zermelo -Fraenkel set theory without the axiom of choice to prove. The proof for arbitrary symbol sets can be run with the axiom of choice, but the sentence is not equivalent to the axiom of choice but to ( relative to the axioms of set theory without the axiom of choice ) include:

• Ultrafilterlemma
• Compactness theorem
• Set of Lindenbaum
• Representation theorem for Boolean algebras