Definition
The propositional calculus is the formal system of classical propositional logic — propositional variables (P, Q, R) combined with the five connectives ~, ∧, ∨, ⊃, ≡, plus axioms and inference rules for proving tautologies. It is both sound (every theorem is a tautology) and complete (every tautology is a theorem), making it the most well-behaved interesting formal system.
Why it matters
How it works
Build formulas from propositional variables and connectives. Define theoremhood via axiom schemes and inference rules (typically modus ponens plus rules for the connectives). Verify soundness by checking that each axiom is a tautology and each rule preserves tautologyhood. Verify completeness via the Henkin construction or by normal-form arguments. Decide tautologyhood mechanically by truth-table inspection (exponential), DPLL backtracking, or modern SAT solvers (often polynomial in practice).