Syntax meets semantics — the fundamental bridge
Proofs push symbols around; truth tables check meaning. These two very different methods always agree, and this lesson shows what that guarantee says.
Pick a tautology and compare the two sides: a proof tree derives it, and a truth table shows it true on every row.
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.
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.
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.
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.
Click any of the 16 two-variable truth functions to see whether it is a tautology, a contradiction, or a contingency. Every tautology has a formal proof.
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.
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.
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.
Choose an axiom system and click the candidate structures to see which ones satisfy every axiom.
Click a candidate structure to see which axiom it fails (if any). Blue-bordered structures are models that satisfy all axioms.
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.
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.
Spot a mistake or have an idea?