Definition
A logical system is complete (or semantically complete) if every semantically valid formula is derivable within the system. Formally, for a logic with derivability relation and semantic entailment :
This states that if is a semantic consequence of (true in all models satisfying ), then is derivable from using the proof rules.
Alternative Formulation
A logical theory is syntactically complete if, for every proposition in the language, either or is derivable.
Under soundness (the converse property ), these two notions are equivalent. Together, soundness and completeness establish:
This equivalence shows that syntactic derivability perfectly matches semantic validity.
Classical Logic
Propositional Logic
Classical propositional logic is complete with respect to truth table semantics. Every tautology has a proof in Natural Deduction or other standard proof systems. The completeness proof is relatively straightforward using truth tables.
First-Order Logic
Gödel’s completeness theorem (1930) established that first-order classical logic is semantically complete. This fundamental result shows that the standard axiomatizations of first-order logic prove exactly the semantically valid formulas.
Intuitionistic Logic
Propositional Case
Intuitionistic propositional logic is complete with respect to Kripke Semantics and Topological Semantics. The completeness proof often uses canonical models constructed from consistent theories.
First-Order Case
First-order intuitionistic logic is complete with respect to Kripke models over arbitrary frames. This was established through Beth Trees and other semantic methods.
Other Logics
Modal Logic
Different modal logics require different completeness theorems:
- S4: Complete with respect to reflexive and transitive frames
- S5: Complete with respect to equivalence relations
- K: Complete with respect to arbitrary accessibility relations
Type Theory
- Simply-Typed Lambda Calculus: Complete with respect to standard models in set theory
- System F: Strong normalization provides a form of completeness
- Martin-Löf Type Theory: Computational completeness through normalization
Temporal Logic
- Linear Temporal Logic (LTL): Complete with respect to infinite sequences
- Computation Tree Logic (CTL): Complete with respect to branching time structures
Proof Techniques
Common methods for establishing completeness include:
- Canonical model construction from maximal consistent sets
- Henkin’s method using witness constants
- Cut elimination in sequent calculi
- Normalization in natural deduction systems
The choice of technique depends on the specific logic and the intended semantic framework.
Limitations
Not all logics are semantically complete:
- Second-order logic is incomplete due to the non-axiomatizability of its valid formulas (Gödel, 1931)
- Some non-classical logics lack completeness with respect to their intended semantics
- Computational systems may be incomplete due to undecidability results