Soundness & completeness

Parent: logic

Modern logic's founding move is to split a logic into two a priori unrelated sides — then prove they coincide. Soundness and completeness are those coincidence theorems.

syntax-and-semantics — the split: syntax (⊢, proofs = finite, meaning-less symbol manipulation) vs semantics (⊨, truth in models = meaning). The whole subject lives on decoupling these and re-relating them.
soundness — ⊢ φ ⟹ ⊨ φ: everything provable is true (the calculus tells no lies). Easy direction.
completeness — ⊨ φ ⟹ ⊢ φ: everything true is provable (no gaps). The hard direction (Gödel, 1929).
propositional-example — see both directions at once on P → (Q → P) (truth table + proof).
hilbert-godel-tarski — how the split was born: the crisis, Hilbert's program, Tarski's truth, Gödel's completeness and incompleteness.
canonical-model — the canonical/term model: how completeness is actually proved (Lindenbaum + Henkin + truth lemma — the syntax becomes the model), worked on the syllogism.

Together: ⊢ φ ⟺ ⊨ φ — provability = truth. A proof system that is both is a faithful mirror of meaning.

Why it's foundational

Logic wants two things that look incompatible: proofs must be mechanical (checkable, no appeal to meaning — Hilbert's formalism), yet they must certify truth (meaning — Tarski's semantics). Soundness+completeness are exactly the bridge:

compute truth by proving — the basis of automated reasoning and proof assistants (a sound kernel means a checked term is genuinely true);
study provability and truth as separate objects — this births proof theory (syntax) and model theory (semantics) as distinct fields;
and they set the stage for Gödel incompleteness: for arithmetic, syntax and semantics come apart — a theory can't prove every truth of ℕ (see the caveat below).

Full story of how it was born → hilbert-godel-tarski. A concrete propositional walk-through → propositional-example.

completeness ≠ "not incomplete"

Completeness of a proof system (proves all valid formulas — FOL, propositional) is a different thing from Gödel incompleteness (a theory can't prove all sentences true in its intended model ℕ). Don't conflate them.