Soundness

Logical systems[edit]

In mathematical logic, a logical system has the soundness property if every formula that can be proved in the system is logically valid with respect to the semantics of the system. In most cases, this comes down to its rules having the property of preserving truth.^[4] The converse of soundness is known as completeness.


A logical system with syntactic entailment ${\displaystyle \vdash }$ and semantic entailment ${\displaystyle \models }$ is sound if for any sequence ${\displaystyle A_{1},A_{2},...,A_{n}}$ of sentences in its language, if ${\displaystyle A_{1},A_{2},...,A_{n}\vdash C}$, then ${\displaystyle A_{1},A_{2},...,A_{n}\models C}$. In other words, a system is sound when all of its theorems are tautologies.


Soundness is among the most fundamental properties of mathematical logic. The soundness property provides the initial reason for counting a logical system as desirable. The completeness property means that every validity (truth) is provable. Together they imply that all and only validities are provable.


Most proofs of soundness are trivial. For example, in an axiomatic system, proof of soundness amounts to verifying the validity of the axioms and that the rules of inference preserve validity (or the weaker property, truth). If the system allows Hilbert-style deduction, it requires only verifying the validity of the axioms and one rule of inference, namely modus ponens. (and sometimes substitution)


Soundness properties come in two main varieties: weak and strong soundness, of which the former is a restricted form of the latter.