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, a formal system is semantically complete if:

^{[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 computable 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.

Main article: Model complete theory |

A theory is *model complete* if and only if every embedding of its models is an elementary embedding.