Soundness and Completeness
Why "provable ⟺ true" holds
Basic (1st–2nd year university)
Goal of this page
Understand the two bridges connecting syntax $\vdash$ and semantics $\models$: soundness (what is derived is true) and completeness (what is true is derivable). Learn that only when both hold can we say "provable ⟺ true."
1. Two directions connecting $\vdash$ and $\models$
As seen in the Introduction, $\Gamma \vdash A$ (derivable by the rules) and $\Gamma \models A$ ($A$ is true in every model that makes $\Gamma$ true) are different definitions. Their relationship raises two questions of opposite direction.
What "true" means here. Throughout this page, "true" always means $\Gamma \models A$: $A$ holds in every model that makes $\Gamma$ true (logically true). It does not mean "true in the real world." So "provable ⟺ true" is, stated precisely, the claim that in first-order predicate logic, derivability by the rules coincides with truth in every model.
2. Soundness: what is derived is true
Soundness
$\Gamma \vdash A \;\Rightarrow\; \Gamma \models A$. That is, a formula derived in the proof system is also semantically true (in every model that makes $\Gamma$ true).
Soundness guarantees that the proof system derives no falsehoods. Without it, something could be derivable by the rules yet actually false, making proof meaningless. It is what must hold before anything else — the minimum requirement for trusting a proof system.
The proof is relatively easy. For each inference rule, check one by one that "if all premises are true, the conclusion is true" (truth is preserved), and chain it by induction on the structure of the proof (its length / tree height). Each natural-deduction rule is designed precisely to satisfy this truth-preservation.
3. Completeness: what is true is derivable
Completeness
$\Gamma \models A \;\Rightarrow\; \Gamma \vdash A$. That is, a semantically correct formula (a logical consequence of $\Gamma$) is always derivable in the proof system.
Completeness guarantees that the proof system misses no truth. Opposite in direction to soundness, it is generally much harder to show. For first-order predicate logic it holds as Gödel's completeness theorem (1930); typically one proves the contrapositive ("a non-derivable formula has a model that makes it false") by constructing, e.g., a maximal consistent set.
Completeness also holds for classical propositional logic, which is the equivalence "derivable by the rules ⟺ a tautology" mentioned in the Introduction.
How the proof goes (the flavour only). Completeness is obtained by proving the contrapositive. (1) Suppose $\Gamma \vdash A$ fails. (2) Then $\Gamma \cup \{\neg A\}$ is consistent. Add new constants to the language (Henkin constants) and, preserving consistency, add for each existential sentence $\exists x\, \varphi(x)$ a witness axiom $\exists x\, \varphi(x) \to \varphi(c)$. (3) Extend further to a maximal consistent set — a consistent set to which no further formula can be added without contradiction (Lindenbaum's lemma) — and use it as a blueprint to build the term model, whose individuals are the terms themselves. (4) In the resulting model every member of $\Gamma$ is true while $A$ is false, so $\Gamma \models A$ fails. That contrapositive is completeness. The details belong to a full logic textbook.
4. The completeness theorem is not the incompleteness theorem
The names are confusing, but the completeness theorem and the incompleteness theorems concern different objects. The completeness theorem is a claim about logic ("every logically valid formula is derivable"). The incompleteness theorems are claims that "a specific theory such as arithmetic contains statements that are true but unprovable within it." The former is about the validity of logic, the latter about the limits of a particular theory's proving power; they do not contradict.
Soundness and completeness are foundational results of logic guaranteeing that the two worlds of syntax (proof) and semantics (truth) correspond cleanly. Because of this correspondence, we can entrust the semantic goal of "verifying truth" to the syntactic task of "constructing a proof."
5. Going further: how far does completeness go?
This section is optional further reading; the goals of this page are already met by sections 1–4. What we have simply called "completeness" so far is, strictly speaking, a theorem about first-order predicate logic. Once we drop the restriction that only individuals may be quantified and move to higher-order logic, where predicates and sets themselves can be quantified, the guarantee is lost.
Higher-order logic has no sound, complete, effective deductive system under standard semantics
Under standard semantics — the reading in which a variable for an $n$-ary predicate ranges over all $n$-ary relations on the domain — there is no deductive system for second- or higher-order logic that is simultaneously sound, complete, and effective (i.e. whose axioms and rules are mechanically checkable, so that the set of theorems is recursively enumerable).
The reason is the flip side of incompleteness. In second-order logic, induction can be written as the single axiom "for every property $P$ …", which makes second-order Peano arithmetic categorical: any structure satisfying the axioms is isomorphic to $\mathbb{N}$, so for an arithmetic sentence $\varphi$, "follows logically from the axioms" coincides with "is true in $\mathbb{N}$". If there were a deductive system that was sound, complete and effective (its proofs mechanically checkable), then enumerating proofs would enumerate every arithmetic sentence true in $\mathbb{N}$. But true arithmetic — the set of first-order arithmetic sentences true in the standard model $\mathbb{N}$ — is not recursively enumerable. Hence no such system can exist. This fact is two sides of the same coin as Gödel's incompleteness theorems and Tarski's undefinability of truth.
Completeness is not the only casualty. Neither the compactness theorem nor the downward Löwenheim–Skolem theorem holds for second-order logic under standard semantics. Read in the other direction, under natural conditions on abstract logics, first-order logic is the most expressive logic that retains both (Lindström's theorem). Expressive power and good metatheory pull against each other, and first-order logic became the common language of mathematics precisely because it sits at that balance point.
So how do HOL Light and Isabelle/HOL relate to completeness? The higher-order logic these proof assistants adopt is read with Henkin semantics (general models) rather than standard semantics: the domains of function and predicate types are not fixed to be "all conceivable functions" but may be any suitable subcollection closed under comprehension. Under this reading completeness is restored (Henkin, 1950) and the system can effectively be treated as many-sorted first-order logic. The claim "higher-order logic is incomplete" is therefore a statement about standard semantics, not a defect in the implemented proof systems. Checking a given proof mechanically is in any case a separate matter from semantic completeness: a system that is sound but incomplete still works perfectly well as a proof assistant.
Summary
Key points
- Soundness: $\Gamma \vdash A \Rightarrow \Gamma \models A$ (what is derived is true; no falsehoods)
- Completeness: $\Gamma \models A \Rightarrow \Gamma \vdash A$ (what is true is derivable; nothing missed)
- When both hold, "provable ⟺ true"
- Soundness = rule truth-preservation + induction; completeness (first-order) = Gödel's completeness theorem
- The completeness theorem and incompleteness theorems concern different objects and do not contradict
- Propositional and first-order logic are complete for their standard semantics; second- and higher-order logic under standard semantics has no sound, complete, effective deductive system (it is restored under Henkin semantics)
References
- Gödel, K. (1930). "Die Vollständigkeit der Axiome des logischen Funktionenkalküls". Monatshefte für Mathematik und Physik, 37, 349–360. (the completeness theorem for first-order logic)
- Henkin, L. (1949). "The completeness of the first-order functional calculus". Journal of Symbolic Logic, 14(3), 159–166. (the modern proof building a model from a maximal consistent set)
- Henkin, L. (1950). "Completeness in the theory of types". Journal of Symbolic Logic, 15(2), 81–91. (completeness of higher-order logic under general models)
- Lindström, P. (1969). "On extensions of elementary logic". Theoria, 35(1), 1–11. (the characterisation of first-order logic by compactness and Löwenheim–Skolem)
- Enderton, H. B. (2001). A Mathematical Introduction to Logic (2nd ed.). Academic Press. (a standard textbook treatment of soundness and completeness)
Frequently asked questions
What is soundness?
The property "what is provable is true," i.e., $\Gamma \vdash A$ implies $\Gamma \models A$. It guarantees the proof system derives no falsehoods (rules preserve truth). It is shown by checking each rule preserves truth and inducting on the length of the proof.
What is completeness?
The property "what is true is provable," i.e., $\Gamma \models A$ implies $\Gamma \vdash A$. It guarantees the proof system can derive every semantically valid statement. For first-order predicate logic it holds as Gödel's completeness theorem.
Do the completeness and incompleteness theorems contradict?
No. The completeness theorem is about logic ("every logically valid formula is derivable"); the incompleteness theorems are about specific theories ("arithmetic contains statements that are true but unprovable within it"). The former concerns the validity of logic, the latter the limits of a particular theory.
Does the completeness theorem hold for higher-order logic?
Not under standard semantics. No deductive system for second- or higher-order logic is at once sound, complete, and effective (with a recursively enumerable set of theorems), which follows from the categoricity of second-order arithmetic together with the fact that true arithmetic (the first-order sentences true in the standard model) is not recursively enumerable. Under Henkin semantics (general models), however, completeness is restored, and this is the reading adopted by HOL Light and Isabelle/HOL.