Syntax vs semantics — the split
Parent: soundness-and-completeness
The founding decoupling of modern logic: pull apart what you can derive from what is true, define each without the other, then ask how they relate.
Two independent sides
- Syntax (
⊢) — proofs: finite strings manipulated by fixed rules (axioms + inference rules like modus ponens). Purely formal — a proof is checkable by a machine that understands no meaning at all. "Γ ⊢ φ" = "there is a derivation ofφfromΓ."- Semantics (
⊨) — truth in models: a structure interprets the symbols, and⊨says a formula holds. Pure meaning. "Γ ⊨ φ" = "every model ofΓmakesφtrue."
The point is that these are defined separately: ⊢ never mentions a model; ⊨ never mentions a proof. There is no a-priori reason the derivable formulas and the true ones should be the same set — and making them precise independently is what let logic become mathematics:
- Hilbert / formalism gave syntax its rigor (proof as mechanical rewriting);
- Tarski (1933) gave semantics its rigor (a recursive definition of "
M ⊨ φ").
Why the split is the whole game
Once the two are separate objects, soundness (⊢ ⟹ ⊨) and completeness (⊨ ⟹ ⊢) become theorems that must be proved, not definitions — and each is proved by crossing the gap:
- soundness pushes truth through the rules (semantics ← syntax);
- completeness builds a model out of a consistent theory (semantics ← syntax, the other way).
And the split is permanent: it's why proof theory (the study of ⊢) and model theory (the study of ⊨) are different fields, and why Gödel incompleteness can even be stated — it's precisely the place where, for arithmetic, the two sides fail to coincide (⊨_ℕ outruns ⊢_PA). The Curry–Howard correspondence is the same syntax↔semantics theme one level up (proofs ↔ programs).