Mathematics.

model theory

Soundness and Completeness

Mathematical Logic25 minDifficulty3 out of 10

You should know: formal proof systems

Overview

Soundness and completeness are the two theorems that connect syntax (⊢, formal derivability) to semantics (⊨, truth in every model) for a given logic and proof system. Soundness states that every provable formula is semantically valid — Γ ⊢ φ implies Γ ⊨ φ — meaning the proof system never lets you derive a false conclusion from true premises; it guarantees the system doesn't 'lie.' Completeness, the converse, states that every valid formula is provable — Γ ⊨ φ implies Γ ⊢ φ — meaning the proof system is powerful enough to prove everything that is semantically true; it guarantees the system doesn't 'miss' anything. Kurt Gödel proved in his 1930 completeness theorem that standard first-order logic, with a suitable proof system (e.g. Hilbert-style or natural deduction), is both sound and complete — a foundational, positive result that should not be confused with his separate (and quite different) 1931 incompleteness theorems about arithmetic.

Intuition

Think of ⊢ as 'what the rulebook lets you formally derive' and ⊨ as 'what is actually true in every possible world consistent with your premises.' Soundness says the rulebook is trustworthy — it never certifies something false as a theorem — while completeness says the rulebook is exhaustive — it can certify every genuinely true statement, leaving no true fact permanently out of reach. Gödel's 1930 completeness theorem shows first-order logic achieves both simultaneously: the syntactic game of formal proof and the semantic notion of truth-in-every-model line up perfectly, which is a deep and reassuring fact — it's precisely because first-order logic is complete in this sense that its later incompleteness results about arithmetic (a much stronger, different claim about specific theories like Peano arithmetic) come as such a striking contrast.

Formal Definition

Definition

For a proof system and semantics over a logic, given a set of premises Γ and formula φ:

Soundness: Γ⊢φ  ⟹  Γ⊨φ\text{Soundness: } \Gamma \vdash \varphi \implies \Gamma \vDash \varphi
Everything provable is true (in all models)
Completeness: Γ⊨φ  ⟹  Γ⊢φ\text{Completeness: } \Gamma \vDash \varphi \implies \Gamma \vdash \varphi
Everything true (in all models) is provable
Together: Γ⊢φ  ⟺  Γ⊨φ\text{Together: } \Gamma \vdash \varphi \iff \Gamma \vDash \varphi
Gödel's completeness theorem for first-order logic (1930)

Worked Examples

  1. Suppose φ and φ→ψ are both true under some truth assignment.

    φ=T, φ→ψ=T\varphi = T,\ \varphi \rightarrow \psi = T

  2. By the truth table for →, φ→ψ is true and φ is true only when ψ is also true (since φ→ψ is false exactly when φ=T, ψ=F).

    φ=T and (φ→ψ)=T  ⟹  ψ=T\varphi = T \text{ and } (\varphi\to\psi)=T \implies \psi = T

Answer: Whenever the premises of modus ponens are true, its conclusion is guaranteed true — so the rule preserves semantic truth, contributing to soundness.

Practice Problems

Difficulty 2/10

If a proof system is sound but not complete, what could go wrong in practice?

Difficulty 3/10

State Gödel's 1930 completeness theorem precisely, and name what logic it applies to.

Difficulty 4/10

Explain why the completeness theorem for first-order logic (1930) and the incompleteness theorems (1931) are not contradictory, despite both being due to Gödel and both using the word 'complete/incomplete.'

Quiz

Soundness of a proof system means:
Completeness of a proof system means:
Gödel's 1930 completeness theorem and his 1931 incompleteness theorems:

Summary

  • Soundness (Γ⊢φ ⟹ Γ⊨φ) guarantees a proof system never derives a false conclusion from true premises.
  • Completeness (Γ⊨φ ⟹ Γ⊢φ) guarantees the proof system can derive every semantically valid conclusion.
  • Gödel's 1930 completeness theorem shows first-order logic achieves both — a distinct, earlier, and positive result from his 1931 incompleteness theorems about arithmetic.

References

  1. WebsiteWikipedia — Gödel's completeness theorem