Soundness is the property 'what is provable is true,' i.e., $\Gamma \vdash A$ implies $\Gamma \models A$. It guarantees that the proof system derives no falsehoods (the inference rules preserve truth). It is shown by checking that each rule preserves truth and chaining this by induction on the length of the proof.

Completeness is the property 'what is true is provable,' i.e., $\Gamma \models A$ implies $\Gamma \vdash A$. It guarantees that the proof system can derive every semantically valid statement without exception. For first-order predicate logic it holds as Gödel's completeness theorem.

Soundness and Completeness

Q: Do the completeness theorem and the incompleteness theorems contradict each other

No. The completeness theorem is a claim about logic ('every logically valid formula is derivable'); the incompleteness theorems are about specific theories ('a theory such as arithmetic contains statements that are true but unprovable within it'). They concern different objects: the validity of logic versus the limits of a particular theory's proving power.

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$ (true in every model) are different definitions. Their relationship raises two questions of opposite direction.

$\Gamma \vdash A$ $\Gamma \models A$ Both together: $\Gamma \vdash A \iff \Gamma \models A$

Figure 1: Soundness goes from syntax to semantics (what is derived is true); completeness goes from semantics to syntax (what is true is derivable). When both hold, "provable ⟺ true."

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. This is really the central thing we want — the minimum condition for trust.

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 (1929); 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.

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."

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

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.