Completeness (logic)

The term completeness has different meanings in logic. It describes two different properties of formal systems or calculi :

• Completeness of theories
• Completeness of calculi

In addition, this term is also used in the sense of

• functional completeness of sets of joiners

used.

Completeness of theories

definition

A theory is understood to be a real subset of sentences of a language of the first-order predicate logic that is closed with regard to the inference relation (deductive), that is, from already follows for all sentences of the language. If there is a model, then it is obviously a theory. A theory is called complete if it contains either this or its negation for every sentence . In this sense, a complete theory leaves no questions of the form “applies or in theory ?” Unanswered. ${\displaystyle T}$ ${\displaystyle L_{I}^{S}}$ ${\displaystyle \vdash }$ ${\displaystyle T\vdash \alpha }$ ${\displaystyle \alpha \in T}$ ${\displaystyle \alpha }$ ${\displaystyle {\mathcal {A}}}$ ${\displaystyle T=Th({\mathcal {A}}):=\{\alpha ;\,{\mathcal {A}}\vDash \alpha \}}$ ${\displaystyle \alpha }$ ${\displaystyle \neg \alpha }$ ${\displaystyle \alpha }$ ${\displaystyle \neg \alpha }$ ${\displaystyle T}$

characterization

The following statements about a theory are equivalent: ${\displaystyle T\varsubsetneq L_{I}^{S}}$

• ${\displaystyle T}$is complete, that is, for all sets is valid or ${\displaystyle \alpha }$ ${\displaystyle T\vDash \alpha }$ ${\displaystyle T\vDash \neg \alpha }$
• ${\displaystyle T}$is maximum, that is, for all theories to apply . ${\displaystyle T_{1}}$ ${\displaystyle T\subset T_{1}\varsubsetneq L_{I}^{S}}$ ${\displaystyle T=T_{1}}$
• For each model of true ${\displaystyle {\mathcal {A}}}$ ${\displaystyle T}$ ${\displaystyle T=Th({\mathcal {A}})}$
• Every two models of are elementarily equivalent . ${\displaystyle T}$

Examples

Let it be the theory of dense orders , that is, the signature is and is the set of all sentences that can be derived from the following four sentences (axioms of dense order). ${\displaystyle DO}$ ${\displaystyle S=\{<\}}$ ${\displaystyle DO}$ ${\displaystyle L_{I}^{S}}$

• ${\displaystyle \forall x\,\neg (x<x)}$ (Irreflectivity)
• ${\displaystyle \forall x\,y\,z\,(x<y\land y<z\rightarrow x<z)}$ (Transitivity)
• ${\displaystyle \forall x\,y\,(x=y\lor x<y\lor y<x)}$ (Linearity of order)
• ${\displaystyle \forall x\,y\,(x<y\rightarrow \exists z\,(x<z\land z<y))}$ (Tightness)

This theory is not complete, because the question of whether there are smallest or largest elements remains open. If one extends to the theory of all theorems, the above four and the two theorems ${\displaystyle DO}$ ${\displaystyle DO_{00}}$

• ${\displaystyle \forall x\,\exists y\,(y<x)}$ (there is no smallest element)
• ${\displaystyle \forall x\,\exists y\,(x<y)}$ (there is no largest element),

this gives a complete theory, because with the help of Fraïssé's theorem one can prove the elementary equivalence of two models, as explained there. This could easily have been proven with Vaught's criterion ; this provides further examples treated there, such as the theory of algebraically closed fields . The quantifier elimination is another method that can be used to prove completeness.

Decidability

Complete theories with an enumerable signature and a recursively enumerable axiomatization are decidable . To see this, set in motion an enumeration of all the propositions of the given theory by systematically generating all the proofs. If there is a sentence, at some point in this list or , because the theory is complete. Then break off the list and answer if it appeared in the list, otherwise answer . This algorithm apparently decides whether . ${\displaystyle \alpha }$ ${\displaystyle \alpha }$ ${\displaystyle \neg \alpha }$ ${\displaystyle \alpha \in T}$ ${\displaystyle \alpha }$ ${\displaystyle \alpha \notin T}$ ${\displaystyle \alpha \in T}$

Completeness of calculi

In colloquial terms, a formal system (a calculus) is semantically complete if every correct theorem can also be derived. This can be described more precisely as follows. Let be the derivative relation ; it is defined purely syntactically with the help of the rules of the formal system, in the case of predicate logic e.g. B. by the sequence calculus . These are rules for character manipulation. ${\displaystyle \vdash }$

There is also the level of semantics and the concept of logical inference belonging to this area, expressed by the symbol of the semantic sequence , which z. B. is explained in the semantics of propositional logic or the semantics of predicate logic . The formal semantics is the subject of the model theory going back to Alfred Tarski . ${\displaystyle \models }$

Of central interest in formal logic is the relationship between (syntactic) derivation and (semantic) inference : semantic completeness means that it always follows. ${\displaystyle \vdash }$ ${\displaystyle \models }$ ${\displaystyle \Sigma \models \psi }$ ${\displaystyle \Sigma \vdash \psi }$

The inversion, which always follows from, is called the correctness (also semantic correctness) of a formal system. ${\displaystyle \Sigma \vdash \psi }$ ${\displaystyle \Sigma \models \psi }$

For concrete formal systems, the correctness is usually easy to prove, because when constructing the formal system, one makes sure that every single rule is correct in this sense. A proof of completeness usually requires more in-depth investigations. The completeness theorem for the first order predicate logic was proved by Kurt Gödel in 1928 ( Gödel's completeness theorem ). An important proof method comes from Leon Henkin from 1949, see Henkin's theorem .

Functional completeness of sets of joiners

With functional completeness property is called a set of logical operators a logical system, to display all logical operators of the system. In classical propositional logic, for example, the set of connectives is functionally complete; H. all conceivable connectives can be expressed from conjunction and negation alone . ${\displaystyle \{\land ,\neg \}}$

Another complete system of connectives consists of the Sheffer's stroke alone . The system, which consists solely of the Peirce operator , is also complete.

literature

• HD Ebbinghaus, J. Flum, W. Thomas: Introduction to mathematical logic . BI-Wiss. Verlag, 1992, ISBN 3-411-15603-1
• Wolfgang Rautenberg : Introduction to Mathematical Logic . 3. Edition. Vieweg + Teubner, Wiesbaden 2008, ISBN 978-3-8348-0578-2 , doi : 10.1007 / 978-3-8348-9530-1 .
• Hans-Peter Tuschik, Helmut Wolter: Mathematical logic - in short. Basics, model theory, decidability, set theory . Mannheim-Leipzig-Vienna-Zurich; BI-Wiss. Verlag, Mannheim / Leipzig / Vienna / Zurich 1994, ISBN 3-411-16731-9

Web links

• Peter H. Starke: Logical Foundations of Computer Science . Script for the lecture, Humboldt University Berlin, October 2000

Individual evidence

1. ^ W. Rautenberg (2008), sentence 5.2.1.
2. ^ W. Rautenberg (2008), Corollary 1.2.2.