# Completeness

In logic, semantic completeness is the converse of soundness for formal systems. A formal system is "semantically complete" when all tautologies are theorems whereas a formal system is "sound" when all theorems are tautologies. Kurt Gödel, Leon Henkin, and Emil Post all published proofs of completeness. (See History of the Church–Turing thesis.) A system is consistent if a proof never exists for both P and not P.

• For a formal system S in formal language L, S is semantically complete or simply complete, iff every logically valid formula of L (every formula which is true under every interpretation of L) is a theorem of S. That is, Failed to parse (Can't write to or create math temp directory): \\models_{\\mathrm S} A\\ \\to\\ \\vdash_{\\mathrm S} A

.<ref name="metalogic">Hunter, Geoffrey, Metalogic: An Introduction to the Metatheory of Standard First-Order Logic, University of California Pres, 1971</ref>

• A formal system S is strongly complete or complete in the strong sense iff for every set of premises T, any formula which semantically follows from T is derivable from T. That is, Failed to parse (Can't write to or create math temp directory): T\\models_{\\mathrm S} A\\ \\to\\ T\\vdash_{\\mathrm S} A

.

• A formal system S is syntactically complete or deductively complete or maximally complete or simply complete iff for each formula A of the language of the system either A or ¬A is a theorem of S. This is also called negation completeness. In another sense, a formal system is syntactically complete iff no unprovable axiom can be added to it as an axiom 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 variable "a" is not a theorem, and neither is its negation, but these are not tautologies). Gödel's incompleteness theorem shows that no recursive system that is sufficiently powerful, such as the Peano axioms, can be both consistent and complete.
• A formal system is inconsistent iff every sentence is a theorem.<ref>Alfred Tarski, Über einige fundamentale Begriffe der Mathematik, Comptes Rendus des séances de la Société des Sciences et des Lettres de Varsovie 23 (1930), Cl. III, pp. 22–29. English translation in: Alfred Tarski, Logic, Semantics, Metamathematics, Claredon Press, Oxford, 1956, pp. 30–37.</ref>
• A language is expressively complete if it can express the subject matter for which it is intended.Template:Fact
• A formal system is complete with respect to a property iff every sentence that has the property is a theorem.

## References

  1. ^ Hunter, Geoffrey, Metalogic: An Introduction to the Metatheory of Standard First-Order Logic, University of California Pres, 1971
2. ^ Alfred Tarski, Über einige fundamentale Begriffe der Mathematik, Comptes Rendus des séances de la Société des Sciences et des Lettres de Varsovie 23 (1930), Cl. III, pp. 22–29. English translation in: Alfred Tarski, Logic, Semantics, Metamathematics, Claredon Press, Oxford, 1956, pp. 30–37.