nLab completeness theorem

Idea

A formal system is complete or semantically complete when all its tautologies are theorems. Since tautologies are defined by reference to “all models”, this can depend on the class of models under consideration.

Examples

• Kurt Gödel showed that classical first-order logic is complete, that is, any first-order sentence, $\phi$, which is true under any interpretation, is provable from the axioms of first-order logic. This is generally known as the completeness theorem. Here the “interpretations” are the models in sets, assigning a set to every sort and a binary truth value $\{\bot,\top\}$ to every proposition.

• If in an infinitary logic, infinitely many quantifiers may appear in sentences, then completeness does not hold.

• In constructive mathematics, Gödel’s proof is not available, and (perhaps depending on definitions) constructive logic may not be complete with respect to ordinary models in sets. However, there are still completeness theorems with respect to models in arbitrary categories, which generally proceed by way of construction of a syntactic model in which the true statements are precisely the theorems.

Related entries

• Deligne completeness theorem

• incompleteness theorem