A topic in the Open Knowledge Graph — a free, open map of 15,290 topics and the order to learn them in.
Soundness means that every formula provable in the proof system is semantically valid: if ⊢ φ then ⊨ φ. Completeness is the converse: every valid formula is provable: if ⊨ φ then ⊢ φ. Together they establish that syntax and semantics perfectly align — proof and truth coincide for propositional logic. Soundness is proved by verifying each inference rule preserves validity. Completeness is proved by showing that any consistent set of formulas has a model (the Lindenbaum–Henkin construction is one approach). These two results certify that the proof system is neither too weak nor too strong.
Prove soundness first by structural induction on derivations. Then study the completeness proof as an example of the Lindenbaum lemma. See how each direction fails if rules are added or removed.
Throughout your study of propositional logic you have been working with two different notions of "correctness." On the semantic side, ⊨ φ means φ is a tautology — true under every truth-value assignment. On the syntactic side, ⊢ φ means φ is derivable using the rules of your proof system (natural deduction, sequent calculus, or another system). These are defined completely independently: semantics is about truth tables; syntax is about symbol manipulation. The questions of soundness and completeness ask whether these two notions align.
Soundness (⊢ φ ⟹ ⊨ φ) says: the proof system never proves a falsehood. Every formula you can derive is indeed a tautology. Proving soundness is typically a structural induction on derivations: you verify that the *axiom schemas* are all tautologies (base case) and that each *inference rule* preserves validity (inductive step). For example, modus ponens: if φ and φ → ψ are both valid, then ψ must be valid, because in any assignment where φ → ψ is true and φ is true, ψ must be true. Checking each rule this way establishes that no derivation can ever produce a non-tautology.
Completeness (⊨ φ ⟹ ⊢ φ) says: the proof system misses nothing. Every tautology has a proof. This is harder to prove because you must show an arbitrary tautology — of which there are infinitely many — has a derivation. One classical approach uses the Lindenbaum lemma: starting from the assumption that ¬φ is consistent (i.e., that φ is not provable), you construct a maximal consistent extension that becomes a model for ¬φ. If you successfully build such a model, you have shown ¬φ is satisfiable, which means φ is not a tautology — contrapositive gives you completeness. For propositional logic, a more direct approach uses truth-table methods to systematically construct proofs from a formula's structure.
It is instructive to consider what each property alone is worth. A proof system with only the rule "derive ⊤" (top) is sound — it only proves the tautology ⊤ — but it is extremely incomplete. A proof system with the additional rule "from any formula, derive any formula" is complete (trivially, everything is provable) but catastrophically unsound. Neither property is useful without the other. Together, soundness and completeness say that the proof system is a *faithful representation* of logical truth — you can safely replace semantic reasoning with syntactic proof.
This result matters because proofs are finitary and mechanical: a derivation is a finite object you can write down and check by algorithm. Tautologies, by contrast, are defined over all possible truth assignments — potentially an infinite check. Completeness tells you that the finite syntactic world of proofs and the infinite semantic world of models nevertheless agree perfectly. This equivalence is what justifies using formal proof systems as the foundation of mathematics and formal verification.