Soundness

Definition for formal systems

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. The converse of soundness is known as completeness.

A logical system with syntactic entailment ${\displaystyle ⊢}$ 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⊢C}$, then ${\displaystyle A_1,A_2,...,A_n\models C}$. In other words, a system is sound when all of its theorems are validities.

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. Strong soundness is the definition given earlier in this section and weak soundness restricts this to sentences which are provable from no premises, i.e., when there are no sentences to the right of the turnstiles.

Weak soundness

Weak soundness of a deductive system is the property that any sentence that is provable from no premises in that deductive system is also true on all interpretations or structures of the semantic theory for the language upon which that theory is based. Symbolically we write, if ${\displaystyle ⊢C}$ then ${\displaystyle \models C}$. Some writers will explicitly include the empty set, giving if ${\displaystyle \mathrm{\varnothing }⊢C}$ then ${\displaystyle \mathrm{\varnothing }\models C}$. Using the narrow definition of theorem, for sentences provable from no premises, weak soundness says that all theorems are tautologies.

Strong soundness

Strong soundness of a deductive system is the property that any sentence ${\displaystyle C}$ that is provable from a (possibly empty) set of premises/sentences ${\displaystyle \mathrm{\Gamma }=\{A_1,A_2,...,A_n\}}$ is also a semantic consequence of that set, i.e., ${\displaystyle C}$ is true in any model that makes all members of ${\displaystyle \mathrm{\Gamma }}$. Symbolically we write, if ${\displaystyle \mathrm{\Gamma }⊢C}$, then ${\displaystyle \mathrm{\Gamma }\models C}$. Notice that when ${\displaystyle \mathrm{\Gamma }}$ is empty, we have the statement of weak soundness.

Arithmetic soundness

If T is a theory whose objects of discourse can be interpreted as natural numbers, we say T is arithmetically sound if all theorems of T are actually true about the standard mathematical integers. For further information, see ω-consistent theory.

Relation to completeness

The converse of the soundness property is the completeness property. A deductive system with a semantic theory is strongly complete if every sentence ${\displaystyle C}$ that is a semantic consequence of a set of sentences ${\displaystyle \mathrm{\Gamma }}$ can be derived in the deduction system from that set. In symbols: if ${\displaystyle \mathrm{\Gamma }\models C}$ then ${\displaystyle \mathrm{\Gamma }⊢C}$. Completeness of first-order logic was first explicitly established by Gödel, though some of the main results were contained in earlier work of Skolem.

Informally, a soundness theorem for a deductive system expresses that all provable sentences are true. Completeness states that all true sentences are provable.

Gödel's first incompleteness theorem shows that for languages sufficient for doing a certain amount of arithmetic, there can be no consistent and effective deductive system that is complete with respect to the intended interpretation of the symbolism of that language. Thus, not all sound deductive systems are complete in this special sense of completeness, in which the class of models (up to isomorphism) is restricted to the intended one. The original completeness proof applies to all classical models, not some special proper subclass of intended ones.