# Philosophy:Completeness (logic)

__: Characteristic of some logical systems__

**Short description**In mathematical logic and metalogic, a formal system is called **complete** with respect to a particular property if every formula having the property can be derived using that system, i.e. is one of its theorems; otherwise the system is said to be **incomplete**.
The term "complete" is also used without qualification, with differing meanings depending on the context, mostly referring to the property of semantical validity. Intuitively, a system is called complete in this particular sense, if it can derive every formula that is true.

The property converse to completeness is called soundness: a system is sound with respect to a property (mostly semantical validity) if each of its theorems has that property.

## Forms of completeness

### Expressive completeness

A formal language is **expressively complete** if it can express the subject matter for which it is intended.

### Functional completeness

A set of logical connectives associated with a formal system is **functionally complete** if it can express all propositional functions.

### Semantic completeness

**Semantic completeness** is the converse of soundness for formal systems. A formal system is complete with respect to tautologousness or "semantically complete" when all its tautologies are theorems, whereas a formal system is "sound" when all theorems are tautologies (that is, they are semantically valid formulas: formulas that are true under every interpretation of the language of the system that is consistent with the rules of the system). That is,

- [math]\displaystyle{ \models_{\mathcal S} \varphi\ \to\ \vdash_{\mathcal S} \varphi. }[/math]
^{[1]}

- [math]\displaystyle{ \models_{\mathcal S} \varphi\ \to\ \vdash_{\mathcal S} \varphi. }[/math]

For example, Gödel's completeness theorem establishes semantic completeness for first-order logic.

### Strong completeness

A formal system S is **strongly complete** or **complete in the strong sense** if for every set of premises Γ, any formula that semantically follows from Γ is derivable from Γ. That is:

- [math]\displaystyle{ \Gamma\models_{\mathcal S} \varphi \ \to\ \Gamma \vdash_{\mathcal S} \varphi. }[/math]

### Refutation completeness

A formal system S is **refutation-complete** if it is able to derive *false* from every unsatisfiable set of formulas. That is,

- [math]\displaystyle{ \Gamma \models_{\mathcal S} \bot \to\ \Gamma \vdash_{\mathcal S} \bot. }[/math]
^{[2]}

- [math]\displaystyle{ \Gamma \models_{\mathcal S} \bot \to\ \Gamma \vdash_{\mathcal S} \bot. }[/math]

Every strongly complete system is also refutation-complete. Intuitively, strong completeness means that, given a formula set [math]\displaystyle{ \Gamma }[/math], it is possible to *compute* every semantical consequence [math]\displaystyle{ \varphi }[/math] of [math]\displaystyle{ \Gamma }[/math], while refutation-completeness means that, given a formula set [math]\displaystyle{ \Gamma }[/math] and a formula [math]\displaystyle{ \varphi }[/math], it is possible to *check* whether [math]\displaystyle{ \varphi }[/math] is a semantical consequence of [math]\displaystyle{ \Gamma }[/math].

Examples of refutation-complete systems include: SLD resolution on Horn clauses, superposition on equational clausal first-order logic, Robinson's resolution on clause sets.^{[3]} The latter is not strongly complete: e.g. [math]\displaystyle{ \{ a \} \models a \lor b }[/math] holds even in the propositional subset of first-order logic, but [math]\displaystyle{ a \lor b }[/math] cannot be derived from [math]\displaystyle{ \{ a \} }[/math] by resolution. However, [math]\displaystyle{ \{ a, \lnot (a \lor b) \} \vdash \bot }[/math] can be derived.

### Syntactical completeness

A formal system S is **syntactically complete** or **deductively complete** or **maximally complete** if for each sentence (closed formula) φ of the language of the system either φ or ¬φ is a theorem of S. This is also called **negation completeness**, and is stronger than semantic completeness. In another sense, a formal system is **syntactically complete** if and only if no unprovable sentence can be added to it without introducing an inconsistency. Truth-functional propositional logic and first-order predicate logic are semantically complete, but not syntactically complete (for example, the propositional logic statement consisting of a single propositional variable **A** is not a theorem, and neither is its negation). Gödel's incompleteness theorem shows that any recursive system that is sufficiently powerful, such as Peano arithmetic, cannot be both consistent and syntactically complete.

### Structural completeness

In superintuitionistic and modal logics, a logic is **structurally complete** if every admissible rule is derivable.

## References

- ↑ Hunter, Geoffrey, Metalogic: An Introduction to the Metatheory of Standard First-Order Logic, University of California Press, 1971
- ↑ David A. Duffy (1991).
*Principles of Automated Theorem Proving*. Wiley. Here: sect. 2.2.3.1, p.33 - ↑ Stuart J. Russell, Peter Norvig (1995).
*A Modern Approach*. Prentice Hall. Here: sect. 9.7, p.286

Original source: https://en.wikipedia.org/wiki/Completeness (logic).
Read more |