Soundness

Remarks

The standard Hilbert system for propositional logic is sound. Each axiom is a tautology, checked by a truth table, and modus ponens preserves truth under every assignment. Induction on the length of a derivation then gives soundness. Adding the rule "from $\psi$ and $\varphi \to \psi$, infer $\varphi$" gives an unsound system. With it, $\set{p \to q, \; q} \vdash p$, but the assignment $p = \mathsf{F}$, $q = \mathsf{T}$ shows $\set{p \to q, \; q} \not\models p$. The converse property, that $\Gamma \models \varphi$ implies $\Gamma \vdash \varphi$, is completeness. For first-order logic it is Gödel's completeness theorem.