A formal system S is syntactically complete or deductively complete or maximally complete or simply complete if and only if for each formula φ of the language of the system either φ or (not φ) is a theorem of S. This is also called negation completeness. In another sense, a formal system is syntactically complete if and only if 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). Godel’s incompleteness theorem shows that any recursive system that is sufficiently powerful, such as Peano arithmetic, cannot be both consistent and complete.

— Wikipedia on Completeness

2012.12.11 Tuesday ACHK

The branch of mathematical logic that deals with what is true in different models is called model theory. The branch called proof theory studies what can be formally proved in particular formal systems. The completeness theorem establishes a fundamental connection between these two branches, giving a link between semantics and syntax.

The completeness theorem should not, however, be misinterpreted as obliterating the difference between these two concepts; in fact Godel’s incompleteness theorem, another celebrated result, shows that there are inherent limitations in what can be achieved with formal proofs in mathematics.

The name for the incompleteness theorem refers to another meaning of complete (see model theory – Using the compactness and completeness theorems). In particular, Godel’s completeness theorem deals with formulas that are logical consequences of a first-order theory, while the incompleteness theorem constructs formulas that are not logical consequences of certain theories.

— 14 February 2012

— Wikipedia on Godel’s completeness theorem

2012.12.07 Friday ACHK