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.

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

Main article: Functional completeness |

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

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

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:

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.

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.

Main article: admissible rule |

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