How the split was born (Hilbert → Tarski → Gödel)
Parent: soundness-and-completeness
The syntax/semantics distinction and the soundness/completeness bridge weren't handed down — they were forged over ~50 years, out of a crisis and a failed dream.
1. The crisis that forced formalization (late 1800s)
Three shocks made "obvious" reasoning untrustworthy: the rigorization of analysis (ε–δ replacing intuition about limits); non-Euclidean geometry (the parallel postulate is a choice, not a truth); and the set-theoretic paradoxes (Russell's paradox, 1901 — the set of all sets that don't contain themselves). If intuition can mislead, proofs must become objects you can check without intuition.
2. Making syntax precise (Frege → Russell → Hilbert)
- Frege, Begriffsschrift (1879): the first genuine formal system — quantifiers, and proof as rule-governed symbol manipulation.
- Russell–Whitehead, Principia Mathematica (1910–13): derive mathematics inside a formal logic.
- Hilbert's program (1920s): formalism — treat mathematics as a finitary game of symbols, and settle everything by syntactic means. Three goals for a formal system of math: it should be complete (every truth is derivable), consistent (provably, by finitary methods), and decidable (an algorithm for provability — the Entscheidungsproblem). Syntax was to be sovereign.
3. Making semantics precise (Tarski, 1933)
Until now "true" was informal. Tarski, The Concept of Truth in Formalized Languages (1933): a recursive definition of M ⊨ φ — truth-in-a-structure, built up from atoms by the connectives/quantifiers. Now semantics is as rigorous as syntax, and the two sides of the split are both mathematical objects — so "do provability and truth coincide?" becomes a precise question.
4. The answers — one yes, then a wall of noes
- Post (1921): propositional calculus is sound and complete.
- Gödel's completeness theorem (1929, his thesis): first-order logic is complete —
⊢ = ⊨for validity. Hilbert's first goal, achieved for the logic itself. - Gödel's incompleteness theorems (1931): the wall. Any consistent, recursively axiomatized theory strong enough for arithmetic has true-but-unprovable sentences, and cannot prove its own consistency. Here
⊢_PAand⊨_ℕcome apart — syntax cannot capture arithmetic truth. Hilbert's completeness-and-consistency dream for theories dies. - Church & Turing (1936): the Entscheidungsproblem is unsolvable — no algorithm decides validity (fol-undecidability). The third Hilbert goal dies too.
5. What survived — the lens
The distinction is exactly what lets us state all of this cleanly: completeness (1929) says syntax reaches all logical validities; incompleteness (1931) says syntax can't reach all arithmetic truths; undecidability (1936) says even the reachable ones can't be decided. The split then permanently forked logic into model theory (Tarski, Robinson — the study of ⊨) and proof theory (Gentzen — the study of ⊢).