Soundness theorem

In mathematical logic, a logical system has the soundness property if and only if its inference rules prove only formulas that are valid with respect to its semantics. In symbols, soundness is the then part of this expression ${\displaystyle A1,A2,...An\vdash C}$ if and only if ${\displaystyle A1,A2,...\models C}$, where ${\displaystyle \vdash }$ means derivation, ${\displaystyle \models }$ means tautological entailment. The other direction is completeness. In most cases, this comes down to its rules having the property of preserving truth.

...
Wikipedia