The soundness theorem is a theorem in mathematical logic stating for a given system of inference rules and system of axioms satisfying certain conditions, any first-order formula that is provable is universally valid.

The converse of the soundness theorem (stating that valid expressions are theorems) is known as Gödel's completeness theorem.