# Completeness (logic)

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.

## Contents

## [edit]

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[edit]

### Expressive completeness[edit]

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

### Functional completeness[edit]

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

### Semantic completeness[edit]

**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,

^{[1]}

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

### Strong completeness[edit]

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:

### Refutation completeness[edit]

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

^{[2]}

Every strongly complete system is also refutation-complete. Intuitively, strong completeness means that, given a formula set , it is possible to *compute* every semantical consequence of , while refutation-completeness means that, given a formula set and a formula , it is possible to *check* whether is a semantical consequence of .

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. holds even in the propositional subset of first-order logic, but cannot be derived from by resolution. However, can be derived.

### Syntactical completeness[edit]

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[edit]

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

## References[edit]

**^**Hunter, Geoffrey, Metalogic: An Introduction to the Metatheory of Standard First-Order Logic, University of California Pres, 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).*Artificial Intelligence: A Modern Approach*. Prentice Hall. Here: sect. 9.7, p.286