Inmathematical logic andmetalogic, aformal system is calledcomplete with respect to a particularproperty if everyformula having the property can bederived using that system, i.e. is one of itstheorems; otherwise the system is said to beincomplete.The term "complete" is also used without qualification, with differing meanings depending on the context, mostly referring to the property of semanticalvalidity. Intuitively, a system is called complete in this particular sense, if it can derive every formula that is true.

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

Aformal language isexpressively complete if it can express the subject matter for which it is intended.

A set oflogical connectives associated with a formal system isfunctionally complete if it can express allpropositional functions.

Semantic completeness is theconverse ofsoundness for formal systems. A formal system is complete with respect to tautologousness or "semantically complete" when all itstautologies aretheorems, whereas a formal system is "sound" when all theorems are tautologies (that is, they are semantically valid formulas: formulas that are true under everyinterpretation of the language of the system that is consistent with the rules of the system). That is, a formal system is semantically complete if:

${\displaystyle {\models }_{\mathcal{S}}\phi \to {⊢}_{\mathcal{S}}\phi .}$^[1]

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

A formal systemS isstrongly complete orcomplete in the strong sense if for every set of premises Γ, any formula that semantically follows from Γ is derivable from Γ. That is:

${\displaystyle \mathrm{\Gamma }{\models }_{\mathcal{S}}\phi \to \mathrm{\Gamma }{⊢}_{\mathcal{S}}\phi .}$

A formal systemS isrefutation-complete if it is able to derivefalse from everyunsatisfiable set of formulas. That is:

${\displaystyle \mathrm{\Gamma }{\models }_{\mathcal{S}}\mathrm{\perp }\to \mathrm{\Gamma }{⊢}_{\mathcal{S}}\mathrm{\perp }.}$^[2]

Every strongly complete system is also refutation complete. Intuitively, strong completeness means that, given a formula set${\displaystyle \mathrm{\Gamma }}$, it is possible tocompute every semantical consequence${\displaystyle \phi }$ of${\displaystyle \mathrm{\Gamma }}$, while refutation completeness means that, given a formula set${\displaystyle \mathrm{\Gamma }}$ and a formula${\displaystyle \phi }$, it is possible tocheck whether${\displaystyle \phi }$ is a semantical consequence of${\displaystyle \mathrm{\Gamma }}$.

Examples of refutation-complete systems include:SLD resolution onHorn clauses,superposition on equationalclausal first-order logic,Robinson's resolution on clause sets.^[3] The latter is not strongly complete: e.g.${\displaystyle \{a\}\models a\vee b}$ holds even in the propositional subset of first-order logic, but${\displaystyle a\vee b}$ cannot be derived from${\displaystyle \{a\}}$ by resolution. However,${\displaystyle \{a,\mathrm{\neg }(a\vee b)\}⊢\mathrm{\perp }}$ can be derived.

A formal systemS issyntactically complete ordeductively complete ormaximally complete ornegation complete if for eachsentence (closed formula) φ of the language of the system either φ or ¬φ is a theorem ofS. Syntactical completeness is a stronger property than semantic completeness. If a formal system is syntactically complete, a corresponding formal theory is calledcomplete if it is aconsistent theory.Gödel's incompleteness theorem shows that anycomputable system that is sufficiently powerful, such asPeano arithmetic, cannot be both consistent and syntactically complete.

Syntactical completeness can also refer to another unrelated concept, also calledPost completeness orHilbert-Post completeness. In this sense, a formal system issyntactically complete if and only if no unprovable sentence can be added to it without introducing aninconsistency.Truth-functional propositional logic andfirst-order predicate logic are semantically complete, but not syntactically complete (for example, the propositional logic statement consisting of a single propositional variableA is not a theorem, and neither is its negation).^{[citation needed]}

Insuperintuitionistic andmodal logics, a logic isstructurally complete if everyadmissible rule is derivable.

A theory ismodel complete if and only if every embedding of its models is anelementary embedding.

• Mathematical logic
• Metalogic
• Model theory
• Proof theory

• Articles with short description
• Short description is different from Wikidata
• All articles with unsourced statements
• Articles with unsourced statements from January 2025