Formal Systems — The Syntax–Semantics Distinction
The starting point of all logic
Introduction (high school to first-year university)
Goal of this page
Understand that syntax (manipulating symbols) and semantics (truth, interpretation) are different things. Be able to explain in words the difference between $\vdash$ (provable) and $\models$ (true).
1. The idea of a formal system
To treat mathematical proof rigorously, we must first make clear "on top of what a proof is an operation." The framework for this is a formal system. A formal system is defined purely by the allowed symbols and the rules for how they may be assembled and rewritten.
A formal system specifies three things: (1) a set of symbols (an alphabet), (2) syntactic rules that determine which symbol strings are well-formed formulas, and (3) inference rules that derive formulas from formulas, together with starting-point axioms.
Crucially, nowhere in the definition do "meaning" or "truth" appear. A formal system is just a game of rearranging symbols; what the symbols stand for is the job of a separately given "interpretation."
2. Separating syntax and semantics
Syntax is the totality of rules concerning the shape and arrangement of symbols. Whether a formula is well-formed, and whether one formula can be derived from another by the rules, can all be decided mechanically by the shape of the symbols alone.
Semantics is the interpretation that assigns objects or truth values to symbol strings. For instance, assigning "true" or "false" to a propositional variable $p$ determines whether the formula $p \to q$ is true.
Consider the formula $p \to (q \to p)$.
- The syntactic view: this is a well-formed formula in which the symbols "$p$," "$\to$," "$($," … are arranged according to the rules. Moreover, using the inference rules, it may be derivable with no assumptions at all.
- The semantic view: no matter what truth values are assigned to $p, q$, this formula is always true (a tautology).
"Derivable" and "always true" happen to coincide here, but as definitions they are entirely different matters.
3. "Derivable" $\vdash$ and "true" $\models$
The distinction between syntax and semantics appears clearly in two symbols.
$\Gamma \vdash A$ (syntactic consequence): from the set of assumptions $\Gamma$, the formula $A$ can be derived using only the axioms and inference rules of the proof system. This asserts that a symbol string called a proof exists.
$\Gamma \models A$ (semantic consequence): in every interpretation (model) that makes all formulas of $\Gamma$ true, $A$ is also true. This asserts that truth is preserved.
The symbols look similar, but one speaks of "the existence of a proof" and the other of "truth in every model" — entirely different worlds. The power of formal logic lies in cleanly separating the everyday "can be proved" and "is correct" into these two.
Many textbooks call $\vdash$ the "turnstile" and $\models$ the "double turnstile." Throughout this series we consciously use $\vdash$ when talking about syntax and $\models$ when talking about semantics.
4. Why this distinction is decisive
Separating syntax and semantics naturally raises two big questions.
- Soundness: if $\Gamma \vdash A$, does $\Gamma \models A$? — "Is what we derived actually true?" (does it never prove a falsehood?).
- Completeness: if $\Gamma \models A$, does $\Gamma \vdash A$? — "Is everything true necessarily derivable?" (does it never miss a truth?).
These two are addressed head-on in Basic: Soundness and Completeness. Furthermore, the fact that syntax can be checked mechanically is the basis of proof checking and of proof assistants. Precisely because the correctness of a proof is reduced to syntax rather than meaning, we can entrust the checking to a computer.
Summary
Key points
- Formal system: a "game of symbols" defined only by symbols, syntactic rules, axioms, and inference rules
- Syntax: the shape and manipulation of symbols; decidable mechanically
- Semantics: interpretation of symbols; fixes truth values
- $\vdash$: derivable (a proof exists) / $\models$: always true (true in every model)
- When the two coincide is the central question of soundness and completeness
Frequently asked questions
What is the difference between syntax and semantics?
Syntax is the set of rules for how symbols may be arranged and rewritten; it can be decided mechanically by the shape of the symbols alone. Semantics is the interpretation of what those symbol strings refer to and when they are true. "Being derivable by the rules" and "being true" are in principle different matters, and distinguishing them is the starting point for understanding a formal system.
How do the symbols $\vdash$ and $\models$ differ?
$\Gamma \vdash A$ is a syntactic relation: $A$ can be derived from $\Gamma$ by the rules of the proof system (the existence of a proof). $\Gamma \models A$ is a semantic relation: in every interpretation that makes all of $\Gamma$ true, $A$ is also true (preservation of truth). When the two coincide is the question of soundness and completeness.
Why treat logic by symbol manipulation alone, discarding meaning?
Restricting to syntax lets us check a proof's correctness mechanically, by the shape of the symbols alone. Meaning tends to depend on human interpretation, but syntactic rules can be defined unambiguously and checked by a machine. Proof assistants can trust a proof precisely because it ultimately reduces to this mechanical syntactic check.