Syntax meets semantics — the fundamental bridge
Logic has two faces: syntax (formal proofs, derivation rules) and semantics (truth, models, satisfaction). The fundamental question is whether they agree. Soundness says every provable formula is true. Completeness says every true formula is provable. Together, they tell us that the proof system perfectly captures logical truth.
In this lesson, you will see syntax and semantics side by side, explore completeness concretely, and discover how models relate to theories.
For a propositional tautology, the syntactic proof (a derivation tree) and the semantic verification (a truth table with all T) are two completely different processes that reach the same conclusion. This coincidence is not an accident -- it is the content of the soundness and completeness theorems.
Soundness says the proof system never proves a falsehood (if ⊢ φ then ⊨ φ). Completeness says every semantic truth has a proof (if ⊨ φ then ⊢ φ). Together they mean the syntactic and semantic notions of validity coincide.
Key insight: Soundness (⊢ φ implies ⊨ φ) is usually easy to prove: check each rule preserves truth. Completeness (⊨ φ implies ⊢ φ) is deep: it says the rules are powerful enough to capture all semantic truths.
For propositional logic with two variables, there are 16 possible truth functions. Some are tautologies, some contradictions, and most are contingencies. The completeness theorem guarantees that every tautology among them has a formal proof. Explore all 16 and verify the correspondence.
All 16 possible truth functions on two variables (p, q). Click any cell to inspect it.
Provable: truth table all T
Completeness Theorem: The set of tautologies (blue cells) equals exactly the set of provable formulas. Every truth function that is always true has a formal proof, and every provable formula is indeed always true.
Key insight: Godel proved completeness for first-order logic in 1929: every first-order sentence true in all models is provable. This is one of the crowning achievements of mathematical logic.
A model of a set of axioms is a structure that satisfies all of them. A theory is the set of all sentences true in every model of the axioms. Model theory studies the interplay between axiom systems and the structures they describe. This is the gateway to the Model Theory module.
Click a candidate structure to see which axiom it fails (if any). Blue-bordered structures are models that satisfy all axioms.
Key insight: The same axioms can have very different models. The group axioms describe everything from Z/2Z to the monster group. Understanding what axioms can and cannot pin down is the heart of model theory.